Parameterizing Models of Propositional Calculus Formulas

John McCarthy Computer Science Department Stanford University jmc@cs.stanford.edu http://www-formal.stanford.edu/jmc/

July 2, 2007

Abstract It is often inadequate that a theory be consistent, i.e. have models. It should have enough models. We discuss parameterizing the set of models in the special case of propositional satisfiability.

A propositional formula π in variables p_{1}, …, p_{n} is called satisfiable if it has a model, i.e. a tuple of truth values for p_{1}, …, p_{n} that makes π true. Many programs exist for deciding this.

However, we can ask for more than just whether a formula has models; we can ask about its set of models. One way to get a grip on the set of a formula’s models is to parametrize it, i.e. to express the variables p_{1}, …, p_{n} of the formula π as propositional expressions in other variables r_{1}, …, r_{k}, such that arbitrary values of r_{1}, …, r_{k} give rise to exactly the values of p_{1}, …, p_{n} satisfying π.

Here are some examples.

• π = p_{1}p_{2}. this is a trivial case and the formulas are p_{1} = true and p_{2} = true.

• π = p_{1} ≡ p_{2}. We have p_{1} = r_{1} and p_{2} = r_{1}.

• π = p_{1} ∨ p_{2}. We have p_{1} = r_{1} and p_{2} = r̄_{1} ∨ r̄_{2}.

• π = true. We have p_{1} = r_{1} and p_{2} = r_{2}.

• π = false. No model.

The number of parameters required depends on the number N of models of π. Indeed it is (log_{2}(N)), the least it could possibly be. Here’s how to construct a parametrization.

Let π be written in disjunctive normal form. Choose enough variables r_{1}, …, r_{k}, so that each conjunction is assigned one or more of the 2^{k} conjunctions of the r_{i} and r̄_{i}. The assignment can be arbitrary provided each conjunction of the p_{i}s gets a unique conjunction of the r_{j}s. For each p_{i}, we write a conditional expression

if case_{1} then tv_{1}
else if case_{2} then tv_{2}
⋮
else if case_{2^{k}} then tv_{2^{k}},

(1)

where the cases are the r-conjunctions and the tv’s are the truth values that p_{i} assumes in that case. The conditional expressions can be converted to propositional expressions if desired, since all the consequents are truth values. Example:

[We’ll use juxtaposition for conjunction to keep the formulas compact.] Let

π = (p_{1}p_{2}p_{3}) ∨ (p̄_{1}p_{2}p̄_{3}) ∨ (p_{1}p̄_{2}p_{3}).  (2)

We need only 2 r variables. These give 4 cases. We can assign the cases to the three terms of (2) arbitrarily, so let’s assign tt and tf to the first conjunction of (2) and ft and ff to the two remaining conjunctions. We then have

p_{1} = if r_{1}r_{2} then t else if r_{1}r̄_{2} then t else if r̄_{1}r_{2} then f else if r̄_{1}r̄_{2} then t
p_{2} = if r_{1}r_{2} then t else if r_{1}r̄_{2} then t else if r̄_{1}r_{2} then t else if r̄_{1}r̄_{2} then f
p_{3} = if r_{1}r_{2} then t else if r_{1}r̄_{2} then t else if r̄_{1}r_{2} then f else if r̄_{1}r̄_{2} then t

Remarks:

1. Presumably the above systematic procedure usually doesn’t give the optimal parametrization in terms of length of formula, although it is optimal in the number of r-variables.

2. The parametrization is easy, because we have assumed that the theory is represented by an expression π in disjunctive normal form. If putting the theory in disjunctive normal form leads to an excessively long expression, the parametrization may be more difficult.

3. There is no apparent way of turning a parameterization of the models of π into a parameterization of the models of ¬π.

4. Parameterizing models of modal formulas may offer difficulties, because there will often be an infinity of models of even rather simple formulas. This will depend on the modal logic.

5. Extending the idea to predicate calculus is likely to be reasonable only under some restrictions. Thus parameterizing the models of the axioms for a group is the problem of group classification with its hundred year history. However, Abelian groups are nicely parameterized.

6. Perhaps monadic predicate calculus will be a good domain.

7. Parameterizing the models of nonmonotonic theories may present interesting problems even in the propositional case. 2001 August.

8. There may be straightforward ways of going from a parameterization of a theory to parameterizations of some kinds of elaborations of the theory. This may help with the problem of establishing consistency of the elaborated theory. Thus the mere fact of consistency of a theory may not help in establishing the consistency of an elaborated theory, but a parameterization of the theory may lead to consistency of the elaborated theory via its parameterization. - 2001 August.