A New Method to Encode the At-Most-One Constraint into SAT

Van-Hau Nguyen, Thai Son Mai

Research output: Chapter in Book/Report/Conference proceedingConference contribution

18 Citations (Scopus)

Abstract

One of the most widely used constraints during the process of translating a practical problem into a propositional satisfiability (SAT) instance is the at-most-one (AMO) constraint. This paper proposes a new encoding for the AMO constraint, the so-called AMO bimander encoding which can be easily extended to encode cardinality constraints, which are often used in constraint programming. Experimental results reveal that the new encoding is very competitive compared with all other state-of-the-art encodings. Furthermore, we will prove that the new encoding allows unit propagation to achieve arc consistency - an important technique in constraint programming. We also show that a special case of the AMO bimander encoding outperforms the AMO binary encoding, a widely used encoding, in all our experiments.
Original languageEnglish
Title of host publicationProceedings of the Sixth International Symposium on Information and Communication Technology
Pages46-53
ISBN (Electronic)978-1-4503-3843-1
DOIs
Publication statusPublished - 2015
Externally publishedYes

Keywords

  • Boolean satisfiability
  • SAT encoding
  • at-most-one constraint
  • constraint programming
  • constraint satisfaction problem
  • CSP

Fingerprint

Dive into the research topics of 'A New Method to Encode the At-Most-One Constraint into SAT'. Together they form a unique fingerprint.

Cite this