Talks and Poster Presentations (with Proceedings-Entry):
A. Rebola Pardo, G. Weissenbacher:
"RAT Elimination";
Talk: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
Alicante, Spain;
2020-05-22
- 2020-05-27; in: "Logic for Programming, Artificial Intelligence and Reasoning",
L. Kovacs, E. Albert (ed.);
EasyChair,
73
(2020),
423
- 448.
English abstract:
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)
http://dx.doi.org/10.29007/fccb
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_293387.pdf
Created from the Publication Database of the Vienna University of Technology.