A More Compact Translation of Pseudo-Boolean Constraints into CNF such that Generalized Arc Consistency is Maintained

Norbert MantheyNorbert Manthey, Tobias PhilippTobias Philipp, Peter SteinkePeter Steinke

Norbert Manthey, Tobias Philipp, Peter Steinke
A More Compact Translation of Pseudo-Boolean Constraints into CNF such that Generalized Arc Consistency is Maintained
In Carsten Lutz and Michael Tielscher, eds., KI 2014: Advances in Artificial Intelligence, volume 8736 of Lecture Notes in Computer Science, 123-134, 2014. Springer

Details
Bibtex

KurzfassungAbstract
In this paper we answer the open question for the existence of a more compact encoding from Pseudo-Boolean constraints into CNF that maintains generalized arc consistency by unit propagation, formalized by Bailleux et al. In contrast to other encodings our approach is defined in an abstract way and we present a concrete instantiation, resulting in a space complexity of O(n2 log2(n) log(wmax)) clauses in contrast to O(n3 log(n) log(wmax)) clauses generated by the previously best known encoding that maintains generalized arc consistency.
Forschungsgruppe:Research Group: WissensverarbeitungKnowledge Representation and Reasoning

The final publication is available at Springer.

@inproceedings{MPS2014,
  author    = {Norbert Manthey and Tobias Philipp and Peter Steinke},
  title     = {A More Compact Translation of Pseudo-Boolean Constraints into
               {CNF} such that Generalized Arc Consistency is Maintained},
  editor    = {Carsten Lutz and Michael Tielscher},
  booktitle = {KI 2014: Advances in Artificial Intelligence},
  series    = {Lecture Notes in Computer Science},
  volume    = {8736},
  publisher = {Springer},
  year      = {2014},
  pages     = {123-134}
}