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.
|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|
|Keywords:||Arithmetic adders and multipliers, Arithmetic encoding, Constraint programming, Effect of encoding on performance, QBF backjumoping algorithms, SAT solvers|
Copyright in each Dissertation and Thesis is retained by the author. All Rights Reserved
The supplemental file or files you are about to download were provided to ProQuest by the author as part of a
dissertation or thesis. The supplemental files are provided "AS IS" without warranty. ProQuest is not responsible for the
content, format or impact on the supplemental file(s) on our system. in some cases, the file type may be unknown or
may be a .exe file. We recommend caution as you open such files.
Copyright of the original materials contained in the supplemental file is retained by the author and your access to the
supplemental files is subject to the ProQuest Terms and Conditions of use.
Depending on the size of the file(s) you are downloading, the system may take some time to download them. Please be