TD 2 : Formes clausales et résolution

Énoncé

EX 1

S’il n’y a pas associativité : il existe des littéraux $p, q, r$ tels que

\[p ∧ (q ∧ r) \not ≡ (p ∧ q) ∧ r\]

Et dans ce cas :

\[\begin{align*} (s ∨ t) ∨ (p ∧ (q ∧ r)) & ≡ ((s ∨ t) ∨ p) ∧ ((s ∨ t) ∨ (q ∧ r)) \\ & ≡ ((s ∨ t) ∨ p) ∧ (((s ∨ t) ∨ q )∧ ((s ∨ t)∨r)) \\ \end{align*}\]

et

\[\begin{align*} (s ∨ t) ∨ (p ∧ (q ∧ r)) & ≡ ((s ∨ (p ∧ (q ∧ r)) ) ∨ (t ∨ (p ∧ (q ∧ r)))) \\ & ≡ ((s ∨ p) ∧ (s ∨ (q ∧ r))) ∨ ((t ∨ p) ∧ (t ∨ (q ∧ r))) \\ & ≡ ((s ∨ p) ∨ (t ∨ p)) ∧ ((s ∨ (q ∧ r)) ∨ (t ∨ p)) ∧ ((s ∨ p) ∨ (t ∨ (q ∧ r))) ∧ ((s ∨ (q ∧ r)) ∨ (t ∨ (q ∧ r))) \\ & ≡ ((s ∨ p) ∨ (t ∨ p)) ∧ ((s ∨ q) ∧ (s∨r)) ∨ (t ∨ p)) ∧ ((s ∨ p) ∨ t) ∨ q) ∧ ((s ∨ p) ∨ r) ∨ q) ∧ ((s ∨ q) ∨ (t ∨ (q ∧ r))) ∧ ((s ∨ r) ∨ (t ∨ (q ∧ r))) \\ \end{align*}\]

EX 2

1.

Par récurrence sur $n$, avec la distributivité de $∨$ sur $∧$ :

  • Initialisation : claire

  • Hérédité :

\[\begin{align*} 𝜑_n & = 𝜑_{n-1} ∨ (P_n ∧ Q_n) \\ & ≡ 𝜓_{n-1} ∨ (P_n ∧ Q_n) \\ & ≡ \left( \bigwedge\limits_{S⊆ \lbrace 1, ⋯, n-1 \rbrace} \bigvee\limits_{i∈S} P_i ∨ \bigvee\limits_{i \not∈S} Q_i \right) ∨ (P_n ∧ Q_n) \\ & ≡ \left( \bigwedge\limits_{S⊆ \lbrace 1, ⋯, n-1 \rbrace} \bigvee\limits_{i∈S} P_i ∨ \bigvee\limits_{i \not∈S} Q_i ∨ P_n \right) ∧ \left( \bigwedge\limits_{S⊆ \lbrace 1, ⋯, n-1 \rbrace} \bigvee\limits_{i∈S} P_i ∨ \bigvee\limits_{i \not∈S} Q_i ∨ Q_n \right) \\ & ≡ \bigwedge\limits_{S⊆ \lbrace 1, ⋯, n \rbrace} \bigvee\limits_{i∈S} P_i ∨ \bigvee\limits_{i \not∈S} Q_i \end{align*}\]

2.

Par l’absurde : car sinon, il existe $i∈⟦1,n⟧$ tq $𝜃_n$ contient une clause $C$ ne contenant ni $P_i$ ni $Q_i$.

Alors pour toute valuation $I$ telle que

\[I \not\vDash 𝜃_n\]

(il en existe car $𝜃_n$ n’est pas une tautologie)

la valuation $I[P_i \mapsto true, Q_i \mapsto true]$ est un modèle de $𝜑_n$, mais n’est toujours pas un modèle de $𝜃_n$ puisque $P_i, Q_i \not\in VarProp(𝜃_n)$

Cela contredit le fait que

\[𝜑_n \vDash 𝜃_n\]

3.

Par l’absurde : Si $𝜃_n$ a une clause qui contient un littéral de la forme $\lnot P_i$ (sans perte de généralité) :

alors la formule $𝜃’_n$ obtenue à partir $𝜃_n$ en supprimant ce littéral vérifie

\[𝜃'_n ≡ 𝜃_n\]

(ce qui est absurde puisqu’elle est en CNF et est de taille strictement inférieure)

En effet :

Clairement : $𝜃’_n \vDash 𝜃_n$, et

pour toute interprétation $I$ satisfaisant $𝜃_n$,

La clause $C$ contenant $\lnot P_i$ contient nécessairement $Q_i$, par 2) (puisqu’elle ne peut pas contenir $P_i$ car sinon elle serait triviale et on pourrait éliminer $P_i$ et $\lnot P_i$, ce qui contredit la minimalité de $𝜃_n$).

Donc comme

  • Cas 1 : un des littéraux différents de $\lnot P_i$ de la clause contenant $\lnot P_i$ est validé par $I$ : alors $I \vDash 𝜃’_n$

  • Cas 2 : tous les littéraux différents de $\lnot P_i$ de la clause $C$ contenant $\lnot P_i$ sont falsifiés par $I$ : alors $I(\lnot P_i) = true$, soit $I(P_i) = false$.

    Et comme, $I(Q_i)=false$:

    \[I \not \vDash 𝜑_n ≡ 𝜃_n\]

    donc ce cas ne se produit pas.

4.

Par l’absurde :

Supposons qu’il existe $S⊆⟦1,n⟧$ tel qu’aucune des clauses de $𝜃_n$ ne contienne

\[C ≝ \bigvee\limits_{i∈S} P_i ∨ \bigvee\limits_{i\not ∈S} Q_i\]

On note $I$ la valuation telle que :

  • $I(P_i) = 0$ ssi $i∈S$
  • $I(Q_i) = 1$ ssi $i∈S$

Comme toutes les clauses de $𝜃_n$ contiennent $P_i$ ET $Q_i$ (par 2), puisque qu’aucune clause ne contient de littéral négatif), $I$ satisfait toutes les clauses de $𝜃_n$, et

\[I \vDash 𝜃_n\]

Mais la clause $C$ de $𝜓_n$ est falsifiée par $I$, donc :

\[I \not \vDash 𝜓_n ≡ 𝜑_n\]

EX 4

$\lnot P ∨ \lnot Q$   $\lnot P ∨ Q$   $P ∨ \lnot Q$   $P ∨ Q$  
    $\lnot P ∨ \lnot P$       $P ∨ P$  
    $\lnot P$       $P$  
        $\bot$      

EX 5

  digraph {
    rankdir=TB;
    subgraph cluster1 {
      label="¬P_2";
      deuxt; troist; troisf;
    }

    subgraph cluster1 {
      label="¬P_2";
      deuxtb; troistc; troisfc;
    }

    subgraph cluster2 {
      label="P_1 ∨ P_2 ∨ P_3";
      troisfd;
    }

    subgraph cluster3 {
      label="¬P_1 ∨ P_2 ∨ ¬P_3";
      troistb;
    }

    subgraph cluster4 {
      label="P_1 ∨ ¬ P_3";
      troistd;
    }

    subgraph cluster5 {
      label="P_1 ∨ ¬P_3";
      troisfb;
    }

    unt[label="P_1"];
    unf[label="¬P_1"];
    deuxt[label="P_2"];
    deuxf[label="¬P_2"];
    deuxtb[label="P_2"];
    deuxfb[label="¬P_2"];
    troist[label="P_3"];
    troisf[label="¬P_3"];
    troistb[label="P_3"];
    troisfb[label="¬P_3"];
    troistc[label="P_3"];
    troisfc[label="¬P_3"];
    troistd[label="P_3"];
    troisfd[label="¬P_3"];
    ∅ -> unt[label="1"];
    ∅ -> unf[label="0"];
    unt -> deuxt[label="1"];
    unt -> deuxf[label="0"];
    unf -> deuxtb[label="1"];
    unf -> deuxfb[label="0"];
    deuxt -> troist[label="1"];
    deuxt -> troisf[label="0"];
    deuxf -> troistb[label="1"];
    deuxf -> troisfb[label="0"];
    deuxtb -> troistc[label="1"];
    deuxtb -> troisfc[label="0"];
    deuxfb -> troistd[label="1"];
    deuxfb -> troisfd[label="0"];
  }

L’ensemble n’est pas satisfaisable car toute valuation falsifie une de ses clauses.

EX 6

1.

Résolution de deux 2-clauses ⟶ une 2-clause (clairement : idem pour factorisation).

Donc Résolution + Factorisation ⟶ tous les noeuds de l’arbre de preuve sont des 2-clauses, et comme il y en a un nombre quadratique, le résultat s’ensuit.

2.

Par réc sur $k$ :

  • $k=0$, $∈E$
  • $k+1$ :

$𝜋_{k+1}^1$

$𝜋_{k}^2$ $𝜋_{k}^3$
$P_0 ∨ ¬P_{n-k}$ $P_{n-k} ∨ P_{n-k-1}$
  $P_{0} ∨ P_{n-k-1}$
$𝜋_{k+1}^1$ $∈E$
$P_0 ∨ P_{n-k-1}$ $¬P_{0} ∨ P_{n-k-2}$
  $P_{n-k-2} ∨ P_{n-k-1}$
$𝜋_{k}^1$   $∈E$ $∈E$  
$P_0 ∨ P_0$   $¬P_{0} ∨ P_1$ $¬P_{0} ∨ ¬P_1$  
  $P_0$     $¬P_0$
    $\bot$    

Donc algo en $O(n^4)$ pour obtenir $\bot$ : partir des clauses de base, et le saturer ⟶ on va finir par obtenir $\bot$ en temps polynomial.

Leave a comment