Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
A. Shukla, F. Slivovsky, S. Szeider:
"Short Q-Resolution Proofswith Homomorphisms";
Vortrag: SAT 2020 - 23rd International Conference on Theory and Applications of Satisfiability Testing,
Alghero, Italy;
03.07.2020
- 10.07.2020; in: "Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing",
LNCS,
12178
(2020),
ISBN: 978-3-030-51824-0;
S. 412
- 428.
Kurzfassung englisch:
We introduce new proof systems for quantified Boolean
formulas (QBFs) by enhancing Q-resolution systems with rules which
exploit local and global symmetries. The rules are based on homomorphisms
that admit non-injective mappings between literals. This results
in systems that are stronger than Q-resolution with (injective) symmetry
rules. We further strengthen the systems by utilizing a dependency
system D in a way that surpasses Q(D)-resolution in relative strength
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-51825-7_29
Elektronische Version der Publikation:
https://publik.tuwien.ac.at/files/publik_293460.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.