Measuring Complexity of Boolean Satisfiability Problem

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?

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.

StackExchange Computer Science Q#63539, answer score: 7