[Back]


Publications in Scientific Journals:

F. Slivovsky, S. Szeider:
"Quantifier Reordering for QBF";
Journal of Automated Reasoning, Volume 55 (2015), 1 - 19.



English abstract:
State-of-the-art procedures for evaluating quantified Boolean formulas often
expect input formulas in prenex conjunctive normal form (PCNF). We study dependency
schemes as a means of reordering the quantifier prefix of a PCNF formula while preserving
its truth value. Dependency schemes associate each formula with a binary relation on its variables
(the dependency relation) that imposes constraints on certain operations manipulating
the formula´s quantifier prefix.We prove that known dependency schemes support a stronger
reordering operation than was previously known. We present an algorithm that, given a formula
and its dependency relation, computes a compatible reordering with aminimum number
of quantifier alternations. In combination with a dependency scheme that can be computed in
polynomial time, this yields a polynomial time heuristic for reducing the number of quantifier
alternations of an input formula. The resolution-path dependency scheme is the most general
dependency scheme introduced so far. Using an interpretation of resolution paths as directed
paths in a formula´s implication graph, we prove that the resolution-path dependency relation
can be computed in polynomial time.


"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/s10817-015-9353-1

Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_247778.pdf


Created from the Publication Database of the Vienna University of Technology.