How exactly is the complexity of a SAT solver measured? My main concern is that, for $N$ variables, you can have, e.g., an OR of $O(2^N)$ AND terms, which would take at least $O(2^N)$ time to process. If the formula can contain duplicate sub-expressions, e.g., $(A \land B) \lor (A \land B)$, then the formula's maximum size is unbounded. In this case, wouldn't the complexity be better measured in terms of how complex the formula is, rather than how many variables it takes?
$\begingroup$
$\endgroup$
2
-
$\begingroup$ If you want to be very precise about runtimes you take the bit size of some reasonably efficient encoding for your problem instance (regardless of which problem you're looking at). That accounts for both number of variables and formula complexity in the case of SAT. $\endgroup$– adrianNSep 16, 2016 at 16:46
-
4$\begingroup$ Complexity should be measured in terms of both the number of variables and the number of clauses. $\endgroup$– Yuval FilmusSep 16, 2016 at 22:42
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
2
The boolean satisfiability problem (SAT) involves finding a satisfying truth assignment for a set of clauses $C$ over the boolean variables $V=\{v_1, v_2, ..., v_n\}$ so that each clause in $C$ contains at least one true literal. Since $V$ contains $n$ variables and each of these variables can only have $2$ different values (i.e., true or false), the total number of possibilities to be tested is $2^n$. We don't know how to solve SAT in polynomial time (since SAT is NP-complete); therefore, all solvers take exponential time in the worst case. Fortunately, however, there exist several ways to prune the search space.
Wouldn't the complexity be better measured in terms of how complex the formula is?
The importance of the SAT problem lies in that every decision problem in NP can be reduced to SAT for CNF formulas. Other restricted versions of SAT exist (such as 3-SAT, Horn-SAT, and XOR-SAT); these restricted versions can be either in P or NP depending on the restriction (see Schaefer's dichotomy theorem). Regardless of this, note that problems in NP (such as SAT) are characterized by solutions (in the case of SAT, truth assignments) that can be verified in polynomial time.
answered Sep 16, 2016 at 17:24
-
$\begingroup$ My concern is about input formulas that aren't in CNF, i.e.
A and (B xor C). While there are $2^N$ possibilities to test, each possibility could take any arbitrary amount of time to compute, possibly making the brute-force runtime larger than $O(2^N)$ (like maybe even $O(2^{2^N})$). $\endgroup$ Sep 16, 2016 at 17:31 -
$\begingroup$ The SAT problem is particularly important because every decision problem in NP can be reduced to SAT for CNF formulas. Other restricted versions exist (e.g., 3-SAT, Horn-SAT, etc.). Depending on the restriction, the problem can be in P or in NP (see Schaefer's dichotomy theorem). Nonetheless, note that problems in NP are characterized by solutions (in the case of SAT, truth assignments) that can be verified in polynomial time. $\endgroup$ Sep 16, 2016 at 18:37
$\begingroup$
$\endgroup$
I think you have a misconception. SAT by definition accepts formulas in CNF form, and only in CNF form. Moreover, in practice, SAT solvers all use CNF form.
(You might find some tools that have a front-end/preprocessor that will convert a formula in some other format into CNF form then feed it to a SAT solver.)
The complexity of a SAT solver isn't measured. We know that in the worst case they can take exponential time, so we don't worry about trying to characterize their asymptotic running time via theory. Instead, think of SAT solvers as a heuristic: in the worst case they could take an extremely long time, but on real-world formula seen in practice, they often run much faster than that.
$\begingroup$
$\endgroup$
There are problems for which there is no reduction to SAT that is of P complexity. Those problems may or may not be solved by computations that can be performed in O(2^n) or less time and space. SAT is always worst case O(2^n) or less by definition.
SAT has a P complexity solution. See arxiv.org/abs/cs/0205064.
