3CF 3-conjunctive form satisfiability I am self studying discrete math and I am going through MIT Mathematics for CS lecture notes but they do not have solutions available. I got stuck at Problem 3.14 (pages 64-65 of this document). The problem is about the construction, given an arbitrary propositional formula $F$, of a proposition $C(F)$ such that:


$C(F)$ is in 3-conjunctive form (3CF), i.e. it is a conjunction of disjunctions of at most literals (a literal is a variable or a negation of a variable);
$C(F)$ has at most 24 times as many occurrences of variables as $F$;
$C(F)$ is satisfiable iff $F$ is.


The idea is to introduce a new variable for each operator that occurs in $F$. For example, given
$$ F_1 = ((P \oplus Q) \oplus R) \vee (\neg P \wedge S)) $$
assign $X_1, X_2, O, A$ to the 4 operators in $F_1$, and define four constraining formulas:
$$ \begin{align*}
 C_1^1 &amp;= X_1 \Leftrightarrow (P \oplus Q) \\
 C_1^2 &amp;= X_2 \Leftrightarrow (X_1 \oplus R) \\
 C_1^3 &amp;= A \Leftrightarrow (\neg P \wedge S) \\
 C_1^4 &amp;= O \Leftrightarrow (X_2 \oplus A) \\
\end{align*} $$
and $C_1 = C_1^1 \wedge C_1^2 \wedge C_1^3 \wedge C_1^4 \wedge O$.

The questions are:


Why is $C_1$ satisfiable iff $F_1$ is satisfiable?
Why is each constraining formula equivalent to a 3CF formula with at most 24 occurrences of variables?
Generalize from the example to construct $C(F)$ for an arbitrary formula $F$.


For question 1, I don't see why $X_1$ is satisfiable.

I think question 2 is wrong, beacuse you can form a 3CF formula with at most 24 occurrences of variables, only if you have a 3-conjunctive normal form but here the author only says 3 conjunctive form. 

(For 3CNF, 8 different triple terms can be formed using 3 variables with a total of 24 variables, For 3CF, 26 different single,double and triple terms can be formed with a total of ? variables.)

No idea about question 3.
First of all, I assume that $C_1^4 \equiv O \iff (X_2 \lor A)$ in accordance to $F_1$. Second, note that 3CF as defined in the exercise is equivalent to 3CNF. In the following, I will denote with $\phi_X$ the subformula of the given formula $F$ which has been assigned new variable $X$ by the construction. For example, $\phi_A=(\lnot P \land S)$ and $\phi_O = F_1$.
$\renewcommand{\models}{\mathop{|\!\!\!=}}\newcommand{\rmodels}{\mathop{=\!\!\!|}} \newcommand{\semeq}{\models\!\rmodels}$

Satisfaction equivalence


  I don't see why $X_1$ is satisfiable


$X_1$ is a single variable and thus trivially satisfiable (by setting it to $1$). The $C_1^i$ essentially take apart $F_1$ operator by operator, introducing new variables that have to evaluate to the same truth values as their respective subformulae. Using $\{O\}$ as clause of $C_1$ guarantees the statement, essentially (as "$O \semeq F_1$", given $C_1$).

Proof

Assume $F_1$ is satisfiable and let $\psi$ be a satisfying valuation of the variables. Construct $\psi'$ by extending $\psi$ with $\psi'(X) = \psi(\phi_{X})$ for $X \in \{X_1,X_2,A,O\}$. As a consequence, $\psi'$ satisfies all $C_i^1$. Because $\psi(F_1)=1$ by assumption, we have chosen $\psi'(O)=1$. Therefore, $\psi'(C_1)=1$.

Conversely, assume $C_1$ is satisfiable and let $\psi$ a satisfying valuation. Clearly, $\psi(O)=1$ and $\psi(C_1^4)=1$. Therefore, $\psi(\psi_O)=1$. Because $\psi_O=F_1$, we are done -- $\psi$ satisfies $F_1$. In order to be rigorous, we would have to iterate this argument top-down, following the structure of $F_1$, to unfold $X_2$ and then $X_1$ (in the general case, we would need a structural induction here).

Size restriction

The constraining formulae all have the same form and are small (three literals, two operators). You can transform those into equivalent 3CF formulae locally, i.e. ignoring the others. This conversion always yields formulae with at most 24 literals, that is at most 8 clauses. This can be shown by dull calculation.

Details

The general form of a contraining formula is $A \iff (A \circ B)$ for $\circ$ some logical operator. Let us transform it into 3CF using laws and rules of boolean algebra.

$\qquad \begin{align}
  C^i &amp;\equiv X \iff (A \circ B) \\
      &amp;\semeq\ [X \land (A \circ B)] \lor [\lnot X \land \lnot(A \circ B)] \\
      &amp;\semeq\ [\lnot X \lor (A \circ B)] \land [ X \lor \lnot(A \circ B)] 
\end{align}$

Now, for $\circ = \land$, we use both distributive and associative law resp. De Morgan's rule:

$\qquad \begin{align}
  C^i &amp;\semeq\ [\lnot X \lor (A \land B)] \land [ X \lor \lnot(A \land B)] \\
      &amp;\semeq\ [\lnot X \lor A] \land [\lnot X \lor B] \land [ X \lor \lnot A \lor \lnot B]
\end{align}$

This has three clauses (after padding with redundant literals, nine literals). For $\circ \in \{\lor, \to\}$¹ this works exactly the same way. You can proceed similarly for other choices of $\circ$, such as $\oplus$ or $\iff$, depending on which operators are allowed in your setting.

Generalisation

This is just a matter of writing down what the example does in general terms. Let $F$ an arbitrary propositional formula, w.l.o.g. without "negation chains"². Now do the following.

$\quad$ Let $i=0$.
$\quad$ Until $F$ is a literal, do
$\qquad$  Increase $i$ by one.
$\qquad$  Pick a subformula of $F$ of the form $L_1 \circ L_2 = \phi$ with $L_1,L_2$ literals.
$\qquad$  Let $C^i \equiv X_i \iff (L_1 \circ L_2)$.
$\qquad$  Replace $\phi$ with $X_i$ in $F$.
$\quad$ For all $j=1,\dots,i$, convert $C^j$ into 3CF by finite case distinction.
$\quad$ Return $[F \lor F \lor F] \land \bigwedge_{j=1}^{i} C^j$.

Note that $F = X_i$ after the loop. For intuition and implementation purposes, think of a formula as a tree: operators are inner nodes, leaves are literals. Above algorithm iteratively contracts subtrees of height two into leaves, collecting the $C^j$ as "mapping" from new variable to the removed subtree along the way.




Remember $A \to B \semeq \lnot A \lor B$.
We can always use $\lnot \lnot A \semeq A$.