Dissertation/Thesis Abstract

Determining Optimal Arithmetic Circuits for Solving Linear Optimization Problems with SAT Solvers
by Nain, Prerna, M.S., California State University, Long Beach, 2018, 54; 10752239
Abstract (Summary)

As the fields of Artificial Intelligence, operations research, and computer science are expanding, the complexity of computing problems also increases, making such problems more difficult to solve. Broadly speaking, many such problems are constraint programming problems. Constraint programming is the paradigm which can be successfully applied to areas such as scheduling, vehicle routing, and many more. All these decision problems are NP-complete and thus hard to solve. In this paper, we will discuss two ways to solve these problems. One is by reducing the problem to a satisfiablity problem and solving it using a SAT solver. Minisat, a SAT solver, is used in this study. The other way is to reduce the problem to a quantified boolean formula decision problem and solve it using the QBF Backjump algorithm. The advantage of using this algorithm is that it is more expressive and makes encoding much simpler. Also, we will discuss how these algorithms accelerate problem solving when they are used with various arithmetic circuits. We will use Linear Optimization problems as input for both of the algorithms. These linear constraint problems are translated to the arithmetic circuit, which is composed of many adder and multiplication circuits. The circuit for addition can be designed by using one of the two arithmetic adders, namely Ripple-Carry (RC) adder, which gives linear size, and Carry-Look-Ahead (CLA) adder, which provides log-linear size. Also, the circuit for multiplication will have either linear size or log-linear size, based on the choice of adder, because multiplication involves addition of partial products. The results show that CLA outperforms the RC adder because the circuit optimization phase reduces the size of the circuit and makes the size comparable to that of RC.

Indexing (document details)
Advisor: Ebert, Todd
Commitee: Englert, Burkhard, Ponce, Oscar Morales
School: California State University, Long Beach
Department: Computer Engineering and Computer Science
School Location: United States -- California
Source: MAI 57/06M(E), Masters Abstracts International
Subjects: Computer science
Keywords: Arithmetic adders and multipliers, Arithmetic encoding, Constraint programming, Effect of encoding on performance, QBF backjumoping algorithms, SAT solvers
Publication Number: 10752239
ISBN: 9780438121553
Copyright © 2019 ProQuest LLC. All rights reserved. Terms and Conditions Privacy Policy Cookie Policy