06/01/1996 09:00 AM
Computer Engineering
Modoc was proposed by Van Gelder as an improvement to model elimination. The main contribution of Modoc is in its new pruning technique based on the concept of autarky, first introduced by Monien and Speckenmeyer. Compared to programs based on model search, Modoc has since been observed to excel in speed on circuit formulas yet to fall behind on random formulas. This paper reports on a study conducted to explain this behavior in Modoc. The study is based on experiment in which the effectiveness of the two pruning techniques used in Modoc---autarky pruning and lemma pruning---are examined on random and circuit formulas. We observe that the effectiveness of autarky pruning differs tremendously between the two classes of formulas. We also observe that for circuit formulas, autarkies, which are believed to be very few of, are more likely to be found by simplifying the formula for some partial truth assignment. This may lead to possible new ways to use autarkies to solve the satisfiability problem.
