Pueblo: A Hybrid Pseudo-Boolean SAT Solver

10 years 12 months ago
Pueblo: A Hybrid Pseudo-Boolean SAT Solver
This paper introduces a new hybrid method for efficiently integrating Pseudo-Boolean (PB) constraints into generic SAT solvers in order to solve PB satisfiability and optimization problems. To achieve this, we adopt the cutting-plane technique to draw inferences among PB constraints and combine it with generic implication graph analysis for conflictinduced learning. Novel features of our approach include a light-weight and efficient hybrid learning and backjumping strategy for analyzing PB constraints and CNF clauses in order to simultaneously learn both a CNF clause and a PB constraint with minimum overhead and use both to determine the backtrack level. Several techniques for handling the original and learned PB constraints are introduced. Overall, our method benefits significantly from the pruning power of the learned PB constraints, while keeping the overhead of adding them into the problem low. In this paper, we also address two other methods for solving PB problems, namely Intege...
Hossein M. Sheini, Karem A. Sakallah
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JSAT
Authors Hossein M. Sheini, Karem A. Sakallah
Comments (0)