SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints

• URL: http://arxiv.org/abs/2110.08068v1
• Date: Fri, 15 Oct 2021 12:53:01 GMT
• Title: SAT Encodings for Pseudo-Boolean Constraints Together With At-Most-One Constraints
• Authors: Miquel Bofill and Jordi Coll and Peter Nightingale and Josep Suy and Felix Ulrich-Oltean and Mateu Villaret
• Abstract summary: 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.
• Score: 5.62245362437303
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• Deep Learning Assisted Multiuser MIMO Load Modulated Systems for Enhanced Downlink mmWave Communications [68.96633803796003]
  This paper is focused on multiuser load modulation arrays (MU-LMAs) which are attractive due to their low system complexity and reduced cost for millimeter wave (mmWave) multi-input multi-output (MIMO) systems. The existing precoding algorithm for downlink MU-LMA relies on a sub-array structured (SAS) transmitter which may suffer from decreased degrees of freedom and complex system configuration. In this paper, we conceive an MU-LMA system employing a full-array structured (FAS) transmitter and propose two algorithms accordingly.
  arXiv  Detail & Related papers  (2023-11-08T08:54:56Z)
• Using Integer Constraint Solving in Reuse Based Requirements Engineering [0.0]
  Product Lines (PL) have proved an effective approach to reuse-based configurations. It is now widely acknowledged that a product can be considered as a constraint satisfaction problem. It is natural to consider constraint programming as a first choice candidate to specify constraints on PL. This paper proposes to further explore the use of integer constraint programming to specify PL constraints.
  arXiv  Detail & Related papers  (2023-09-28T09:20:07Z)
• Toward Unified Controllable Text Generation via Regular Expression Instruction [56.68753672187368]
  Our paper introduces Regular Expression Instruction (REI), which utilizes an instruction-based mechanism to fully exploit regular expressions' advantages to uniformly model diverse constraints. Our method only requires fine-tuning on medium-scale language models or few-shot, in-context learning on large language models, and requires no further adjustment when applied to various constraint combinations.
  arXiv  Detail & Related papers  (2023-09-19T09:05:14Z)
• 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)
• DiNADO: Norm-Disentangled Neurally-Decomposed Oracles for Controlling Language Models [55.06442277395388]
  NeurAlly-Decomposed Oracle (NADO) is a powerful approach for controllable generation with large language models. Vanilla NADO suffers from vanishing gradient for low-probability control signals. We propose a improved version of the NADO algorithm, namely DiNADO, which improves the performance of the NADO algorithm.
  arXiv  Detail & Related papers  (2023-06-20T18:36:52Z)
• Qubit Number Optimization for Restriction Terms of QUBO Hamiltonians [62.997667081978825]
  It is mathematically allowed to ask for fractional values of $R$. We show how they can reduce the number of qubits needed to implement the restriction hamiltonian even further. Finally, we characterize the response of DWave's Advantage$_$system4.1 Quantum Annealer (QA) when faced with the implementation of FRCs.
  arXiv  Detail & Related papers  (2023-06-12T08:25:56Z)
• 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)
• Lifting Symmetry Breaking Constraints with Inductive Logic Programming [2.036811219647753]
  We introduce a new model-oriented approach for Answer Set Programming that lifts the Symmetry Breaking Constraints into a set of interpretable first-order constraints. Experiments demonstrate the ability of our framework to learn general constraints from instance-specific SBCs.
  arXiv  Detail & Related papers  (2021-12-22T11:27:48Z)
• 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)
• Encoding Linear Constraints into SAT [0.0]
  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.
  arXiv  Detail & Related papers  (2020-05-05T11:37:43Z)

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.