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

• Applying the quantum approximate optimization algorithm to general constraint satisfaction problems [0.0]
  We develop theoretical techniques for analysing the performance of the quantum approximate optimization (QAOA) when applied to random constraint satisfaction problems (CSPs) Our techniques allow us to compute the success probability of QAOA with one layer and given parameters, when applied to randomly generated instances of CSPs. We find that random $k$-SAT seems to be the most promising of these CSPs for demonstrating a quantum-classical separation using QAOA.
  arXiv  Detail & Related papers  (2024-11-26T14:00:34Z)
• Contextual Combinatorial Bandits with Probabilistically Triggered Arms [55.9237004478033]
  We study contextual bandits with probabilistically triggered arms (C$2$MAB-T) under a variety of smoothness conditions. Under the triggering modulated (TPM) condition, we devise the C$2$-UC-T algorithm and derive a regret bound $tildeO(dsqrtT)$.
  arXiv  Detail & Related papers  (2023-03-30T02:51:00Z)
• 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)
• 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.