<jupyter_start><jupyter_text>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<jupyter_code>x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11 = symbols('x:12')<jupyter_output><empty_output><jupyter_text>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<jupyter_code>sp.to_cnf((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))<jupyter_output><empty_output><jupyter_text>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 excepted2. sort them by depth 3. Conjunct all substitutions and the substitution4. then transform all substitution in CNF  Step 1: computing $$((p \lor q) \land r) \implies \neg s$$ subformulas<jupyter_code>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"
subformulas(((p |q) & r) >> (~s))<jupyter_output><empty_output><jupyter_text>**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<jupyter_code>subformulas(A & B & C)<jupyter_output><empty_output><jupyter_text>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)<jupyter_code>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"
depth(((p |q) & r) >> (~s))<jupyter_output><empty_output><jupyter_text>Again we consider the boolen operator to be binary, so depth(A & B & C) = depth(A & (B & C))=2<jupyter_code>depth(A& B & C)<jupyter_output><empty_output><jupyter_text>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}$$<jupyter_code>F = ((p |q) & r) >> (~s)
sorted(subformulas(F), key=depth)<jupyter_output><empty_output><jupyter_text>We can now  write the following formulas$\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}$and conjunct them to get $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:<jupyter_code>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
si = symbol_init('t')
si() | si()<jupyter_output><empty_output><jupyter_text>As sympy boolean operator are n aries, sympy subs will not work well for us need. For instance<jupyter_code>(x1 & Not(x2) &x3).subs(Not(x2) & x3, A)<jupyter_output><empty_output><jupyter_text>So we need to define a custom substiturion handling boolean operator as binary<jupyter_code>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)
            
binSubs((x1 & ~x2 &x3), x1 & ~x2, A)<jupyter_output><empty_output><jupyter_text>We can now put together tseitin transformation<jupyter_code>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")   
F = ((p |q) & r) >> (~s)
tseitin1(F)
F2 = (~(p |~q) & r) >> (~s)
tseitin1(F2)<jupyter_output><empty_output><jupyter_text>From there, we leverage makes the final transformation to CNF leveraging the following equivalences $\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}$<jupyter_code>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)))
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
def tseitin(Expr):
    return tseitin2(tseitin1(Expr))
F = ((p |q) & r) >> (~s)
print("original formula:", F)
T = tseitin1(F)
print("step 1: ", T)
c = tseitin2(T)
print("step 2: ", c)

tseitin(Not((A & B ) | C))
tseitin((x1 & x2 & x3))
tseitin((x1 & x2) | (x3 & x4) | (x5 & x6))
tseitin((x1 & x2) | (x3 & x4) | (x5 & x6)| (x7 & x8))<jupyter_output><empty_output><jupyter_text>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<jupyter_code>tseitin((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))
sp.to_cnf((x0 & x1) | (x2 & x3) | (x4 & x5) | (x6 & x7)| (x8 & x9)| (x10 & x11))<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.15516420752022847, 'fraction_numerical': 0.024036173250832935, 'mean_word_length': 3.0564671814671813, 'pattern_counts': {'":': 0, '<': 53, '<?xml version=': 0, '>': 73, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 3, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '13', 'dir': 'jupyter-structured-clean-dedup', 'id': '622828', 'license': 'MIT', 'n_tokens_mistral': 3287, 'n_tokens_neox': 3139, 'n_words': 954, 'path': 'Tseitin.ipynb', 'repo_name': 'Emmanuel75/SAT-illustrations', 'size': '8404'}