PaperlayerView exact revision on arXiv

Source-linked AI summary

The Good Old Davis-Putnam Procedure Helps Counting Models

E. Birnbaum, E. L. Lozinskii

arXiv:1106.0218v1cs.AI

TL;DR

The pure literal rule is inefficient for counting models. The paper presents CDP for propositional model counting; experiments report that Lozinskii performs better on formulas with fewer than six clauses.

  • Problem

    The pure literal rule is inefficient for counting models.

    Source: ) _ DPP(F · p. 4

  • Method

    The paper presents CDP for counting models of propositional formulas and analyzes a variant using only splitting, without the unit-clause rule.

    Source: ) _ DPP(F · pp. 5, 10

  • Results

    For formulas with fewer than six clauses, Lozinskii performs better than CDP.

    Source: ) _ DPP(F · p. 8

  • Takeaways & Limitations

    CDP provides a model-counting procedure for propositional formulas.

    Source: ) _ DPP(F · p. 10

    The developed model-counting algorithms are designed for propositional formulas, while systems are usually expressed in predicate calculus.

    Source: ) _ DPP(F · p. 11

Abstract

from arXiv · show

As was shown recently, many important AI problems require counting the number of models of propositional formulas. The problem of counting models of such formulas is, according to present knowledge, computationally intractable in a worst case. Based on the Davis-Putnam procedure, we present an algorithm, CDP, that computes the exact number of models of a propositional CNF or DNF formula F. Let m and n be the number of clauses and variables of F, respectively, and let p denote the probability that a literal l of F occurs in a clause C of F, then the average running time of CDP is shown to be O(nm^d), where d=-1/log(1-p). The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.

) _ DPP(F

This section describes CDP’s splitting-based approach to counting models of propositional formulas, including a dual algorithm for DNF and refinements to variable selection and small-formula handling. It analyzes average running time and reports experiments on hard instances, including how difficulty varies with formula size and, for fixed clause length, with the clauses-to-variables ratio.

Counting Models

  • DPP treats splitting as its basis, with pure-literal and unit-clause rules serving as literal-choice guides; either can leave only one formula to process.Choosing a non-pure, non-unit-clause literal leaves two formulas for further processing.Source: ) _ DPP(F · p. 4
  • Splitting on a variable x partitions F’s models into disjoint true and false branches, so counting cannot discard a pure-literal branch as satisfiability testing can.The text notes that the pure literal rule is inefficient for model counting.Source: ) _ DPP(F · p. 4
  • Each CDP iteration deletes the chosen variable, reducing the variable count by at least one and guaranteeing termination.The procedure stops on an empty formula or one containing an empty clause.Source: ) _ DPP(F · p. 5

The Recurrence Equation

  • The average-time analysis defines T(m,n) for formulas with m clauses and n variables, assuming common literal-occurrence probability p and independent occurrences.The analysis allows duplicate clauses and tautologies.Source: ) _ DPP(F · p. 5
  • One CDP iteration takes at most cmn time for some constant c.The text bounds formula size by mn and says an iteration requires at most two passes over the formula.Source: ) _ DPP(F · p. 5

Average Running Time

  • The analysis obtains low average-time bounds even for a variant that omits the unit-clause rule and chooses splitting literals randomly.The paper states this result for splitting alone; it does not require frequent application of the unit-clause rule.Source: ) _ DPP(F · p. 5
  • CDP estimates average running time for arbitrary literal-occurrence probability p by modeling splitting as a binary tree whose child formulas have an expected k(1-p) clauses.The analysis estimates the expected tree height and iteration count, with each iteration taking O(mn) time for the formula being processed.Source: ) _ DPP(F · p. 7
  • The variable-selection refinement minimizes the clause count, then breaks ties by minimizing the maximum branch clause count using min(pos(x), neg(x)).The authors report that this combined choice performed best in experiments.Source: ) _ DPP(F · p. 7
  • For formulas below a clause-count threshold, CDP switches to Lozinskii’s algorithm, which outperformed original CDP on randomly chosen formulas in that size range.Source: ) _ DPP(F · p. 8
  • Across tested literal-probability pairs, a clause-count threshold marked hard cases near a corresponding variable count; CDP runtimes ranged from under one second to five hours.Source: ) _ DPP(F · p. 8
  • 1.2 was the hard clauses-to-variables ratio for 3-literal formulas, where CDP’s running time peaked.More generally, for a fixed clause length, running time reached a maximum at a particular ratio.Source: ) _ DPP(F · p. 10
  • As m/n decreases, model counting takes longer relative to satisfiability checking because formulas are more likely to have many models, all of which must be counted.A SAT program stops after finding a satisfying assignment, whereas counting continues over satisfying assignments.Source: ) _ DPP(F · p. 10
  • CDP counts models of propositional formulas, and a dual algorithm can be constructed for DNF formulas.The maximum number of stored clauses is bounded by mn; experimentally, M was almost independent of n and proportional to m, with the coefficient depending on p.Source: ) _ DPP(F · pp. 10–11
  • Having more variables occur both negated and unnegated in clauses improves the performance of the discussed algorithms, while pure literals slow model counting compared with satisfiability checking.Source: ) _ DPP(F · pp. 10–11
  • Experiments found CDP performs better than Lozinskii’s algorithm, with its main advantage being the amount of storage it requires.CDP’s depth-first search of the split tree, deleting at least one variable per split, bounds the maximum number of stored clauses by mn.Source: ) _ DPP(F · p. 11
  • The model-counting algorithms discussed are designed for propositional formulas; developing algorithms for predicate-calculus formulas is identified as an important next challenge.The stated motivation is reasoning with incomplete information in logic systems usually expressed in predicate calculus.Source: ) _ DPP(F · p. 11

Ac kno wledgmen ts

The authors thank the anonymous referees and acknowledge partial support from the Israel Science Foundation, administered by the Israel Academy of Sciences and Humanities.

Acknowledgments

  • The authors thank the anonymous referees and acknowledge partial support from the Israel Science Foundation, administered by the Israel Academy of Sciences and Humanities.Source: Ac kno wledgmen ts · p. 11

App endix A. Pro ofs

The appendix proves bounds relating the recurrence measures T(m,n) and S(m,n), then analyzes conditions on the recurrence parameters. Additional experimental data report recursive-call counts and clauses stored during CDP.

Appendix A. Proofs

  • The proof of Lemma 1 combines a bound on S(m,n) with direct computations for m=0, 1, 2, 3, and 4.Source: App endix A. Pro ofs · p. 12
  • Lemma 2 bounds T(m,n) by a constant multiple of S(m,n) for all m and n.Its proof proceeds by induction on n.Source: App endix A. Pro ofs · p. 12
  • The recurrence analysis derives conditions on its parameters for the stated asymptotic bound, including conditions involving p and the bracketed expression g.The text notes that g is less than 1 for all d and that it diminishes monotonically, tending to 0 as m tends to 1.Source: App endix A. Pro ofs · pp. 13–14

Appendix B. More Experimental Data

Loading 1106.0218v1…