3
$\begingroup$

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?

$\endgroup$
  • $\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$ – adrianN Sep 16 '16 at 16:46
  • 3
    $\begingroup$ Complexity should be measured in terms of both the number of variables and the number of clauses. $\endgroup$ – Yuval Filmus Sep 16 '16 at 22:42
5
$\begingroup$

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.

$\endgroup$
  • $\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$ – Drew McGowen Sep 16 '16 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$ – Mario Cervera Sep 16 '16 at 18:37
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.