Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques

• Published in: Constraints : an international journal 2007-09, Vol.12 (3), p.345-369
• Main Authors: Liu, Lengning, Truszczyński, Mirosław
• Format: Article
• Language: English
• ISSN: 1383-7133; 1572-9354
• DOI: 10.1007/s10601-007-9022-z

Some search problems are most directly specified by conjunctions of (sets of) disjunctions of pseudo-Boolean (PB) constraints. We study a logic PL super()PBwhose formulas are of such form, and design local-search methods to compute models of PL super()PBtheories. In our approach we view a PL super()PBtheory 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 super()PBtheories, 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 super()PBtheories.