An MDD-based SAT encoding for pseudo-Boolean constraints with at-most-one relations
- PDF / 4,397,003 Bytes
- 32 Pages / 439.37 x 666.142 pts Page_size
- 24 Downloads / 175 Views
An MDD‑based SAT encoding for pseudo‑Boolean constraints with at‑most‑one relations Miquel Bofill1 · Jordi Coll1 · Josep Suy1 · Mateu Villaret1
© Springer Nature B.V. 2020
Abstract 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. Keywords Pseudo-Boolean · Decision diagram · At-most-one · Exactly-one · Implication chain · SAT · Encodings
1 Introduction ∑n Pseudo-Boolean (PB) constraints are linear expressions of the form i=1 qi xi #K , where # ∈ {} , q1 , … , qn and K are integer constants, and x1 , … , xn are 0/1 variables. A PB constraint represents a Boolean function f ∶ {0, 1}n → {0, 1} . A well-known * Jordi Coll [email protected] Miquel Bofill [email protected] Josep Suy [email protected] Mateu Villaret [email protected] 1
Universitat de Girona, Girona, Spain
13
Vol.:(0123456789)
M. Bofill et al.
approach to solve PB constraints is to represent them as Binary Decision Diagrams (BDD), which are then encoded into SAT (Eén and Sorensson 2006; Abío et al. 2012). PB constraints appear frequently in formulations of Constraint Satisfaction Problems (CSP). Sometimes, there are also other constraints imposed on the Boolean variables of a PB constraint. A very frequent case is that of the at-most-one (AMO) constraint, which states that at most one of the Boolean variables in a set can be assigned true. For example, in routing problems (Miller et al. 1960; Dantzig and Ramser 1959; Laporte 1992), the length of paths can be represented using PB constraints, where each variable encodes if the path is joining two particular points. Since it is usually required that Hamiltonian paths are followed, only one variable among the ones which represent going from a particular point to any other can be set to true. Also, in combinatorial auctions the objective function is usually a PB constraint (De Vries and Vohra 2003; Bofill et al. 2013), where each Boolean variable represents whether a ce
Data Loading...
