Question

A boolean expression in Conjunctive Normal Form (CNF) is mimsy if every clause contains a variable that appears in no earlier clause. So, if $\varphi = C_1 \wedge C_2 \wedge \dots \wedge C_i \wedge \dots \wedge C_m$ where each $C_i$ is a disjunction of literals, then $\varphi$ is mimsy if, for each i, there is a variable $x_i$ that appears in $C_i$ (either as $x_i$ or negated $\neg x_i$) but does not appear in any of $C_1, \dots, C_{i-1}$.

For example, the following expression $\alpha$ is mimsy: $\alpha := (x \lor \neg y) \wedge (y \lor \neg z)$. This is because the first clause, $C_1 = x \lor \neg y$, includes at least one variable that does not appear in any earlier clauses, and the second clause, $C_2 = y \lor \neg z$, includes a variable, z, that does not appear in $C_1$.

On the other hand, the following expression $\beta$ is not mimsy: $\beta := (x \lor y) \wedge (x \lor y)$. This is because all the variables in the second clause also appeared in the first clause.

A Boolean expression is satisfiable if there is an assignment of truth values to its variables that makes the expression True.

---

Prove the following statement, by mathematical induction:

For all $m \ge 1$, every mimsy Boolean expression in CNF with $m$ clauses is satisfiable.

(a) Pre-proof exploration: (i) Show that each of the example expressions above, $\alpha$ and $\beta$, is satisfiable. For each of them, you just need to give one truth assignment to its variables that satisfies it. (ii) Construct an expression in CNF, with at least two literals in each clause, that is not mimsy and not satisfiable.

(b) Inductive basis: prove the statement (*) for $m=1$.

(c) Given a mimsy Boolean expression $\varphi$ with $m+1$ clauses, show how to construct from it a mimsy Boolean expression $\varphi^-$ with just m clauses that will help with your proof.

(d) What does your Inductive Hypothesis tell you about $\varphi^-$?

(e) Using the fact that $\varphi$ is mimsy, and your answer to (d), show that $\varphi$ has a satisfying truth assignment.

(f) When drawing your final conclusion, don't forget to briefly state that you are using the Principle of Mathematical Induction!

---

Answer

(a) Pre-proof exploration:

(i) Satisfiability of $\alpha$ and $\beta$

• For the expression $\alpha := (x \lor \neg y) \wedge (y \lor \neg z)$, a satisfying truth assignment is x = True, y = True, z = True.

  • $(True \lor \neg True) \wedge (True \lor \neg True)$
  • $(True \lor False) \wedge (True \lor False)$
  • $True \wedge True$, which is True.

• For the expression $\beta := (x \lor y) \wedge (x \lor y)$, a satisfying truth assignment is x = True, y = False.

  • $(True \lor False) \wedge (True \lor False)$
  • $True \wedge True$, which is True.

(ii) Non-mimsy and non-satisfiable expression

An example of an expression in CNF with at least two literals in each clause that is not mimsy and not satisfiable is: $(x \lor y) \wedge (\neg x \lor \neg y) \wedge (x \lor \neg y) \wedge (\neg x \lor y)$

• Not Mimsy: All variables in the subsequent clauses ($x$ and $y$) have already appeared in the first clause.
• Not Satisfiable: There is no truth assignment for $x$ and $y$ that will make all four clauses true simultaneously. For any of the four possible assignments (T,T), (T,F), (F,T), (F,F), one of the clauses will evaluate to False.

(b) Inductive basis:

We must prove the statement for $m=1$: "every mimsy Boolean expression in CNF with 1 clause is satisfiable". An expression with one clause is just $C_1$. By definition, any expression with one clause is mimsy because there are no earlier clauses for its variables to have appeared in. A clause is a disjunction of literals. We can satisfy the clause by choosing a truth assignment that makes at least one of its literals true. For any variable $x_i$ in $C_1$, if the literal is $x_i$, we set $x_i$ to True; if the literal is $\neg x_i$, we set $x_i$ to False. This satisfies $C_1$. Thus, the statement holds for $m=1$.

(c) Construction of $\varphi^-$

Given a mimsy Boolean expression $\varphi$ with $m+1$ clauses, $\varphi = C_1 \wedge \dots \wedge C_m \wedge C_{m+1}$. We construct $\varphi^-$ by removing the last clause: $\varphi^- = C_1 \wedge \dots \wedge C_m$. This new expression $\varphi^-$ has $m$ clauses and is also mimsy, as the condition for being mimsy holds for each of its clauses $C_1, \dots, C_m$ just as it did in the original expression $\varphi$.

(d) Implication of the Inductive Hypothesis

The Inductive Hypothesis (IH) assumes that every mimsy Boolean expression in CNF with $m$ clauses is satisfiable. Since $\varphi^-$ is a mimsy Boolean expression with $m$ clauses, the IH tells us that $\varphi^-$ is satisfiable. This means a truth assignment exists that makes $\varphi^-$ true.

(e) Proving satisfiability for $\varphi$

We know $\varphi = \varphi^- \wedge C_{m+1}$ and that there is a truth assignment, $A$, that satisfies $\varphi^-$. Because the original expression $\varphi$ is mimsy, the clause $C_{m+1}$ must contain a variable, $x_{m+1}$, that does not appear in any of the preceding clauses $C_1, \dots, C_m$.

This means the variable $x_{m+1}$ is not in $\varphi^-$, and the assignment $A$ does not assign it a value. We can extend assignment $A$ by assigning a truth value to $x_{m+1}$ without affecting the truth of $\varphi^-$. We choose a value for $x_{m+1}$ that satisfies $C_{m+1}$:

• If $C_{m+1}$ contains the literal $x_{m+1}$, we set $x_{m+1} =$ True.
• If $C_{m+1}$ contains the literal $\neg x_{m+1}$, we set $x_{m+1} =$ False.

This extension makes $C_{m+1}$ true. Since the assignment still satisfies $\varphi^-$, the full extended assignment satisfies $\varphi = \varphi^- \wedge C_{m+1}$. Therefore, $\varphi$ is satisfiable.

(f) Conclusion

We have shown that the base case ($m=1$) is true, and we have shown that if the statement holds for any integer $m \ge 1$, it also holds for $m+1$. Therefore, by the Principle of Mathematical Induction, we conclude that every mimsy Boolean expression in CNF with $m$ clauses is satisfiable for all $m \ge 1$.

Changelog

8/8/25, 4:17 AM

View All Changelog

• 2aa48-web-deploy(Auto): Update base URL for web-pages branchon 8/8/25

Copyright

Copyright Ownership:WARREN Y.F. LONG

License under:Attribution-NonCommercial-NoDerivatives 4.0 International (CC-BY-NC-ND-4.0)