SAT Requires Exhaustive Search
- URL: http://arxiv.org/abs/2302.09512v8
- Date: Thu, 21 Sep 2023 09:49:23 GMT
- Title: SAT Requires Exhaustive Search
- Authors: Ke Xu, Guangyan Zhou
- Abstract summary: This paper shows that proving computational hardness is not hard in mathematics.
In cases of extremely hard examples, exhaustive search may be the only viable option.
It makes the separation between SAT (with long clauses) and 3-SAT much easier than that between 3-SAT and 2-SAT.
- Score: 5.859552783895773
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this paper, by constructing extremely hard examples of CSP (with large
domains) and SAT (with long clauses), we prove that such examples cannot be
solved without exhaustive search, which is stronger than P $\neq$ NP. This
constructive approach for proving impossibility results is very different (and
missing) from those currently used in computational complexity theory, but is
similar to that used by Kurt G\"{o}del in proving his famous logical
impossibility results. Just as shown by G\"{o}del's results that proving formal
unprovability is feasible in mathematics, the results of this paper show that
proving computational hardness is not hard in mathematics. Specifically,
proving lower bounds for many problems, such as 3-SAT, can be challenging
because these problems have various effective strategies available for avoiding
exhaustive search. However, in cases of extremely hard examples, exhaustive
search may be the only viable option, and proving its necessity becomes more
straightforward. Consequently, it makes the separation between SAT (with long
clauses) and 3-SAT much easier than that between 3-SAT and 2-SAT. Finally, the
main results of this paper demonstrate that the fundamental difference between
the syntax and the semantics revealed by G\"{o}del's results also exists in CSP
and SAT.
Related papers
- Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
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.
arXiv Detail & Related papers (2023-12-16T12:44:36Z) - Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
We introduce CausalSAT, which employs causal reasoning to gain insights into the functioning of modern SAT solvers.
We use CausalSAT to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings.
arXiv Detail & Related papers (2023-06-09T22:53:16Z) - A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems.
The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
arXiv Detail & Related papers (2023-06-07T12:19:22Z) - Amplitude amplification-inspired QAOA: Improving the success probability
for solving 3SAT [55.78588835407174]
The amplitude amplification algorithm can be applied to unstructured search for satisfying variable assignments.
The Quantum Approximate Optimization Algorithm (QAOA) is a promising candidate for solving 3SAT for Noisy Intermediate-Scale Quantum devices.
We introduce amplitude amplification-inspired variants of QAOA to improve the success probability for 3SAT.
arXiv Detail & Related papers (2023-03-02T11:52:39Z) - W2SAT: Learning to generate SAT instances from Weighted Literal
Incidence Graphs [13.173307471333619]
W2SAT is a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances.
We introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability.
Decoding from WLIG into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method.
arXiv Detail & Related papers (2023-02-01T06:30:41Z) - 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) - 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) - 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) - 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) - On Computation Complexity of True Proof Number Search [19.376328966299322]
We show that the computation of true emphproof and emphdisproof numbers for proof number search in arbitrary directed acyclic graphs is NP-hard.
The proof requires a reduction from SAT, which demonstrates that finding true proof/disproof number for arbitrary DAG is at least as hard as deciding if arbitrary SAT instance is satisfiable.
arXiv Detail & Related papers (2021-02-08T06:06:54Z)
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.