Sciweavers

Share
JSAT
2006

A Translation of Pseudo Boolean Constraints to SAT

8 years 8 months ago
A Translation of Pseudo Boolean Constraints to SAT
This paper introduces a new CNF encoding of pseudo-Boolean constraints, which allows unit propagation to maintain generalized arc consistency. In the worst case, the size of the produced formula can be exponentially related to the size of the input constraint, but some important classes of pseudo-Boolean constraints, including Boolean cardinality constraints, are encoded in polynomial time and size. The proposed encoding was integrated in a solver based on the zChaff SAT solver and submitted to the PB05 evaluation. The results provide new perspectives in the field of full CNF approach of pseudo-Boolean constraints solving.
Olivier Bailleux, Yacine Boufkhad, Olivier Roussel
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JSAT
Authors Olivier Bailleux, Yacine Boufkhad, Olivier Roussel
Comments (0)
books