Preprocessing of CNF formulas is an invaluable technique when attempting to solve large formulas, such as those that model industrial verification problems. Unfortunately, the best combination of preprocessing techniques, which involve variable elimination combined with subsumption, is incompatible with incremental satisfiability. The reason is that soundness is lost if a variable is eliminated and later reintroduced. Look-ahead is a known technique to solve this problem, which simply blocks elimination of variables that are expected to be part of future instances. The problem with this technique is that it relies on knowing the future instances, which is impossible in several prominent domains. We show a technique for this realm, which is empirically far better than the known alternatives: running without preprocessing at all or applying preprocessing separately at each step. © 2012 Springer-Verlag.
CITATION STYLE
Nadel, A., Ryvchin, V., & Strichman, O. (2012). Preprocessing in incremental SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 256–269). https://doi.org/10.1007/978-3-642-31612-8_20
Mendeley helps you to discover research relevant for your work.