| 摘要 |
Existing satisfiability algorithms are improved by a modification to the problem representation that exploits the structure of naturally occurring problems. Common satisfiability algorithms include WSAT and RELSAT. Each of these algorithms performs, one or more times, a specific calculation, called "subsearch", where the algorithm searches through the original theory for ground clauses that satisfy some numeric property. For realistic problems, the time spent on subsearch can be expected to dominate the computational cost of the algorithm. The present invention represents subsearch in terms of S(C,P,us), the set of ground instances of C that have u literals unvalued by P and s literals satisfied by the assignments in P. This representation allows intelligent search to be performed to answer subsearch problems posed in terms of S(C,P,u,s). Intelligent subsearch uses truth value assignments to atoms to eliminate sets of bindings to universally quantified variables within a quantified clausal constraint; the bindings being eliminated because the bindings cannot satisfy a specific statement. In addition, it is possible to backtrack away from poor choices in the search for bindings to variables within the quantified clauses. In typical uses, intelligent subsearch can reduce the time of the checking problem from O(D<U>) to O(D< alpha U>) for some alpha <1.
|
