Decomposing Hard SAT Instances with Metaheuristic Optimization

• URL: http://arxiv.org/abs/2312.10436v1
• Date: Sat, 16 Dec 2023 12:44:36 GMT
• Title: Decomposing Hard SAT Instances with Metaheuristic Optimization
• Authors: Daniil Chivilikhin and Artem Pavlenko and Alexander Semenov
• Abstract summary: We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
• Score: 52.03315747221343
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In the article, within the framework of the Boolean Satisfiability problem (SAT), the problem of estimating the hardness of specific Boolean formulas w.r.t. a specific complete SAT solving algorithm is considered. Based on the well-known Strong Backdoor Set (SBS) concept, we introduce the notion of decomposition hardness (d-hardness). If $B$ is an arbitrary subset of the set of variables occurring in a SAT formula $C$, and $A$ is an arbitrary complete SAT solver , then the d-hardness expresses an estimate of the hardness of $C$ w.r.t. $A$ and $B$. We show that the d-hardness of $C$ w.r.t. a particular $B$ can be expressed in terms of the expected value of a special random variable associated with $A$, $B$, and $C$. For its computational evaluation, algorithms based on the Monte Carlo method can be used. The problem of finding $B$ with the minimum value of d-hardness is formulated as an optimization problem for a pseudo-Boolean function whose values are calculated as a result of a probabilistic experiment. To minimize this function, we use evolutionary algorithms. In the experimental part, we demonstrate the applicability of the concept of d-hardness and the methods of its estimation to solving hard unsatisfiable SAT instances.

Related papers

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• Deterministic Nonsmooth Nonconvex Optimization [94.01526844386977]
  We show that randomization is necessary to obtain a dimension-free dimension-free algorithm. Our algorithm yields the first deterministic dimension-free algorithm for optimizing ReLU networks.
  arXiv  Detail & Related papers  (2023-02-16T13:57:19Z)
• Mind the gap: Achieving a super-Grover quantum speedup by jumping to the end [114.3957763744719]
  We present a quantum algorithm that has rigorous runtime guarantees for several families of binary optimization problems. We show that the algorithm finds the optimal solution in time $O*(2(0.5-c)n)$ for an $n$-independent constant $c$. We also show that for a large fraction of random instances from the $k$-spin model and for any fully satisfiable or slightly frustrated $k$-CSP formula, statement (a) is the case.
  arXiv  Detail & Related papers  (2022-12-03T02:45:23Z)
• 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)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  We propose a novel method named Multi-block-probe Variance Reduced (MSVR) to alleviate the complexity of compositional problems. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on strongity.
  arXiv  Detail & Related papers  (2022-07-18T12:03:26Z)
• MAJORITY-3SAT (and Related Problems) in Polynomial Time [4.035753155957698]
  We give an algorithm that can determine whether a given $k$-CNF has at least $ rho in (0,1)$ with bounded denominator. Our algorithms have interesting positive implications for counting complexity and the complexity of inference.
  arXiv  Detail & Related papers  (2021-07-06T17:24:04Z)
• diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming [0.0]
  diff-SAT combines regular solving with the capability to use probabilistic clauses, facts and rules. The sampling process minimizes a user-defined differentiable objective function.
  arXiv  Detail & Related papers  (2021-01-03T09:04:31Z)
• Learning from Survey Propagation: a Neural Network for MAX-E-$3$-SAT [0.0]
  This paper presents a new algorithm for computing approximate solutions in $Theta(N)$ for the Maximum Exact 3-Satisfiability (MAX-E-$3$-SAT) problem.
  arXiv  Detail & Related papers  (2020-12-10T07:59:54Z)
• List-Decodable Mean Estimation in Nearly-PCA Time [50.79691056481693]
  We study the fundamental task of list-decodable mean estimation in high dimensions. Our algorithm runs in time $widetildeO(ndk)$ for all $k = O(sqrtd) cup Omega(d)$, where $n$ is the size of the dataset. A variant of our algorithm has runtime $widetildeO(ndk)$ for all $k$, at the expense of an $O(sqrtlog k)$ factor in the recovery guarantee
  arXiv  Detail & Related papers  (2020-11-19T17:21:37Z)

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.