Faculty of Computer Science

Research Group Theoretical Computer Science

Oberseminar: Heterogene formale Methoden

Abstract:

The boolean satisfiability problem plays a significant role in theoretical computer science and application alike. While efficient solvers working for arbitrary instances don't exist (given P!=NP), there are still quite efficient algorithms, namely DPLL/CDCL based solvers and portfolio approaches, that are quite fast for certain types of formulas. Besides already efficient algorithms, solving time can also be reduced (in many cases) by employing some form of preprocessing, transforming the initial formula into one that is easier to solve, utilising its structure and/or higher level reasoning. This talk aims to summarise "Chapter 9: Preprocessing in SAT solving" of "Handbook of Satisfiability" (second edition), while taking a closer look at a selection of established/prominent preprocessing techniques: Unit Propagation, Pure Literal Elimination, Failed Literal Probing, Subsumption, Self-Subsuming Resolution, Bounded Variable Elimination, Equivalent Literal Substitution, Hyper Binary Resolution, Asymmetric-/Hidden Literal Elimination, Asymmetric-/Hidden Tautology Elimination(ATE), Distillation/Vivification(ATE variants), Blocked Clause Elimination, Resolution Asymmetric Tautologies, Covered Clause Elimination, Blocked Clause Decomposition.
For further reading, a freely available manuscript version of Chapter 9 can be found at https://fmv.jku.at/papers/BiereJarvisaloKiesl-SAT-Handbook-2021-Preprocessing-Chapter-Manuscript.pdf