Modern solvers for the Boolean Satisfiability (SAT) problem rely heavily on the analysis of conflicts in a backtrack search to learn useful constraints to guide the search. Other families of constraints such as linear pseudo-Boolean and cardinality constraints may more naturally express constraints normally found in many EDA applications, making the underlying structure more transparent. These constraints may be handled by generic integer linear programming (ILP) solvers, but they may ignore the Boolean nature of the variables.
We generalize learning schemes from recent SAT solvers to efficiently handle the more expressive constraints. Theoretical results have shown that there may be exponential improvements in runtime in moving from conjunctive normal form to cardinality constraints, which are exhibited in some of our experiments.