Automatic Detection of At-Most-One and Exactly-One Relations for Improved SAT Encodings of Pseudo-Boolean Constraints

摘要: Pseudo-Boolean (PB) constraints often have a critical role in constraint satisfaction and optimisation problems. Encoding PB to SAT has proven be an efficient approach many applications, however care must taken encode them compactly with good propagation properties. It been shown that at-most-one (AMO) exactly-one (EO) relations over subsets of the variables can exploited various encodings constraints, improving their compactness solving performance. In this paper we detect AMO EO completely automatically exploit improve are based on Multi-Valued Decision Diagrams (MDDs). Our experiments show substantial reductions encoding size dramatic improvements time thanks automatic detection.