Some aspects of the probabilistic behavior of variants of resolution

Abstract

The SAT-Problem fot boolean formulas in conjunctive normal form often arises in the area of artificial intelligence, its solution is known as mechanical theorem proving. Most mechanical theorem provers perform this by using a variant of the resolution principle. The time and space complexity of resolution strongly depends on the class of formulas. Horn formulas, where each clause may contain at most one positive literal, represent the most important class where resolution proofs with polynomial length exist. A special sort of Horn formulas, where each clause contains exactly one positive literal, is called logic programs. In logic programs, clauses of length one are also known as facts, clauses of length greater than one are known as rules. We show that there are typically short resolution proofs under unit/Davis-Putnam resolution for some models of formulas, and we study the “density” of rules necessary in another model for deriving the empty clause with probability tending to one.