Institut für Informatik   Abteilung V

 Universität Bonn -> Institut für Informatik -> Abteilung V CS-Reports 1990 Copyright 1990 Universität Bonn, Institut für Informatik, Abt. V 8555 A Resolution Method for Quantified Boolean Formulas Marek Karpinski, Hans Kleine-Buening [Download PostScript] [Download PDF] A complete and sound resolution operation directly applicable to quantified boolean formulas is presented. If we restrict the resolution to unit resolution, then the completeness and soundness for extended quantified Horn formulas is shown. We prove that the truth of a quantified Horn formula can be decided in \$O(rn)\$ time, where \$n\$ is the length of the Formula and \$r\$ is the number of universal variables, whereas in contrast the evaluation problem for extended quantified Horn formulas is coNP-complete for formulas with prefix \$\forall \, \exists\$. Further we show that the resolution is exponential for extended quantified Horn formulas. Last Change: 08/18/99 at 13:00:38  English Universität Bonn -> Institut für Informatik -> Abteilung V