# Tag Info

### Do any quantum algorithms improve on classical SAT?

Indeed, as wwjohnsmith1 said, you can get a square root speed-up over Schöning's algorithm for 3-SAT, but also more generally for Schöning's algorithm for k-SAT. In fact, many randomized algorithms ...
• 13.7k
Accepted

### Do any quantum algorithms improve on classical SAT?

I think one can obtain a non-trivial upper bound from quantum computing by speeding up the randomized algorithms of Schöning for 3-SAT. The algorithm of Schöning runs in time $(4/3)^n$ and ...
• 326

### Are there any hard instances of 3-SAT when the clauses can only use literals that are "nearby" each other?

No. If the 3-SAT instance has $m$ clauses, then you can test satisfiability in $O(m 2^N)$ time. Since $N$ is a fixed constant, this is a polynomial-time algorithm that solves all instances of your ...
• 12.1k

### Theoretical explanations for practical success of SAT solvers?

I am assuming that you are referring to CDCL SAT solvers on benchmark data sets like those used in the SAT Competition. These programs are based on many heuristics and lots of optimization. There were ...
• 21.7k

### Theoretical explanations for practical success of SAT solvers?

I am typing this quite quickly due to severe time constraints (and didn't even get to responding earlier for the same reason), but I thought I would try to at least chip in with my two cents. I ...
Accepted

### Algebraic equivalent of SAT?

This is standard and widely used in computer science theory. There are many references that use boolean polynomials with False -> 0 and True -> 1, or in other words, a polynomial over GF(2) used ...
• 12.1k
Accepted

### Counting the number of satisfying assignments in a POSITIVE CNF-SAT

This is still #P-complete [1]. This problem is usually referred to as montone (#)SAT. Monotone #2-SAT is already #P-complete (this is equivalent to counting vertex covers of a graph). [1] Roth, Dan. "...
• 2,174

### Theoretical explanations for practical success of SAT solvers?

I'm not an expert in this area, but I think the random SAT / phase transition stuff is more or less completely unrelated to the industrial/practical applications stuff. E.g., the very good solvers ...
• 1,811

### Theoretical explanations for practical success of SAT solvers?

Let me add my two cents of understanding to this, even though I've never actually worked in the area. You're asking one of two questions, "what are all the known approaches to proving theoretical ...

### Theoretical explanations for practical success of SAT solvers?

There is a paper "Relating Proof Complexity Measures and Practical Hardness of SAT" by Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný in CP '12 that attempts to link the hardness ...
• 4,630

### Are there any hard instances of 3-SAT when the clauses can only use literals that are "nearby" each other?

Incident graph of a SAT formula is a bipartite graph that has a vertex for each clause and each variable. We add edges between a clause and all of its variables. If the incident graph has bounded ...
• 3,440
Accepted

### On theoretical aproaches for solving $\mathsf{SAT}$ in special cases

Concerning Question 1, there have mainly been two lines of work to find tractable restrictions of SAT. The first one that you are already familiar with is to restrict the types of the clauses that ...
• 2,174

### Counting the number of satisfying assignments in a POSITIVE CNF-SAT

This problem is Monotone-SAT. It is #P-Complete under Cook Reductions. It is one of those problems that are "easy to decide but hard to count." I recommend the following paper. Self-Reducibility of ...
• 2,598
Accepted

### Is there a SETH (Strong Exponential Time Hypothesis) for CSP (Constraint Satisfaction Problem)?

This CSP is known to be SETH-hard. More precisely, assuming SETH, for any constant $\varepsilon > 0$ there is no $d^{(1-\varepsilon)n}$-time algorithm for solving this CSP with domain size $d$. ...
• 4,878

### Questions regarding SETH

The subtlety comes in where we introduce the notion of "harder". The reduction showing that SAT can be reduced to Hamiltonian Cycle shows that the latter is "harder" up to polynomial factors. In doing ...
• 1,642
Accepted

### Best Upper Bounds on SAT

The best algorithm for 3-SAT now has numerical upper bound $O^{*}(1.306995^n)$ on unique-3-SAT and on general-3-SAT it is also fastest but now the specific values have not been analyzed yet. Authors ...
• 490
Accepted

### What is the complexity of checking equivalence of two boolean formulae without NOT symbol?

Note that formulas using $\land$ and $\lor$ gates (and possibly the constants $0$ and $1$) are known as monotone. The complexity of monotone formula equivalence depends on how complex formulas are ...
• 17.6k
Accepted

### Complexity of 1-or-3-in-3-SAT (odd-3-SAT)

Somewhat surprisingly to me, this problem is in fact in PTIME. The key insight is that, considering a clause $C$, letting $0 \leq k \leq 3$ be the number of negated literals in $C$, then the clause is ...
• 9,409

### Is this variation of TQBF still PSPACE-complete?

We proved that this game is PSPACE-complete for 5-CNFs but has Linear Time algorithm for 2-CNFs. The previous best result was Ahlroth and Orponen's 6-CNFs. You can find the conference paper at ISAAC ...
Accepted

### What are the consequences of solving XOR 3-SAT in Logspace?

Take a look at https://www.sciencedirect.com/science/article/pii/S0022000008001141 "The complexity of satisfiability problems: Refining Schaefer's theorem" by Allender et al. which answer your ...
• 1,047

### Algebraic equivalent of SAT?

I think what you are asking about is also known as "polynomial calculus" in proof complexity and SAT solving. It was introduced in [1, 2] to investigate whether coNP can be separated from NP ...
• 11.5k

### On reducing the hardness of CNF-SAT to k-Clique

I don't know the answer to your specific question (it seems related to the question of whether W1=W[2]). But the algorithm you give in your question is subsumed by several other results. Using your ...
• 27.5k
Accepted

### Random 3-SAT: What is the consensus experimental range of the threshold?

In light of the Ding--Sly--Sun verification of the 1-step Replica Symmetry Breaking picture for kSAT (when k is large enough) I think experts would now be pretty surprised if the MPZ/MMZ-conjectured ...
• 1,811
Accepted

### Is bounded-width SAT decidable in logspace?

Indeed, using the resultss in Elberfeld-Jakoby-Tantau-2010 one can show that SAT can be decided in logspace on formulas whose incidence graph has bounded treewidth. Here is a sketch of how the main ...
Accepted

### Sparsification Lemma for k-SAT and Exponential Time Hypothesis

I think your confusion might come from misquoting the statement of ETH. $3$-SAT instances (with $n$ variables and $m$ clauses) cannot be solved in time $poly(n)\cdot 2^{o(n)}$. This statement is ...
• 2,247

### Complexity of 3SAT where each pair of 3-clauses share at most one variable

The central insight is that you can use two $2$-variable clauses to make sure two variables have the same value. Let me abbreviate $(x \vee \neg y) \wedge (y \vee \neg x)$ with $x=y$. This allows the ...
• 1,969

### Verifying a subtlety of Karp's original proof that SAT has a polynomial time reduction to 3SAT

The conjunction of the first two clauses, $(\sigma_1\cup\sigma_2\cup u_1)(\sigma_3\cup\ldots\cup\sigma_m\cup\bar{u}_1)$ is equisatisfiable to the original clause, as can be easily checked (any ...
• 2,520
Accepted

### a polynomial representation of boolean functions

Well done on your independent discovery. This is a Hadamard matrix of Sylvester type, written in a different order. There is a massive literature on this topic. It is used in coding theory, ...
• 2,070
Accepted

Just an alternative proof using a mix of well known results. Suppose that: variables are expressed with the regular expression $d = (+|-)1(0|1)^*$ and that the (regular) language (over $\Sigma = \{0,... 8 votes Accepted ### Reference request: complexity of$k$-partite$k$-SAT Claim: If there exists an$\epsilon > 0$such that for every$k'$,$k'$-partite$k'$-SAT can be solved in$2^{n(1-\epsilon)}\$ time, then SETH fails. Proof: Suppose such an algorithm exists. We ...
• 3,266

Only top scored, non community-wiki answers of a minimum length are eligible