Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
A. Rebola Pardo, G. Weissenbacher:
"RAT Elimination";
Vortrag: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR),
Alicante, Spain;
22.05.2020
- 27.05.2020; in: "Logic for Programming, Artificial Intelligence and Reasoning",
L. Kovacs, E. Albert (Hrg.);
EasyChair,
73
(2020),
S. 423
- 448.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.29007/fccb
Elektronische Version der Publikation:
https://publik.tuwien.ac.at/files/publik_293387.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.