Encoding Linear Constraints into SAT

• URL: http://arxiv.org/abs/2005.02073v1
• Date: Tue, 5 May 2020 11:37:43 GMT
• Title: Encoding Linear Constraints into SAT
• Authors: Ignasi Ab\'io, Valentin Mayer-Eichberger, Peter Stuckey
• Abstract summary: We define new SAT encodings based on multi-valued decision diagrams, and sorting networks. We show they can be better than linear integer (MIP) solvers and sometimes better than LCG or SMT solvers on appropriate problems.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• General Method for Solving Four Types of SAT Problems [12.28597116379225]
  Existing methods provide varying algorithms for different types of Boolean satisfiability problems (SAT) This study proposes a unified framework DCSAT based on integer programming and reinforcement learning (RL) algorithm to solve different types of SAT problems.
  arXiv  Detail & Related papers  (2023-12-27T06:09:48Z)
• Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints [1.1371889042789218]
  We show that it is possible to select encodings effectively using a standard set of features for constraint problems. We obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. Our results compare favourably to AutoFolio when using the same feature set.
  arXiv  Detail & Related papers  (2023-07-18T15:26:46Z)
• Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints [39.96302127802424]
  We study a new application of hybrid Boolean constraints, which arises in quantum computing. The problem relates to constrained perfect matching in edge-colored graphs. We show that direct encodings of the constrained-matching problem as hybrid constraints scale poorly and special techniques are still needed.
  arXiv  Detail & Related papers  (2023-01-24T06:14:24Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  Constrained optimization problems abound in industry, from portfolio optimization to logistics. One of the major roadblocks in solving these problems is the presence of non-trivial hard constraints which limit the valid search space. In this work, we encode arbitrary integer-valued equality constraints of the form Ax=b, directly into U(1) symmetric networks (TNs) and leverage their applicability as quantum-inspired generative models.
  arXiv  Detail & Related papers  (2022-11-16T18:59:54Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints [5.62245362437303]
  We study encodings of Pseudo-Boolean (PB) constraints, a common type of arithmetic constraint. 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.
  arXiv  Detail & Related papers  (2021-10-15T12:53:01Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length. This problem is central in Combinatorial Testing for the detection of system failures.
  arXiv  Detail & Related papers  (2021-05-26T14:00:56Z)
• An Integer Linear Programming Framework for Mining Constraints from Data [81.60135973848125]
  We present a general framework for mining constraints from data. In particular, we consider the inference in structured output prediction as an integer linear programming (ILP) problem. We show that our approach can learn to solve 9x9 Sudoku puzzles and minimal spanning tree problems from examples without providing the underlying rules.
  arXiv  Detail & Related papers  (2020-06-18T20:09:53Z)
• Sparsified Linear Programming for Zero-Sum Equilibrium Finding [89.30539368124025]
  We present a totally different approach to the problem, which is competitive and often orders of magnitude better than the prior state of the art. With experiments on poker endgames, we demonstrate, for the first time, that modern linear program solvers are competitive against even game-specific modern variants of CFR.
  arXiv  Detail & Related papers  (2020-06-05T13:48:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.