47
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 differences are largely in how each approach structures information about the exploration of the search space.
My working analogy is that SAT is machine code, while the ...
35
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, Unordered Constraint Satisfaction Games.
Lecture Notes in Computer Science Volume 7464, 2012, pp 64-75.
Abstract: We consider two-player constraint satisfaction ...
30
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 for k-SAT can be implemented quadratically faster on a quantum computer.
The reason for this general phenomenon is the following. Many randomized algorithms for ...
30
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 problem.
The algorithm works in $m$ stages. Let $\varphi_i$ denote the formula consisting of the clauses that use only variables from $x_1,\dots,x_i$. Let $...
29
The answer depends on $k$, $m$, and $n$. Exact counts are generally not known, but there is a "threshold" phenomenon that for most settings of $k$, $m$, $n$, either nearly all $k$-SAT instances are satisfiable, or nearly all instances are unsatisfiable. For example, when $k=3$, it has been empirically observed that when $m < 4.27 n$, all but a $o(1)$ ...
27
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, he proves a slightly stronger result in that the language remains PSPACE-complete even when restricted to positive CNF formulas.
26
Yes, there has been. Moshe Vardi recently gave a survey talk at BIRS Theoretical Foundations of Applied SAT Solving workshop:
Moshe Vardi, Phase transitions and computational complexity, 2014.
(Moshe presents the graph of their experiment a bit after minute 14:30 in his talk linked above.)
Let $\rho$ denote the clause ratio.
As the value of $\rho$ ...
26
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 to solve SAT on odd-length strings. But if you use a language like $L=\{\phi 01^*\ |\ \phi\in SAT^A\}$ then you should be fine.
23
You need to understand that $\mathsf{CSP}$ problems have a structure that generic $\mathbf{SAT}$ problems do not have. I will give you a simple example. Let $\Gamma=\{\{(0,0),(1,1)\},\{(0,1),(1,0)\}\}$. This language is such that you can only express equality and inequality between two variables. Clearly any such set of constraints is ...
21
Resolution Search (just applying the resolution rule with some good heuristics) is another possible strategy for SAT solvers. Theoretically it's exponentially more powerful (i.e. there exist problems for which it has exponential shorter proofs) than DPLL (which just does tree resolution though you can augment it with nogood learning to increase its power - ...
21
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. Suppose Merlin can prove to Arthur that for a $k$-variable arithmetic circuit $C$, its value on all points in $\{0,1\}^k$ is a certain table of $2^k$ field ...
21
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 using standard amplitude amplification techniques one can obtain a quantum algorithm that runs in time $(2/\sqrt{3})^n=1.15^n$ which is significantly faster than ...
21
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 some very good introductions to how they work at
Theoretical Foundations of Applied SAT Solving workshop at Banff in 2014
(videos).
These algorithms are based ...
20
This problem is the same as the Vertex Cover problem for $3$-uniform hypergraphs:
given a collection $H$ of subsets of $V$ of size $3$ each, find a minimal subset $U\subseteq V$ that intersects each set in $H$.
It is therefore NP-hard, but fixed parameter tractable.
It is also NP-hard to approximate to within a factor of $2-\epsilon$ for every $\epsilon&...
20
If SAT had a subexponential-time algorithm, the you would disprove the exponential time hypothesis.
For fun consequences: if you showed that circuit SAT over AND,OR,NOT with $n$ variables and $poly(n)$ circuit gates can be solved faster than the trivial $2^n poly(n)$ approach, then by Ryan Williams' paper you show that $NEXP \not\subseteq P/poly$.
20
If I may, quite blatantly, advertise myself, we wrote an article about this last year
Abstraction-Based Algorithm for 2QBF. I've got an implementation for qdimacs, which I can provide if you wish but from my experience, one can benefit greatly from specializing the algorithm for a particular problem. There is also an older paper A Comparative Study of 2QBF ...
20
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. "On the hardness of approximate reasoning." Artificial Intelligence 82.1-2 (1996): 273-302.
19
There are at least two lines of research concerning random $k\text-\mathsf{SAT}$ for formulas with a clause/variable-ratio larger than the satisfiability threshold:
For such formulas lower bounds on the length of refutations in resolution and stronger propositional proof systems have been shown, starting with the paper "Many hard examples for resolution" by ...
19
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 solution. See e.g. https://en.wikipedia.org/wiki/Median_graph#2-satisfiability and its references. So if you can find three solutions for which this is not true, then ...
18
SETH says that for all $\delta < 1$ there is a $k$ such that $k$-SAT requires $2^{\delta n}$ time to be solved in the worst-case. The computational model is generally taken to be the random-access machine or pointer machine model, which allows for $O(\log N)$ time access to a storage of $N$ items, and is generally assumed to also be probabilistic with ...
17
(Making comment an answer as requested and expanding a bit.)
"A curious mind" should read Schaefer's dichotomy theorem and the generalization by Allender et al. that shows that every possible SAT variant is either trivial or in one of six well-known complexity classes:
NP-complete
P-complete
NL-complete
L-complete
⊕L-complete
co-NLOGTIME
17
This list will be very long;)
Here are some of my favourite (NP-complete) variants of SAT:
PLANAR($\le 3, 3$)-SAT (each clause contains at least two and at most three literals, each variable appears in exactly three clauses;
twice in its non-negated form, and once in its negated form, and the bipartite incidence graph is planar.)
See: Dahlhaus, Johnson, ...
17
It is possible ;-)
It would give new circuit lower bounds. Since you are making a pretty strong assumption this could follow from the seminal work by Impagliazzo, Kabanets, and Wigderson, I haven't checked.
If you use Williams' approach, tightened here, you get a lower bound of $n^{1+\Omega(1)}$ for a function on $n$ bits in the class E$^{NP}$. (For this ...
17
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 think this is a truly great question, and have spent a nontrivial amount of time over the last few years looking into this. (Full disclosure: I have received a big ...
16
If what you are studying worked out, it definitely would not be trivial.
It would imply that 3SAT has (non-uniform) circuits of size $n^{O(\log n)}$. Then, every language in $NP$ (and the polynomial time hierarchy) would have quasi-polynomial (i.e., $n^{O(\log^c n)}$) size circuits.
Even if it took $2^{2^n}$ preprocessing time to produce a data structure ...
16
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, and an edge for a clause indicating the colors need to be different. Thus, the question is to make the graph bipartite by deleting a minimum number of edges. ...
16
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 exponentially hard to invert on all but finitely many lengths.
This problem directly reduces to SAT on the same length input, so it does
follow that SAT^A is not in ...
16
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 way to do that is described below. I will freely use the fact that NL is closed under $\mathrm{AC}^0$-reductions, hence NL-functions are closed under ...
answered Apr 5 '15 at 15:02
Emil Jeřábek supports Monica
10.9k3 gold badges40 silver badges63 bronze badges
16
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 efficiency of some SAT solver for some type of instances" and "why are SAT solvers efficient in reality".
For the former question, I'll just direct you to the ...
Only top voted, non community-wiki answers of a minimum length are eligible
