Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints

• URL: http://arxiv.org/abs/2307.09342v2
• Date: Wed, 8 Nov 2023 10:33:04 GMT
• Title: Learning to Select SAT Encodings for Pseudo-Boolean and Linear Integer Constraints
• Authors: Felix Ulrich-Oltean, Peter Nightingale, James Alfred Walker
• Abstract summary: 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.
• Score: 1.1371889042789218
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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 encodings in the literature with widely varying performance, and the problem of selecting suitable encodings for a given problem instance is not trivial. We explore the problem of selecting encodings for pseudo-Boolean and linear constraints using a supervised machine learning approach. We show that it is possible to select encodings effectively using a standard set of features for constraint problems; however we obtain better performance with a new set of features specifically designed for the pseudo-Boolean and linear constraints. In fact, we achieve good results when selecting encodings for unseen problem classes. Our results compare favourably to AutoFolio when using the same feature set. We discuss the relative importance of instance features to the task of selecting the best encodings, and compare several variations of the machine learning method.

Related papers

• Efficient Encodings of the Travelling Salesperson Problem for Variational Quantum Algorithms [0.0]
  We investigate different encodings for the Travelling Salesperson Problem. We find evidence that the permutation encoding can yield good results since it does not suffer from feasibility issues.
  arXiv  Detail & Related papers  (2024-04-08T12:30:07Z)
• 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)
• Interactively Learning Preference Constraints in Linear Bandits [100.78514640066565]
  We study sequential decision-making with known rewards and unknown constraints. As an application, we consider learning constraints to represent human preferences in a driving simulation.
  arXiv  Detail & Related papers  (2022-06-10T17:52:58Z)
• Encoding trade-offs and design toolkits in quantum algorithms for discrete optimization: coloring, routing, scheduling, and other problems [0.0]
  We present an intuitive method for synthesizing and analyzing discrete (i.e., integer-based) optimization problems. This method is expressed using a discrete quantum intermediate representation (DQIR) that is encoding-independent. Second, we perform numerical studies comparing several runtime encodings. Third, we design low-depth graph-derived partial mixers (GDPMs) up to 16-level quantum variables.
  arXiv  Detail & Related papers  (2022-03-28T01:01:12Z)
• Fast Feature Selection with Fairness Constraints [49.142308856826396]
  We study the fundamental problem of selecting optimal features for model construction. This problem is computationally challenging on large datasets, even with the use of greedy algorithm variants. We extend the adaptive query model, recently proposed for the greedy forward selection for submodular functions, to the faster paradigm of Orthogonal Matching Pursuit for non-submodular functions. The proposed algorithm achieves exponentially fast parallel run time in the adaptive query model, scaling much better than prior work.
  arXiv  Detail & Related papers  (2022-02-28T12:26:47Z)
• 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)
• 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)
• Discovering Representations for Black-box Optimization [73.59962178534361]
  We show that black-box optimization encodings can be automatically learned, rather than hand designed. We show that learned representations make it possible to solve high-dimensional problems with orders of magnitude fewer evaluations than the standard MAP-Elites.
  arXiv  Detail & Related papers  (2020-03-09T20:06:20Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms. We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
  arXiv  Detail & Related papers  (2020-01-29T09:40:58Z)
• Optimal Clustering from Noisy Binary Feedback [75.17453757892152]
  We study the problem of clustering a set of items from binary user feedback. We devise an algorithm with a minimal cluster recovery error rate. For adaptive selection, we develop an algorithm inspired by the derivation of the information-theoretical error lower bounds.
  arXiv  Detail & Related papers  (2019-10-14T09:18: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.