A Note on Boolean Satisfiability.

From: conesetter (conesetter_at_btopenworld.com)
Date: 10/18/04

  • Next message: Torben Ęgidius Mogensen: "Re: Testing for acceptance of Kleene closure of alphabet" 
    Date: 17 Oct 2004 22:41:09 -0700

    Any Boolean truth-function of n variables can be expressed in
    disjunctive normal form, as a disjunction of conjunctions of literals
    of the n variables. We determine how many such conjunctions there are
    and how many are satisfiable. For n=1 there are 4: the null
    conjunction, call it T, the variable, its negation and the conjunction
    of the two. The last is not satisfiable so there are 3 satisfiable.
    General formulas are obtained by induction. If x is a new variable
    then a conjunction can be left as it is or have x included or ¬x
    included or both, so the total number of possible conjunctions is
    multiplied by 4. Since adding both would remove a conjunction from
    satisfiability the number of satisfiable conjunctions is multiplied by
    3. So there are 4^n in total of which 3^n are satisfiable, the
    difference of the two numbers, call it D(n), being the number not
    satisfiable.
      Given a disjunction formed from a subset of these 4^n conjunctions
    let it be asked if it is satisfiable. It is so if at least one of its
    conjunctions is. By the above if, with exclusion of repetitions, there
    are more than D(n) then one of them must be satisfiable so the
    disjunction is satisfiable. This can be asserted without a witness to
    satisfiability actually having to be found.
      If there are not more than D(n) conjunctions the above existence
    argument does not apply and one may be reduced to looking for some
    witness among them which may or may not exist.
      The number 4^n - 3^n, which we have called D(n), is easily shown to
    increase more rapidly than 3^n.

      Copyright Oct2004 conesetter. References are welcome, use requires
    consent.

  • Next message: Torben Ęgidius Mogensen: "Re: Testing for acceptance of Kleene closure of alphabet"