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 affect 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 difficult to derive within a Resolution-based SAT-solver. Such encodings can be used as polytime preprocessing to speed up SAT algorithms. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Hertel, A., Hertel, P., & Urquhart, A. (2007). Formalizing dangerous SAT encodings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4501 LNCS, pp. 159–172). Springer Verlag. https://doi.org/10.1007/978-3-540-72788-0_18
Mendeley helps you to discover research relevant for your work.