Talks and Poster Presentations (with Proceedings-Entry):
A. Shukla, F. Slivovsky, S. Szeider:
"Short Q-Resolution Proofswith Homomorphisms";
Talk: SAT 2020 - 23rd International Conference on Theory and Applications of Satisfiability Testing,
Alghero, Italy;
2020-07-03
- 2020-07-10; in: "Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing",
LNCS,
12178
(2020),
ISBN: 978-3-030-51824-0;
412
- 428.
English abstract:
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
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-51825-7_29
Electronic version of the publication:
https://publik.tuwien.ac.at/files/publik_293460.pdf
Created from the Publication Database of the Vienna University of Technology.