Determining Optimal Arithmetic Circuits for Solving Linear Optimization Problems with SAT Solver

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.