Toni Jussila, Carsten Sinz, Armin Biere,
"Extended Resolution Proofs for Symbolic SAT Solving with Quantification"
: Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06), Serie Lecture Notes in Computer Science (LNCS), Vol. 4121, Springer, Seite(n) 54-60, 2006, ISBN: 978-3-540-37206-6
Original Titel:
Extended Resolution Proofs for Symbolic SAT Solving with Quantification
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 9th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'06)
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-