SAT encodings for pseudo-Boolean constraints together with at-most-one constraints

DOI10.1016/J.ARTINT.2021.103604MaRDI QIDQ2060735zbMATH OpenOpenAlexFDO

Authors Miquel Bofill, Jordi Coll, Josep Suy, Felix Ulrich-Oltean, Mateu Villaret, Peter W. Nightingale

Publication date 13 December 2021

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2110.08068

zbMATH Keywords

at-most-one constraintsencodingpseudo-Boolean constraintsSAT

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07)

Abstract: When solving a combinatorial problem using propositional satisfiability (SAT), the encoding of the problem is of vital importance. We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint that appears in a wide variety of combinatorial problems such as timetabling, scheduling, and resource allocation. In some cases PB constraints occur together with at-most-one (AMO) constraints over subsets of their variables (forming PB(AMO) constraints). Recent work has shown that taking account of AMOs when encoding PB constraints using decision diagrams can produce a dramatic improvement in solver efficiency. In this paper we extend the approach to other state-of-the-art encodings of PB constraints, developing several new encodings for PB(AMO) constraints. Also, we present a more compact and efficient version of the popular Generalized Totalizer encoding, named Reduced Generalized Totalizer. This new encoding is also adapted for PB(AMO) constraints for a further gain. Our experiments show that the encodings of PB(AMO) constraints can be substantially smaller than those of PB constraints. PB(AMO) encodings allow many more instances to be solved within a time limit, and solving time is improved by more than one order of magnitude in some cases. We also observed that there is no single overall winner among the considered encodings, but efficiency of each encoding may depend on PB(AMO) characteristics such as the magnitude of coefficient values.

Recommendations

• New Encodings of Pseudo-Boolean Constraints into CNF
• scientific article; zbMATH DE number 5139168
• N-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
• Optimal base encodings for pseudo-Boolean constraints
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF

Cites work

• N-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
• A New Look at BDDs for Pseudo-Boolean Constraints
• Automatically improving constraint models in Savile Row
• Budgeting with bounded multiple-choice constraints.
• Cardinality networks: a theoretical and empirical study
• Combinatorial auctions: a survey
• Efficient CNF encoding of Boolean cardinality constraints
• Hard multidimensional multiple choice knapsack problems, an empirical study
• Heuristics for determining the number of warehouses for storing non-compatible products
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Integer Programming Formulation of Traveling Salesman Problems
• New Encodings of Pseudo-Boolean Constraints into CNF
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF
• Presolve Reductions in Mixed Integer Programming
• PSPLIB -- a project scheduling problem library
• Resource-constrained project scheduling: Notation, classification, models, and methods
• SAT encodings of pseudo-Boolean constraints with at-most-one relations
• Theory and Applications of Satisfiability Testing
• Toward leaner binary-clause reasoning in a satisfiability solver

Cited in

(11)

• N-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
• SAT encodings of pseudo-Boolean constraints with at-most-one relations
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 5139168 (Why is no real title available?)
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF
• New Encodings of Pseudo-Boolean Constraints into CNF
• A constraint programming-based iterated greedy algorithm for the open shop with sequence-dependent processing times and makespan minimization
• Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints
• Comparing and extending satisfiability solution methods for the resource-constrained project scheduling problem
• Solving weighted maximum satisfiability with branch and bound and clause learning
• Revisiting pseudo-Boolean encodings from an integer perspective

This page was built for publication: SAT encodings for pseudo-Boolean constraints together with at-most-one constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2060735)