Grande Salle de VERIMAG
16 mars 2011 - 15h30
Clause Manipulation for Faster Satisfiability
par Fabio Somenzi de University of Colorado in Boulder
Abstract: Propositional Satisfiability solvers used in verification are mostly
based on backtracking search and read formulae in Conjunctive Normal
Form. Which formula is chosen to represent a function has great
impact on solution time. Therefore, various techniques have been
devised to either preprocess the input formula or modify it
during the search. In this talk, we review existing techniques and
describe new ones. We characterize these techniques with respect to
two criteria, deductive power and proof conciseness, and present
experiments aimed at evaluating the clause manipulation techniques as
well as the criteria.
Joint work with Hyojung Han and HoonSang Jin.
