52
votes
Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming
SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems.
However, they come at these problems from different angles and with different toolboxes.
These ...
- 18.7k
38
votes
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.3k
37
votes
Accepted
Is this variation of TQBF still PSPACE-complete?
It is an Unordered Constraint Satisfaction game and it is PSPACE-complete and it has been proved to be PSPACE-complete only recently;
a proof can be found in:
Lauri Ahlroth and Pekka Orponen, ...
- 22.3k
31
votes
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 ...
- 10.4k
30
votes
Is this variation of TQBF still PSPACE-complete?
It may also be worthwhile to note that this problem was also solved in the 70's by Thomas Schaefer in Complexity of decision problems based on finite two-person perfect-information games. In fact, ...
- 541
30
votes
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 ...
- 316
27
votes
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.3k
26
votes
Accepted
Is there an oracle such that SAT is not infinitely often in sub-exponential time?
You can just take the oracle A s.t. NP$^A$=EXP$^A$ since EXP is not in i.o.-subexp. For SAT$^A$ it depends on the encoding, for example if the only valid SAT instances have even length then it is easy ...
- 8,546
22
votes
Accepted
How is the MA version of SETH proven to be false?
You can find a preprint by following this link http://eccc.hpi-web.de/report/2016/002/
EDIT (1/24) By request, here is a quick summary, taken from the paper itself, but glossing over many things. ...
- 26.4k
22
votes
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 ...
- 484
20
votes
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. "...
- 1,855
19
votes
Accepted
Properties expressible in 2-CNF or 2-SAT
A family of bitvectors is the class of solutions to a 2-SAT problem if and only if it has the median property: if you apply the bitwise majority function to any three solutions you get another ...
- 50.2k
18
votes
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,781
18
votes
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 ...
- 803
17
votes
Accepted
MAX 1 in 2 SAT Algorithm
A monotone 1-in-2 clause demands that the two variables have different values. Thus, you can model the problem as a graph problem, with one vertex per variable which is to be colored black or white, ...
- 1,023
17
votes
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,501
17
votes
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,420
16
votes
Is there an oracle such that SAT is not infinitely often in sub-exponential time?
You don't have to go to the lengths Lance was suggesting. For
example, relative to a random oracle, using the oracle as a one-way function
(say, evaluated on consecutive bit postions)
is ...
- 1,321
16
votes
Accepted
Complexity of the search version of 2-SAT assuming $\mathsf{L = NL}$
Given a satisfiable 2-CNF $\phi$, you can compute a particular satisfying assignment $e$ by an NL-function (that is, there is an NL-predicate $P(\phi,i)$ that tells you whether $e(x_i)$ is true). One ...
- 14.8k
15
votes
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,579
14
votes
MAX 1 in 2 SAT Algorithm
An exact algorithm for the Max Monotone 1 in 2 Sat problem (i.e., MaxCut) running faster than $2^n$ (about $O(1.8^n)$ time) can be found in Chapter 6 of my PhD thesis, here: http://web.stanford.edu/~...
- 26.4k
14
votes
Accepted
Are there subexponential algorithms for PLANAR SAT known?
Well, you can apply the planar separator theorem together with dynamic programming and get running time $2^{O(\sqrt{n})}$, where $n$ is the number of vertices in the graph. The idea being that you try ...
- 9,556
14
votes
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,624
14
votes
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 ...
- 1,855
13
votes
Accepted
Translation of context-free parsing into SAT
(I guess the important word in the original question is ``published''.) There is such an encoding of context-free parsing (more exactly of CYK-style parsing) in Roland Axelsson, Keijo Heljanko, and ...
- 3,324
13
votes
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,027
13
votes
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 ...
- 14.8k
12
votes
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 ...
- 470
12
votes
Accepted
Approximating #P-hard problems
We're interested in additive approximations to #3SAT. i.e. given a 3CNF $\phi$ on $n$ variables count the number of satisfying assignments (call this $a$) up to additive error $k$.
Here are some ...
- 2,743
12
votes
Definition of Planar 3-SAT
There's a nice compilation of definitions of related NP-complete planar satisfiability problems at http://courses.csail.mit.edu/6.890/fall14/scribe/lec7.pdf
One of them, planar monotone 3-sat, allows ...
- 50.2k
Only top scored, non community-wiki answers of a minimum length are eligible