```python
import sympy as sp
from sympy import *
from sympy.abc import *
```

# Summary 

Any propositional formula can be rewritten with De Morgan laws as an equivalent formula in Clausal Normal Form. However this can lead to exponential growhth in size and therefore prevent any real life application.

Tseitin transformation https://en.wikipedia.org/wiki/Tseytin_transformation is a classical work around. It transform a propositional formula A into another formula T(A) which can be in turn be rewritten as a CNF with a linear increase in size.

We illustrated Tseitin transformation using sympy 



```python
x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11 = symbols('x:12')
```

Straight forward rewritten of (x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11) into a CNF has 64 clauses of 6 literals each 


```python
sp.to_cnf((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))
```




    (x0 | x10 | x2 | x4 | x6 | x8) & (x0 | x10 | x2 | x4 | x6 | x9) & (x0 | x10 | x2 | x4 | x7 | x8) & (x0 | x10 | x2 | x4 | x7 | x9) & (x0 | x10 | x2 | x5 | x6 | x8) & (x0 | x10 | x2 | x5 | x6 | x9) & (x0 | x10 | x2 | x5 | x7 | x8) & (x0 | x10 | x2 | x5 | x7 | x9) & (x0 | x10 | x3 | x4 | x6 | x8) & (x0 | x10 | x3 | x4 | x6 | x9) & (x0 | x10 | x3 | x4 | x7 | x8) & (x0 | x10 | x3 | x4 | x7 | x9) & (x0 | x10 | x3 | x5 | x6 | x8) & (x0 | x10 | x3 | x5 | x6 | x9) & (x0 | x10 | x3 | x5 | x7 | x8) & (x0 | x10 | x3 | x5 | x7 | x9) & (x0 | x11 | x2 | x4 | x6 | x8) & (x0 | x11 | x2 | x4 | x6 | x9) & (x0 | x11 | x2 | x4 | x7 | x8) & (x0 | x11 | x2 | x4 | x7 | x9) & (x0 | x11 | x2 | x5 | x6 | x8) & (x0 | x11 | x2 | x5 | x6 | x9) & (x0 | x11 | x2 | x5 | x7 | x8) & (x0 | x11 | x2 | x5 | x7 | x9) & (x0 | x11 | x3 | x4 | x6 | x8) & (x0 | x11 | x3 | x4 | x6 | x9) & (x0 | x11 | x3 | x4 | x7 | x8) & (x0 | x11 | x3 | x4 | x7 | x9) & (x0 | x11 | x3 | x5 | x6 | x8) & (x0 | x11 | x3 | x5 | x6 | x9) & (x0 | x11 | x3 | x5 | x7 | x8) & (x0 | x11 | x3 | x5 | x7 | x9) & (x1 | x10 | x2 | x4 | x6 | x8) & (x1 | x10 | x2 | x4 | x6 | x9) & (x1 | x10 | x2 | x4 | x7 | x8) & (x1 | x10 | x2 | x4 | x7 | x9) & (x1 | x10 | x2 | x5 | x6 | x8) & (x1 | x10 | x2 | x5 | x6 | x9) & (x1 | x10 | x2 | x5 | x7 | x8) & (x1 | x10 | x2 | x5 | x7 | x9) & (x1 | x10 | x3 | x4 | x6 | x8) & (x1 | x10 | x3 | x4 | x6 | x9) & (x1 | x10 | x3 | x4 | x7 | x8) & (x1 | x10 | x3 | x4 | x7 | x9) & (x1 | x10 | x3 | x5 | x6 | x8) & (x1 | x10 | x3 | x5 | x6 | x9) & (x1 | x10 | x3 | x5 | x7 | x8) & (x1 | x10 | x3 | x5 | x7 | x9) & (x1 | x11 | x2 | x4 | x6 | x8) & (x1 | x11 | x2 | x4 | x6 | x9) & (x1 | x11 | x2 | x4 | x7 | x8) & (x1 | x11 | x2 | x4 | x7 | x9) & (x1 | x11 | x2 | x5 | x6 | x8) & (x1 | x11 | x2 | x5 | x6 | x9) & (x1 | x11 | x2 | x5 | x7 | x8) & (x1 | x11 | x2 | x5 | x7 | x9) & (x1 | x11 | x3 | x4 | x6 | x8) & (x1 | x11 | x3 | x4 | x6 | x9) & (x1 | x11 | x3 | x4 | x7 | x8) & (x1 | x11 | x3 | x4 | x7 | x9) & (x1 | x11 | x3 | x5 | x6 | x8) & (x1 | x11 | x3 | x5 | x6 | x9) & (x1 | x11 | x3 | x5 | x7 | x8) & (x1 | x11 | x3 | x5 | x7 | x9)



Let's have first a look at Tseitin transformation for formula $$((p \lor q) \land r) \implies \neg s$$
we need to 
1. compute all subformulas, atoms excepted
2. sort them by depth 
3. Conjunct all substitutions and the substitution
4. then transform all substitution in CNF 

Step 1: computing $$((p \lor q) \land r) \implies \neg s$$ subformulas


```python
def subformulas(expr):
# subformula of expr without atoms
# considering operator as binary
    
    if expr.func == sp.Symbol:
        return []
    elif len(expr.args)==1:
        return [expr] + subformulas(expr.args[0])
    elif len(expr.args)==2:
        return [expr] + subformulas(expr.args[0]) + subformulas(expr.args[1]) 
    elif len(expr.args)>2:
        return [expr] + subformulas(expr.args[0]) + subformulas(eval(str(expr.func)+str(expr.args[1:])))  
    else:
        return "error"
```


```python
subformulas(((p |q) & r) >> (~s))
```




    [Implies(r & (p | q), ~s), r & (p | q), p | q, ~s]



**Note**: we considers the operators as binary while sympy consider them as n-ary. So we choose for subformulas (ignoring atoms) of (A & B & C), the subformulas of A & (B & C): A & B & C,  B & C


```python
subformulas(A & B & C)
```




    [A & B & C, B & C]



We define the depth of a formula in the following way
- depth(A)=0 if A is an atom
- depth(~F) = depth(F) + 1
- depth(F1 op F2) = max(depth(F1), depth(F2)) + 1, for op a boolean binary operator (here we consider conjunction, disjunction and implication)


```python
def depth(expr):
# still considering operator as binary
    if expr.func == Not:
        return 1 + depth(expr.args[0])
    elif (len(expr.args)==2):
        return 1 + max([depth(x) for x in expr.args])
    elif ( len(expr.args)>2):
        #return 1 + max(depth(expr.args[0]), depth(eval(str(expr.func)+str(expr.args[1:]))))
        return len(expr.args)-1 + max([depth(x) for x in expr.args])
    elif expr.func == Symbol:
        return 0
    else: 
        return"error"
```


```python
depth(((p |q) & r) >> (~s))
```




    3



Again we consider the boolen operator to be binary, so depth(A & B & C) = depth(A & (B & C))=2


```python
depth(A& B & C)
```




    2



Sorting subformulas (not taking into account atoms) of
$$((p \lor q) \land r) \implies \neg s$$
per depth will give us 
$$\begin{array}{l}
p \lor q\\
\neg s \\
r \land (p \lor q)\\
r \land (p \lor q) \implies \neg s\\
\end{array}$$





```python
F = ((p |q) & r) >> (~s)
sorted(subformulas(F), key=depth)
```




    [p | q, ~s, r & (p | q), Implies(r & (p | q), ~s)]



We can now  write the following formulas
<br>
$\begin{array}{lll}
x_0  & \Leftrightarrow & p \lor q \\
x_1  & \Leftrightarrow & \neg s \\
x_2  & \Leftrightarrow & r \land x_0\\
x_3  & \Leftrightarrow & (x_2 \implies x_1)
\end{array}$
<br>

and conjunct them to get <br>
$T(((p \lor q) \land r) \implies \neg s) := x_3 \land (x_3  \Leftrightarrow (x2 \implies x1)) \land (x_2  \Leftrightarrow r \land x0) \land (x_1  \Leftrightarrow \neg s) \land (x_0  \Leftrightarrow p \lor q)$

First We need  a way to get new symbol. This is done using closure:


```python
def symbol_init(x, count=0):
    def new_symbol ():
        nonlocal count
        count += 1
        return var(str(x) + str(count)) #var add the new symbol in the name space
    return new_symbol
```


```python
si = symbol_init('t')
```


```python
si() | si()
```




    t1 | t2



As sympy boolean operator are n aries, sympy subs will not work well for us need. For instance 


```python
(x1 & Not(x2) &x3).subs(Not(x2) & x3, A)
```




    x1 & x3 & ~x2



So we need to define a custom substiturion handling boolean operator as binary 


```python
def binSubs(x, y, z):
    #replace y by z in x
    #print("subs", x, y, z)
    if (len(y.args) >0) and (len(x.args)>2) and (y!=x) and (y.func==x.func):
     
        if all([y in x.args for y in y.args]): 
            l = list(x.args)
            for i in y.args:
                l.remove(i)
            if (z.func== Symbol):
                t=tuple(l + [z])
            else:
                t=tuple(l+list(z.args))
            return eval(str(x.func) + str(t))
    
    return x.subs(y,z)
            
```


```python
binSubs((x1 & ~x2 &x3), x1 & ~x2, A)
```




    A & x3



We can now put together tseitin transformation 


```python
def tseitin1(expr):
    # for binary operation

    s=symbol_init("p")
    if expr.func == Symbol:
        return true
    else:
        return tseitin_aux(sorted(subformulas(expr), key=depth), s) 

def tseitin_aux(L, s):
    #nonlocal newvar
    newvar = s()
    if (L==[]):
        return true
    if depth(L[0]) > 0:
        if len(L[1:])>0 :
            #newList = [x.subs(L[0], newvar) for x in L[1:]]  
            
            newList = [binSubs(x, L[0], newvar) for x in L[1:]]  
            
            return Equivalent(newvar, L[0]) & tseitin_aux(newList, s)
        else:      
            return Equivalent(newvar, L[0]) & newvar
    else:
        print("error")   
```


```python
F = ((p |q) & r) >> (~s)
tseitin1(F)
```




    p4 & (Equivalent(p2, ~s)) & (Equivalent(p1, p | q)) & (Equivalent(p3, p1 & r)) & (Equivalent(p4, Implies(p3, p2)))




```python
F2 = (~(p |~q) & r) >> (~s)
tseitin1(F2)
```




    p6 & (Equivalent(p1, ~q)) & (Equivalent(p2, ~s)) & (Equivalent(p4, ~p3)) & (Equivalent(p3, p | p1)) & (Equivalent(p5, p4 & r)) & (Equivalent(p6, Implies(p5, p2)))



From there, we leverage makes the final transformation to CNF leveraging the following equivalences <br>
$\begin{array}{lll}
x  \Leftrightarrow (y \land z)  & \equiv  & (y \lor \neg x) \land (z \lor \neg x) \land (x \lor \neg y \lor \neg z)\\
x  \Leftrightarrow (y \lor z) & \equiv & (x \lor \neg y) \land (x \lor \neg z) \land (y \lor z \lor \neg x)\\
x  \Leftrightarrow (y \implies z) & \equiv & (x \lor y) \land (x \lor \neg z) \land (z \lor \neg x \lor \neg y)\\
x  \Leftrightarrow (\neg y) & \equiv & (x \lor y) \land (\neg x \lor \neg y)\\
\end{array}$
<br>


```python
print(sp.to_cnf(Equivalent(x, y & z)))
print(sp.to_cnf(Equivalent(x, y | z)))
print(sp.to_cnf(Equivalent(x, y >> z)))
print(sp.to_cnf(Equivalent(x, ~y)))
```

    (y | ~x) & (z | ~x) & (x | ~y | ~z)
    (x | ~y) & (x | ~z) & (y | z | ~x)
    (x | y) & (x | ~z) & (z | ~x | ~y)
    (x | y) & (~x | ~y)



```python
def tseitin2(Expr):
    #take as input the output of tseitin1: a conjuction of equivalence
    # replaces the equivalences by conjunction of disjunction of litterals
    result = Expr.args[0] #first arg is an atom by construction
    for i in Expr.args[1:]:
        op = i.args[1].func
        x = i.args[0]
        y =  i.args[1].args[0]
        if (op == Not):       
            result = result & (x | y) & (~x | ~y)
        else:
            z = i.args[1].args[1]
            if (op == And):
                result = result & (y | ~x) & (z | ~x) & (x | ~y | ~z)
            elif (op == Or):
                result = result & (x | ~y) & (x | ~z) & (y | z | ~x)
            elif (op == Implies):
                result = result & (x | y) & (x | ~z) & (z | ~x | ~y)
            else:
                print("error: unsupported operator")
    return result
```


```python
def tseitin(Expr):
    return tseitin2(tseitin1(Expr))
```


```python
F = ((p |q) & r) >> (~s)
print("original formula:", F)
T = tseitin1(F)
print("step 1: ", T)
c = tseitin2(T)
print("step 2: ", c)

```

    original formula: Implies(r & (p | q), ~s)
    step 1:  p4 & (Equivalent(p2, ~s)) & (Equivalent(p1, p | q)) & (Equivalent(p3, p1 & r)) & (Equivalent(p4, Implies(p3, p2)))
    step 2:  p4 & (p2 | s) & (p3 | p4) & (p1 | ~p) & (p1 | ~p3) & (p1 | ~q) & (p4 | ~p2) & (r | ~p3) & (~p2 | ~s) & (p | q | ~p1) & (p2 | ~p3 | ~p4) & (p3 | ~p1 | ~r)



```python

```


```python
tseitin(Not((A & B ) | C))
```




    p3 & (p2 | p3) & (A | ~p1) & (B | ~p1) & (p2 | ~C) & (p2 | ~p1) & (~p2 | ~p3) & (C | p1 | ~p2) & (p1 | ~A | ~B)




```python
tseitin((x1 & x2 & x3))
```




    p2 & (p1 | ~p2) & (x1 | ~p2) & (x2 | ~p1) & (x3 | ~p1) & (p1 | ~x2 | ~x3) & (p2 | ~p1 | ~x1)




```python
tseitin((x1 & x2) | (x3 & x4) | (x5 & x6))
```




    p5 & (p4 | ~p2) & (p4 | ~p3) & (p5 | ~p1) & (p5 | ~p4) & (x1 | ~p1) & (x2 | ~p1) & (x3 | ~p2) & (x4 | ~p2) & (x5 | ~p3) & (x6 | ~p3) & (p1 | p4 | ~p5) & (p2 | p3 | ~p4) & (p1 | ~x1 | ~x2) & (p2 | ~x3 | ~x4) & (p3 | ~x5 | ~x6)




```python
tseitin((x1 & x2) | (x3 & x4) | (x5 & x6)| (x7 & x8))
```




    p7 & (p5 | ~p3) & (p5 | ~p4) & (p6 | ~p2) & (p6 | ~p5) & (p7 | ~p1) & (p7 | ~p6) & (x1 | ~p1) & (x2 | ~p1) & (x3 | ~p2) & (x4 | ~p2) & (x5 | ~p3) & (x6 | ~p3) & (x7 | ~p4) & (x8 | ~p4) & (p1 | p6 | ~p7) & (p2 | p5 | ~p6) & (p3 | p4 | ~p5) & (p1 | ~x1 | ~x2) & (p2 | ~x3 | ~x4) & (p3 | ~x5 | ~x6) & (p4 | ~x7 | ~x8)



 Tseitin transformation of formula  (x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11) has 34 clauses of one, two or three litteral each, to be compared with the 64 clauses of 6 literals each of the classical CNF transformation


```python
tseitin((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))
```




    p11 & (p10 | ~p2) & (p10 | ~p9) & (p11 | ~p1) & (p11 | ~p10) & (p7 | ~p5) & (p7 | ~p6) & (p8 | ~p4) & (p8 | ~p7) & (p9 | ~p3) & (p9 | ~p8) & (x0 | ~p1) & (x1 | ~p1) & (x10 | ~p2) & (x11 | ~p2) & (x2 | ~p3) & (x3 | ~p3) & (x4 | ~p4) & (x5 | ~p4) & (x6 | ~p5) & (x7 | ~p5) & (x8 | ~p6) & (x9 | ~p6) & (p1 | p10 | ~p11) & (p2 | p9 | ~p10) & (p3 | p8 | ~p9) & (p4 | p7 | ~p8) & (p5 | p6 | ~p7) & (p1 | ~x0 | ~x1) & (p2 | ~x10 | ~x11) & (p3 | ~x2 | ~x3) & (p4 | ~x4 | ~x5) & (p5 | ~x6 | ~x7) & (p6 | ~x8 | ~x9)




```python
sp.to_cnf((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))
```




    (x0 | x10 | x2 | x4 | x6 | x8) & (x0 | x10 | x2 | x4 | x6 | x9) & (x0 | x10 | x2 | x4 | x7 | x8) & (x0 | x10 | x2 | x4 | x7 | x9) & (x0 | x10 | x2 | x5 | x6 | x8) & (x0 | x10 | x2 | x5 | x6 | x9) & (x0 | x10 | x2 | x5 | x7 | x8) & (x0 | x10 | x2 | x5 | x7 | x9) & (x0 | x10 | x3 | x4 | x6 | x8) & (x0 | x10 | x3 | x4 | x6 | x9) & (x0 | x10 | x3 | x4 | x7 | x8) & (x0 | x10 | x3 | x4 | x7 | x9) & (x0 | x10 | x3 | x5 | x6 | x8) & (x0 | x10 | x3 | x5 | x6 | x9) & (x0 | x10 | x3 | x5 | x7 | x8) & (x0 | x10 | x3 | x5 | x7 | x9) & (x0 | x11 | x2 | x4 | x6 | x8) & (x0 | x11 | x2 | x4 | x6 | x9) & (x0 | x11 | x2 | x4 | x7 | x8) & (x0 | x11 | x2 | x4 | x7 | x9) & (x0 | x11 | x2 | x5 | x6 | x8) & (x0 | x11 | x2 | x5 | x6 | x9) & (x0 | x11 | x2 | x5 | x7 | x8) & (x0 | x11 | x2 | x5 | x7 | x9) & (x0 | x11 | x3 | x4 | x6 | x8) & (x0 | x11 | x3 | x4 | x6 | x9) & (x0 | x11 | x3 | x4 | x7 | x8) & (x0 | x11 | x3 | x4 | x7 | x9) & (x0 | x11 | x3 | x5 | x6 | x8) & (x0 | x11 | x3 | x5 | x6 | x9) & (x0 | x11 | x3 | x5 | x7 | x8) & (x0 | x11 | x3 | x5 | x7 | x9) & (x1 | x10 | x2 | x4 | x6 | x8) & (x1 | x10 | x2 | x4 | x6 | x9) & (x1 | x10 | x2 | x4 | x7 | x8) & (x1 | x10 | x2 | x4 | x7 | x9) & (x1 | x10 | x2 | x5 | x6 | x8) & (x1 | x10 | x2 | x5 | x6 | x9) & (x1 | x10 | x2 | x5 | x7 | x8) & (x1 | x10 | x2 | x5 | x7 | x9) & (x1 | x10 | x3 | x4 | x6 | x8) & (x1 | x10 | x3 | x4 | x6 | x9) & (x1 | x10 | x3 | x4 | x7 | x8) & (x1 | x10 | x3 | x4 | x7 | x9) & (x1 | x10 | x3 | x5 | x6 | x8) & (x1 | x10 | x3 | x5 | x6 | x9) & (x1 | x10 | x3 | x5 | x7 | x8) & (x1 | x10 | x3 | x5 | x7 | x9) & (x1 | x11 | x2 | x4 | x6 | x8) & (x1 | x11 | x2 | x4 | x6 | x9) & (x1 | x11 | x2 | x4 | x7 | x8) & (x1 | x11 | x2 | x4 | x7 | x9) & (x1 | x11 | x2 | x5 | x6 | x8) & (x1 | x11 | x2 | x5 | x6 | x9) & (x1 | x11 | x2 | x5 | x7 | x8) & (x1 | x11 | x2 | x5 | x7 | x9) & (x1 | x11 | x3 | x4 | x6 | x8) & (x1 | x11 | x3 | x4 | x6 | x9) & (x1 | x11 | x3 | x4 | x7 | x8) & (x1 | x11 | x3 | x4 | x7 | x9) & (x1 | x11 | x3 | x5 | x6 | x8) & (x1 | x11 | x3 | x5 | x6 | x9) & (x1 | x11 | x3 | x5 | x7 | x8) & (x1 | x11 | x3 | x5 | x7 | x9)




```python

```

3ec46e696e4c8109005803b40c7e78ce29246a14
ipynb
Jupyter Notebook
Tseitin.ipynb
Emmanuel75/SAT-illustrations
b40eabe59d1c7c2f198f662290f3cb7ca438ba2d
MIT
Tseitin.ipynb
Emmanuel75/SAT-illustrations
b40eabe59d1c7c2f198f662290f3cb7ca438ba2d
MIT
Tseitin.ipynb
Emmanuel75/SAT-illustrations
b40eabe59d1c7c2f198f662290f3cb7ca438ba2d
MIT
Qwen/Qwen-72B
1. YES
2. YES