Speaker: Benjamin Kiesl, Vienna University of Technology

Title: Local Redundancy in SAT: Generalizations of Blocked Clauses

Abstract:

Clause-elimination procedures that simplify formulas in conjunctive
normal form play an important role in modern SAT solving. Before or
during the actual solving process, such procedures identify and remove
clauses that are irrelevant to the solving result. These simplifications
usually rely on so-called redundancy criteria that characterize cases in
which the removal of a clause does not affect the satisfiability status
of a formula. A particularly successful redundancy criterion is that of
blocked clauses, because it generalizes several other redundancy
notions. To find out whether a clause is blocked---and therefore
redundant---one only needs to consider its resolution environment, i.e.,
the clauses with which it can be resolved.  For this reason, the
redundancy criterion of blocked clauses is said to be local. In my talk,
I show that there exist local redundancy criteria that are even more
general than blocked clauses. To this end, I present a semantic notion
of blocking and illustrate that it constitutes the most general local
redundancy criterion. I furthermore introduce the syntax-based notions
of set-blocking and super-blocking, the latter of which coincides with
the afore-mentioned semantic blocking notion. I also give some
complexity results for checking the local redundancy criteria and relate
them to prominent redundancy criteria from the literature.