Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called "Qresolution", is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs

• Type: Journal
• Year: 2006
• Where: JAIR
• Authors: Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella
• Keywords: Conjunctive Normal Form, JAIR 2006, Normal Form, Procedure