Parameterizing Models of Propositional Calculus Formulas

John McCarthy

Computer Science Department

December 24, 2003

Stanford University

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 $\pi$ in variables $p_1,\ldots,p_n$ is called satisfiable if it has a model, i.e. a tuple of truth values for $p_1,\ldots,p_n$ that makes $\pi$ 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,\ldots,p_n$ of the formula $\pi$ as propositional expressions in other variables $r_1,\ldots,r_k$, such that arbitrary values of $r_1,\ldots,r_k$ give rise to exactly the values of $p_1,\ldots,p_n$ satisfying $\pi$.

Here are some examples.

• $\pi = p_1p_2$. this is a trivial case and the formulas are $p_1 = \mathbf{true}$ and $p_2 = \mathbf{true}$.

• $\pi = p_1 \equiv p_2$. We have $p_1 = r_1$ and $p_2 = r_1$.

• $\pi = p_1 \lor p_2$. We have $p_1 = r_1$ and $p_2 = \bar{r}_1 \lor \bar{r}_2$.

• $\pi = \mathbf{true}$. We have $p_1 = r_1$ and $p_2 = r_2$.

• $\pi = \mathbf{false}$. No model.

The number of parameters required depends on the number $N$ of models of $\pi$. Indeed it is $\mathit{ceiling}(\log_2(N))$, the least it could possibly be. Here's how to construct a parametrization.

Let $\pi$ be written in disjunctive normal form. Choose enough variables $r_1,\ldots,r_k$, so that each conjunction is assigned one or more of the $2^k$ conjunctions of the $r_i$ and $\bar{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

$$\begin{array}{l} \mathbf{if}\ \mathit{case}_1\ \mathbf{the... ...case}_{2^k}\ \mathbf{then}\ \mathit{tv}_{2^k}, \end{array}$$ (1)

where the $\mathit{case}$s are the r-conjunctions and the $\mathit{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

$$\pi = (p_1p_2p_3) \lor (\bar{p}_1p_2\bar{p}_3) \lor (p_1\bar{p}_2p_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

$$\begin{eqnarray*} p_1 &=& \mathbf{if}\ r_1r_2\ \mathbf{then}\ t\ \mathbf{else\ ... ...en}\ f\ \mathbf{else\ if}\ \bar{r}_1\bar{r}_2\ \mathbf{then}\ t \end{eqnarray*}$$

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 $\pi$ 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 $\pi$ into a parameterization of the models of $\lnot \pi$.

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.