Formalizing Dangerous SAT Encodings

In this paper we prove an exponential separation between two very similar and natural SAT encodings for the same problem, thereby showing that researchers must be careful when designing encodings, lest they accidentally introduce complexity into the problem being studied. This result provides a formal explanation for empirical results showing that the encoding of a problem can dramatically aect its practical solvability. We also introduce a domain-independent framework for reasoning about the complexity added to SAT instances by their encodings. This includes the observation that while some encodings may add complexity, other encodings can actually make problems easier to solve by adding clauses which would otherwise be dicult to derive within a Resolution-based SAT-solver. Such encodings can be used as polytime preprocessing to speed up SAT algorithms.