Title :
Pueblo: a modern pseudo-Boolean SAT solver
Author :
Sheini, Hossein M. ; Sakallah, Karem A.
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Michigan Univ., Ann Arbor, MI, USA
Abstract :
The paper introduces a new SAT (satisfiability) solver that integrates logic-based reasoning and integer programming methods to systems of CNF and PB constraints. Its novel features include an efficient PB literal watching strategy and several PB learning methods that take advantage of the pruning power of PB constraints while minimizing their overhead.
Keywords :
computability; constraint handling; inference mechanisms; integer programming; learning (artificial intelligence); minimisation; Boolean constraint propagation; integer programming; learning methods; literal watching strategy; logic-based reasoning; overhead minimization; pruning power; pseudo-Boolean SAT solver; pseudo-Boolean constraints; satisfiability solver; Automatic testing; Counting circuits; Data analysis; Design automation; Europe; Watches;
Conference_Titel :
Design, Automation and Test in Europe, 2005. Proceedings
Print_ISBN :
0-7695-2288-2
DOI :
10.1109/DATE.2005.246
