Talks and Poster Presentations (with Proceedings-Entry):
A. Rebola Pardo, G. Weissenbacher:
Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
- 2020-05-27; in: "Logic for Programming, Artificial Intelligence and Reasoning",
L. Kovacs, E. Albert (ed.);
Inprocessing techniques have become one of the most promising advancements in SAT solving over the last decade. Some inprocessing techniques modify a propositional formula in non model-perserving ways. These operations are very problematic when Craig inter- polants must be extracted: existing methods take resolution proofs as an input, but these inferences require stronger proof systems; state-of-the-art solvers generate DRAT proofs. We present the first method to transform DRAT proofs into resolution-like proofs by eliminating satisfiability-preserving RAT inferences. This solves the problem of extracting interpolants from DRAT proofs.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.