ML Supported Predictions for SAT Solvers Performance

• URL: http://arxiv.org/abs/2112.09438v1
• Date: Fri, 17 Dec 2021 11:17:29 GMT
• Title: ML Supported Predictions for SAT Solvers Performance
• Authors: A.-M. Leventi-Peetz, J\"org-Volker Peetz, Martina Rohde
• Abstract summary: Internal solver runtime parameters have been collected and analyzed. A machine learning model has been created for the binary classification of the solver's termination behavior.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In order to classify the indeterministic termination behavior of the open source SAT solver CryptoMiniSat in multi-threading mode while processing hard to solve boolean satisfiability problem instances, internal solver runtime parameters have been collected and analyzed. A subset of these parameters has been selected and employed as features vector to successfully create a machine learning model for the binary classification of the solver's termination behavior with any single new solving run of a not yet solved instance. The model can be used for the early estimation of a solving attempt as belonging or not belonging to the class of candidates with good chances for a fast termination. In this context a combination of active profiles of runtime characteristics appear to mirror the influence of the solver's momentary heuristics on the immediate quality of the solver's resolution process. Because runtime parameters of already the first two solving iterations are enough to forecast termination of the attempt with good success scores, the results of the present work deliver a promising basis which can be further developed in order to enrich CryptoMiniSat or generally any modern SAT solver with AI abilities.

Related papers

• Self-Supervised Learning of Iterative Solvers for Constrained Optimization [0.0]
  We propose a learning-based iterative solver for constrained optimization. It can obtain very fast and accurate solutions by customizing the solver to a specific parametric optimization problem. A novel loss function based on the Karush-Kuhn-Tucker conditions of optimality is introduced, enabling fully self-supervised training of both neural networks.
  arXiv  Detail & Related papers  (2024-09-12T14:17:23Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits [0.9831489366502301]
  Machine learning (ML) techniques have been proposed to automatically select the best solver from a portfolio of solvers. These methods, known as meta-solvers, take an instance of a problem and a portfolio of solvers as input. "Anytime" meta-solvers predict the best-performing solver within the specified time limit.
  arXiv  Detail & Related papers  (2023-09-07T03:04:50Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SAT is a fundamental NP-complete problem with many applications, including automated scheduling. To solve large instances, SAT solvers have to rely on Booleans, e.g., choosing a branching variable in DPLL and CDCL solvers. We suggest a strategy of making a few initial steps with a trained ML model and then releasing control to classical runtimes.
  arXiv  Detail & Related papers  (2023-07-18T10:46:28Z)
• 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)
• 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)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  We present an end-to-end method to learn the proximal operator across non-family problems. We show that for weakly-ized objectives and under mild conditions, the method converges globally.
  arXiv  Detail & Related papers  (2022-01-28T05:53:28Z)
• 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)
• QROSS: QUBO Relaxation Parameter Optimisation via Learning Solver Surrogates [14.905085636501438]
  We build surrogate models of QUBO solvers via learning from solver data on a collection of instances of a problem. In this way, we are able capture the common structure of the instances and their interactions with the solver, and produce good choices of penalty parameters. QROSS is shown to generalise well to out-of-distribution datasets and different types of QUBO solvers.
  arXiv  Detail & Related papers  (2021-03-19T09:06:12Z)
• Meta-Solver for Neural Ordinary Differential Equations [77.8918415523446]
  We investigate how the variability in solvers' space can improve neural ODEs performance. We show that the right choice of solver parameterization can significantly affect neural ODEs models in terms of robustness to adversarial attacks.
  arXiv  Detail & Related papers  (2021-03-15T17:26:34Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)

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.