[Back]


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.