Backdoors To Typical Case Complexity

Backdoors To Typical Case Complexity Ryan Williams, Carla P. Gomes, and Bart Selman IJCAI'03

SAT solvers frequently perform much better on real-world problems than would be predicted by a worst-case analysis. This paper provides a clue as to why some problems are tractable and presents algorithms to solve such problems.

The analysis here applies equally to SAT problems and CSP problems.

This quote sums up the motivating idea behind the paper (all variables are not created equal):

Another powerful intuition in the design of search methods is that one wants to select variables that simplify the problem instance as much as possible when these variables are assigned values.

A backdoor is a subset of the variables in a SAT/CSP problem. There exists at least one assignment of backdoor variables to values such that the values of the remaining variables can easily be found by a sub-solver. A sub-solver is a SAT/CSP solver which runs in polynomial time and can solve a subset of SAT/CSP problems. The input to the sub-solver is a SAT/CSP problem, along with a partial assignment. A partial assignment assigns concrete values to some variables (e.g., the backdoor variables).

When we say that a sub-solver “solves” a problem, we mean that it returns one of:

1. A mapping of variable names to values which satisfies all constraints

2. “Unsatisfiable” - the constraints cannot all be satisfied

3. “Too hard” - the problem is not one of the kinds that the sub-solver can handle

An example sub-solver for SAT problems is one that can only solve 2-SAT problems.

Table 2 contains backdoor sizes from real-world SAT problems:

Think about that for a second. The first row means that in a problem with 6783 variables, the crux of the issue can be solved by only considering 12 variables. So rather than searching for a needle in a haystack of size 2⁶⁷⁸³, one only needs to find the correct values for the 12 variables in the backdoor (2¹² options to explore). Once that assignment has been found, the sub-solver can find the values of the other 6771 variables.

The only trouble is how one finds a backdoor.

The deterministic strategy optimistically assumes there exists a small backdoor. First it assumes the backdoor contains 1 variable. If that fails, then the strategy assumes the backdoor contains 2 variables, and so on.

At step N, the deterministic strategy enumerates all possible backdoors of size N. For each candidate backdoor, it uses a backtracking search (which will invoke a sub-solver) to try to solve the problem. Backtracking search is more efficient than exhaustively searching all 2^N variable assignments because this search can invoke the sub-solver with a partial assignment of fewer than N variables, in the hopes that the sub-solver can fail quickly.

The randomized strategy is similar to the deterministic strategy, but it chooses random subsets of variables to perform a backtracking search on. Again, the process begins with a bias that the size of the backdoor is small and gradually increases the expected size of the random subset.

The key question running through my mind is: “are there ways to transform SAT problems such that the output of the transformation has a smaller backdoor than the input”?