51
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 ...
37
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 ...
34
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 ...
31
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 $...
30
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.
27
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 ...
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.
24
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 ...
22
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 ...
22
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 ...
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 ...
18
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 for random instances (such as https://www.gableske.net/dimetheus) are based on the statistical physics methods (belief propagation etc.) I believe, whereas the ...
18
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 ...
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
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. ...
17
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 or easiness of solving certain formulas by CDCL solvers with resolution proof complexity measures, in particular resolution proof space. The results are ...
17
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 treewidth then we can decide the SAT formula in P, actually we can do much more. Your incident graph is very restricted. E.g it is a bounded pathwidth graph, so it ...
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 ...
15
It is worth noting that the problem becomes NP-hard when the restriction is relaxed slightly.
With a fixed number of clauses that are also of bounded size, the average number of literals in a clause is as close to 2 as one wants, by considering an instance with enough variables. As you point out, there is then a simple upper bound which is polynomial if ...
14
You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them.
I do not know of a tool that solves your problem because people add these algorithms on top of existing SAT solvers but rarely seem to release these extensions. Two papers that should help you in ...
14
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/~rrwill/thesis.pdf
I don't know of another exact algorithm for the problem that improves over exhaustive search on all instances. For sparse instances (with $O(n)...
14
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 all possible assignments for the variable vertices on the separator, and all variables mentioned in clauses in the separator (assuming each clause has a ...
Only top voted, non community-wiki answers of a minimum length are eligible
