Marijn Heule, Martina Seidl, Armin Biere,
"Efficient Extraction of Skolem Functions from QRAT Proofs"
: Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14), FMCAD Inc., Seite(n) 107-114, 2014
Original Titel:
Efficient Extraction of Skolem Functions from QRAT Proofs
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 14th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'14)
Original Kurzfassung:
Many synthesis problems can be solved by formulating
them as a quantified Boolean formula (QBF). For such
problems, a mere true/false answer is often not enough. Instead,
expressing the answer in terms of Skolem functions reflecting
the quantifier dependencies of the variables is required. Several
approaches have been presented to extract such functions from
term-resolution proofs. However, not all solvers and preprocessors
are able to produce term-resolution proofs, especially when
universal expansion is involved. In previous work, we developed
the QRAT proof system consisting of three simple rules which
allowed us to overcome this issue and to equip modern expansionbased
tools like the preprocessor bloqqer with proof tracing. In
this paper, we show how to extract Skolem functions from QRAT
proofs. We present a general extraction tool and compare its
performance to similar resolution-based tools. We show that the
Skolem functions extracted from QRAT proofs are smaller than
those produced by alternative approaches making our method in
particular useful for synthesis applications.