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

Research output: Contribution to journalArticlepeer-review

5 Scopus citations

Abstract

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.

Original languageEnglish
Pages (from-to)345-369
Number of pages25
JournalConstraints
Volume12
Issue number3
DOIs
StatePublished - Sep 2007

Bibliographical note

Funding Information:
Acknowledgements We acknowledge the support of NSF grant IIS-0325063 and KSEF grant KSEF-1036-RDE-008. We are thankful to the reviewers of the paper for many helpful comments.

Copyright:
Copyright 2008 Elsevier B.V., All rights reserved.

Keywords

  • Boolean satisfiability
  • Pseudo-Boolean constraints
  • Stochastic local search

ASJC Scopus subject areas

  • Software
  • Discrete Mathematics and Combinatorics
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint

Dive into the research topics of 'Satisfiability testing of boolean combinations of pseudo-boolean constraints using local-search techniques'. Together they form a unique fingerprint.

Cite this