Handling of satisfaction and conflicts in a quantified Boolean formula solver
View Patent ↗In order to provide for more efficient QBF satisfiability determination, the formula to be checked is transformed into one formula which is equi-satisfiable, and one which is equi-tautological. The conjunction or disjunction of these two formulas, then, is used to determine satisfiability, with the result being that a determination of satisfiability is more easily achieved. A conjunctive normal form transformation of the initial formula yields a group of clauses, only one of which must be unsatisfiable for the formula to be unsatisfiable. A disjunctive normal form transformation of the initial formula yields a group of cubes, only one of which must be satisfiable in order for the formula to be determined to be satisfiable.
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.
2. The computer-readable medium of claim 1 wherein the computer executable instructions further comprise determining that the QBF formula is satisfiable if an assignment is found which causes a clause of the CNF formula to be conflict.
3. A method 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.
4. The method of claim 3 further comprising determining that the QBF formula is satisfiable if an assignment is found which causes a clause of the CNF formula to be conflict.
5. A system for satisfying a Quantified Boolean Formula (QBF) formula comprising:
a processor operative to execute computer-executable instructions; and
memory having stored therein computer-executable instructions 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.
6. The system of claim 5 wherein the computer executable instructions further comprise determining that the QBF formula is satisfiable if an assignment is found which causes a clause of the CNF formula to be conflict.