46
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 ...
33
Yes, there is a major difference between MiniSAT and WalkSAT. First, let's clarify - MiniSAT is a specific implementation of the generic class of DPLL/CDCL algorithms which use backtracking and clause learning, whereas WalkSAT is the general name for an algorithm which alternates between greedy steps and random steps.
In general DPLL/CDCL is much faster on ...
30
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
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
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 ...
28
Each SAT clause has 1, 2, 3 or more variables. The 3 variable clause can be copied with no issue
The 1 and 2 variable clauses {a1} and {a1,a2} can be expanded to {a1,a1,a1} and {a1,a2,a1} respectively.
The clause with more than 3 variables {a1,a2,a3,a4,a5} can be expanded to {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5} with s1 and s2 new variables whose value will ...
28
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
This is probably beyond the scope of the question, but I wanted to post it anyway. Using techniques from parameterized complexity it has been proven that, assuming the polynomial hierarchy doesn't collapse to its third level, there is no polynomial-time algorithm which takes an instance of CNF-SAT on n variables with unbounded clause length, and outputs an ...
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 ...
22
At least two of the literals $x$, $y$, $z$ are satisfied iff at least one literal in each pair $(x,y)$, $(x,z)$, $(y,z)$ is satisfied. Therefore it is a special case of 2SAT, and there is a polynomial-time algorithm for solving it.
21
What you are doing is deriving a topological representation of a Boolean algebra. The study of representations of Boolean algebras goes back at least to Lindenbaum and Tarski who proved (in 1925, I think) that the complete, atomic Boolean algebras are isomorphic to powerset lattices.
There are however, Boolean algebras that are not complete and atomic. For ...
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 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 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
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 ...
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
If you need a reduction from k-SAT to 3-SAT, then ratchet's answer works fine.
If you want a direct reduction from generic propositional formula to CNF (and to 3-SAT) then - at least from the "SAT solvers perspective" - I think that the answer to your question What is the 'most natural' reduction ...?, is: There is no 'natural' reduction!.
From the ...
19
If SAT had a subexpoential-time algorithm, the you would disprove the exponential time hypothesis.
For fun cosequences: 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$.
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
An excellent beginner overview is given by the following article from 2009.
Boolean Satisfiability: From Theoretical Hardness to Practical Success, Sharad Malik, Lintao Zhang, Communications of the ACM, 2009
There are several ways to get into the technical aspects. You can even start with the original Davis-Putnam paper. It is extremely clear and has ...
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
I suggest first understanding which techniques really advanced the solvers, for which I would suggest the following overview and analysis.
Then I would recommend downloading the source code of minisat and read its description.
It might of course be individual but I found looking at the source code most valuable.
17
There is an enormous difference between sat instances. SAT solver $A$ might perform well on the class $X$ of instances, but poorly on the class $Y$ of instances, while solver $B$ performs well on class $Y$ and poorly on class $X$.
A good paper to read on this topic is this one by Nudelman et al. The whole point of the paper is to determine easy-to-compute ...
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
Only top voted, non community-wiki answers of a minimum length are eligible
