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.
CITATION STYLE
Shukla, A., Slivovsky, F., & Szeider, S. (2020). Short Q-Resolution Proofs with Homomorphisms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12178 LNCS, pp. 412–428). Springer. https://doi.org/10.1007/978-3-030-51825-7_29
Mendeley helps you to discover research relevant for your work.