An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations

摘要

Pseudo-Boolean (PB) constraints are ubiquitous in Constraint Satisfaction Problems. Encoding such constraints to SAT has proved to be an efficient solving approach. A commonly used technique for encoding PB constraints consists in representing the constraint as a Binary Decision Diagram (BDD), and then encoding this BDD to SAT. A key point in this technique is to obtain small BDD representations to generate small SAT formulas. In many problems, some subsets of the Boolean variables occurring in a PB constraint may also have other constraints imposed on them. In this work we introduce a way to take advantage of those constraints in order to obtain smaller SAT encodings. The main idea is that decision diagrams may be smaller if they avoid to represent truth assignments that are already forbidden by some other constraints. In particular, we present encodings for monotonic decreasing PB constraints, in conjunction with other constraints such as at-most-one, exactly-one and implication chains on subsets of their variables. We provide empirical evidence of the usefulness of this technique to reduce the size of the encodings as well as the solving time.