Algorithms for satisfiability problems in linear integer arithmetic logic.

Abstract

Recent advances in solving propositional satisfiability problems (SAT) have extended their applications to several domains including design verification and synthesis, program analysis, scheduling and temporal reasoning. Current methods for solving these problems mostly suffer from poor scalability especially when more expressive atoms from different theories are involved. In such cases methods such as abstraction or bit-vector conversion are adopted to translate the problem into a Boolean formula to be solved by a SAT solver. This conversion considerably affects the efficiency of the overall process. Nonetheless, the capability of SAT algorithms to solve large problems with tens of thousand of constraints over thousands of Boolean variables has brought them into the spotlight to be used for solving problems involving combination of different theories including linear and non-linear arithmetic. In this work, we present new scalable SAT-based algorithms for solving first-order linear integer arithmetic logic. We address problems involving arithmetic operations over Boolean variables (the so-called Pseudo-Boolean problems) as well as first-order formulas involving arithmetic operations over integer variables (the so-called Satisfiability Modulo Theories problems). In the latter case, we incorporate theory solvers for the conjunctions of cheap linear integer constraints, i.e. equalities and two-variable inequalities, within the SAT solver. These theory solvers are tightly but gradually integrated into the SAT solver and the problem is modeled such that the SAT solver is maximally utilized in order to leverage its power and efficiency. To curb the cost of processing hard constraints, i.e. general linear integer constraints, a subset of them are only added to the problem when/if the satisfiability of the rest of the problem is established. We also develop a set of algorithms to optimize the overall process taking into account special structures of the problems arising from design verification applications. These methods, implemented in our two solvers, Pueblo and Ario, have been applied to several problems in software verification, electronic design automation (EDA) and scheduling. In this work, we describe some of these applications and present advantages of our method in a few of them, mainly in hardware and software verification and temporal reasoning.