Encoding Linear Constraints into SAT
Linear integer constraints are one of the most important constraints in combinatorial problems since they are commonly found in many practical applications. Typically, encodings to Boolean satisfiability (SAT) format of conjunctive normal form perform poorly in problems with these constraints in comparison with SAT modulo theories (SMT), lazy clause generation (LCG) or mixed integer programming (MIP) solvers. In this paper we explore and categorize SAT encodings for linear integer constraints. We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We compare different SAT encodings of linear constraints and demonstrate where one may be preferable to another. We also compare SAT encodings against other solving methods and show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems. Combining the new encoding with lazy decomposition, which during runtime only encodes constraints that are important to the solving process that occurs, gives the best option for many highly combinatorial problems involving linear constraints.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Generalized Totalizer Encoding for Pseudo-Boolean Constraints
Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are used to model many real-world problems. A common approach to solve these constraints is to encode them into a SAT formula. The runtime of the …
ARCLearning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
Many constraint satisfaction and optimisation problems can be solved effectively by encoding them as instances of the Boolean Satisfiability problem (SAT). However, even the simplest types of constraints have many encodi…
Neural encoding with affine feature response transforms
Current linearizing encoding models that predict neural responses to sensory input typically neglect neuroscience-inspired constraints that could enhance model efficiency and interpretability. To address this, we propose…
A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Sever…
NegationOmniColor: A Unified Framework for Multi-modal Lineart Colorization
Lineart colorization is a critical stage in professional content creation, yet achieving precise and flexible results under diverse user constraints remains a significant challenge. To address this, we propose OmniColor,…