Patent ID: 7577625
Filing Date: 2009-08-18
Classification: G06N

Abstract:
1. A computer-readable medium comprising computer-executable instructions for determining satisfiability of a Quantified Boolean Formula (QBF) formula comprising: finding a Conjunctive Normal Form (CNF) formula which is equi-satisfiable to the QBF formula; finding a Disjunctive Normal Form (DNF) formula which is equi-tautological to the QBF formula; finding an assignment of values to variables of the CNF and DNF formulas which either causes a clause of the CNF formula to be conflict or which causes a cube of the DNF formula to be satisfied; performing a satisfiability determination comprising determining that the QBF formula is unsatisfiable if an assignment of values is found which causes a cube of the DNF formula to be satisfied; and performing a task comprising model checking, program verification, sequential circuit verification or artificial intelligence planning in accordance with the satisfiability determination.