Satisfiability testing of boolean combinations of pseudo-boolean constraints using local-search techniques

Some search problems are most directly specified by conjunctions of (sets of) disjunctions of pseudo-Boolean (PB) constraints. We study a logic PL ^PB whose formulas are of such form, and design local-search methods to compute models of PL ^PB theories. In our approach we view a PL ^PB theory T as a data structure, a concise representation of a certain propositional conjunctive normal form (CNF) theory cl(T) logically equivalent to T. The key idea is an observation that parameters needed by local-search algorithms for CNF theories, such as walksat, can be estimated on the basis of T without the need to compute cl(T) explicitly. We compare our methods to a local-search algorithm wsat(oip). The experiments demonstrate that our approach performs better. In order for wsat(oip) to handle arbitrary PL ^PB theories, it is necessary to represent disjunctions of PB constraints by sets of PB constraints, which often increases the size of the theory dramatically. A better performance of our method underscores the importance of developing solvers that work directly on PL ^PB theories.