Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms

• URL: http://arxiv.org/abs/2210.13159v1
• Date: Mon, 24 Oct 2022 12:22:25 GMT
• Title: Towards an Understanding of Long-Tailed Runtimes of SLS Algorithms
• Authors: Jan-Hendrik Lorenz and Florian W\"orz
• Abstract summary: GapSAT solver demonstrated a successful way to improve the performance of an SLS solver on average by learning additional information. We propose a method for generating logically equivalent problem formulations. We prove that the runtimes for Sch"oning's random walk algorithm are approximately Johnson SB.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The satisfiability problem is one of the most famous problems in computer science. Its NP-completeness has been used to argue that SAT is intractable. However, there have been tremendous advances that allow SAT solvers to solve instances with millions of variables. A particularly successful paradigm is stochastic local search. In most cases, there are different ways of formulating the underlying problem. While it is known that this has an impact on the runtime of solvers, finding a helpful formulation is generally non-trivial. The recently introduced GapSAT solver [Lorenz and W\"orz 2020] demonstrated a successful way to improve the performance of an SLS solver on average by learning additional information which logically entails from the original problem. Still, there were cases in which the performance slightly deteriorated. This justifies in-depth investigations into how learning logical implications affects runtimes for SLS. In this work, we propose a method for generating logically equivalent problem formulations, generalizing the ideas of GapSAT. This allows a rigorous mathematical study of the effect on the runtime of SLS solvers. If the modification process is treated as random, Johnson SB distributions provide a perfect characterization of the hardness. Since the observed Johnson SB distributions approach lognormal distributions, our analysis also suggests that the hardness is long-tailed. As a second contribution, we theoretically prove that restarts are useful for long-tailed distributions. This implies that additional restarts can further refine all algorithms employing above mentioned modification technique. Since the empirical studies compellingly suggest that the runtime distributions follow Johnson SB distributions, we investigate this property theoretically. We succeed in proving that the runtimes for Sch\"oning's random walk algorithm are approximately Johnson SB.

Related papers

• Light Schrödinger Bridge [72.88707358656869]
  We develop a lightweight, simulation-free and theoretically justified Schr"odinger Bridges solver. Our light solver resembles the Gaussian mixture model which is widely used for density estimation. Inspired by this similarity, we also prove an important theoretical result showing that our light solver is a universal approximator of SBs.
  arXiv  Detail & Related papers  (2023-10-02T13:06:45Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers.
  arXiv  Detail & Related papers  (2023-09-20T16:27:52Z)
• 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)
• Approximating a RUM from Distributions on k-Slates [88.32814292632675]
  We find a generalization-time algorithm that finds the RUM that best approximates the given distribution on average. Our theoretical result can also be made practical: we obtain a that is effective and scales to real-world datasets.
  arXiv  Detail & Related papers  (2023-05-22T17:43:34Z)
• Formalizing Preferences Over Runtime Distributions [25.899669128438322]
  We use a utility-theoretic approach to characterize the scoring functions that describe preferences over algorithms. We show how to leverage a maximum-entropy approach for modeling underspecified captime distributions.
  arXiv  Detail & Related papers  (2022-05-25T19:43:48Z)
• 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)
• Choosing the Right Algorithm With Hints From Complexity Theory [16.33500498939925]
  We show that the Metropolis algorithm is clearly the best of all algorithms regarded for reasonable problem sizes. An artificial algorithm of this type having an $O(n log n)$ runtime leads to the result that the significance-based compact genetic algorithm (sig-cGA) can solve the DLB problem in time $O(n log n)$ with high probability.
  arXiv  Detail & Related papers  (2021-09-14T11:12:32Z)
• 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)
• Evidence for Long-Tails in SLS Algorithms [0.0]
  Local search (SLS) is a successful paradigm for solving the satisfiability problem of propositional logic. A recent development in this area involves solving not the original instance, but a modified, yet logically equivalent one. This paper studies how this technique affects the runtimes of SLS solvers.
  arXiv  Detail & Related papers  (2021-07-01T11:31:39Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)
• Hardness of Random Optimization Problems for Boolean Circuits, Low-Degree Polynomials, and Langevin Dynamics [78.46689176407936]
  We show that families of algorithms fail to produce nearly optimal solutions with high probability. For the case of Boolean circuits, our results improve the state-of-the-art bounds known in circuit complexity theory.
  arXiv  Detail & Related papers  (2020-04-25T05:45:59Z)

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.