Description
Speaker: Katalin Fazekas (Johannes Kepler University Linz)
Title: Incremental Inprocessing in SAT Solving
Abstract:
In many applications, such as model checking or planning, one needs to decide the satisfiability of not just a single formula, but rather a sequence of formulas, where each problem is an extension or slight modification of the previously solved one. Incremental SAT solvers provide an efficient way to solve these formulas by being suited to reuse parts of previous evaluations and thereby avoiding repeated work. However, some of the employed inprocessing (i.e. formula simplifications before and during the CDCL search) techniques of modern SAT solvers are not necessarily sound to be used within incremental reasoning.
In this talk, I will give a short overview of the challenges regarding inprocessing during incremental SAT solving and will present briefly our proposed approach to efficiently address some of these challenges.