| In many logic programming applications, one must prove a large number of theorems of axioms specified by a given propositional logic formula in conjunctive normal form (CNF). When each such theorem is a CNF clause, as is typically the case, then each case becomes a SAT (satisfiability problem) instance that is derived from the given CNF formula by fixing some variables. Thus, the instances are closely related, and one should be able to learn how to solve them quickly. A related situation exists for the logic minimization problem MINSAT, where costs are associated with the assignment of True/False values, and where minimum-cost solutions have to be obtained. A problem instance is derived from a given CNF formula by fixing some of the variables. We have developed a solution algorithm for SAT and MINSAT and have implemented it in existing logic programming software called the Leibniz System. It is based on decomposition of the original instance and on backtracking search. A learning process, which is applied to classes of SAT and MINSAT, has been integrated into the compiler of the Leibniz System. We tested the solution algorithm and the learning process on a number of SAT and MINSAT cases. Learning leads to dramatic speedups of the measured worst-case run times. In many cases, we also obtained very low solution-time bounds after learning.; SAT and MINSAT are at the first level of the polynomial hierarchy. Some expert systems demand the solution of problems at higher levels of that hierarchy. We define three problems Q-ALL SAT, Q-MIN UNSAT, and Q-MAX MINSAT at the second level of the polynomial hierarchy that are of much interest, for example, for diagnostic systems. For each problem, we describe a solution algorithm. As in the SAT and MINSAT case, real applications give rise to classes of Q-ALL SAT, Q-MIN UNSAT, and Q-MAX MINSAT. Using a compiler, we describe a solution algorithm that is effective for all instances in specific classes. |
