Extended Resolution Proofs for Symbolic SAT Solving with Quantification
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06)
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Symbolic SAT solving is an approach where the clauses of a CNF formula are
represented using BDDs. These BDDs are then conjoined, and finally checking satisfiability
is reduced to the question of whether the final BDD is identical to false. We present a
method combining symbolic SAT solving with BDD quantification (variable elimination)
and generation of extended resolution proofs. Proofs are fundamental to many applications,
and our results allow the use of BDDs instead of—or in combination with—established
proof generation techniques like clause learning. We have implemented a symbolic SAT
solver with variable elimination that produces extended resolution proofs. We present details
of our implementation, called EBDDRES, which is an extension of the system presented
in [1], and also report on experimental results.
Forschungs-