pythonpython-3.xlogical-operatorsboolean-logiccnf

Convert formula to cnf python


I want to convert a formula to CNF. Is there a library to do this? This is my code. I created many function to convert any (a or b) to the CNF format.

But if there are many propositions, that will be hard like (a > b) & (c & d) or not(f) ..

operator="&|>=~"

def isOperand(c):
    return c >= 'a' and c <= 'z'

operators ="&|>=~"
def isOperator(c): #it cheak if the the given c is on the operators
 return c in operators
def dblimplique(a):
    if(a=='a = b' ):
       a='(a > b) & (b > a)'
    return a
def limplique(a):
    if(a=='a > b' ):
       a='~a | b'
    return a
def nonAouB(a):
    if(a=='~(a | b)' ):
       a='~a & ~b'
    return a
def nonAetB(a):
    if (a == '~(a & b)'):
        a = '~a | ~b'
    return a
def doublenon(a):
    if (a == '~~a'):
        a = 'a'
    return a
def doublenon(a):
    if (a == '~~a'):
        a = 'a'
    return a
def AetBouc(a):
    if (a == 'a & (b | c)'):
        a = '(a & b) | (a & c)'
    return a


def AouBetc(a):
    if (a == 'a | (b & c)'):
        a = '(a | b) & (a | c)'
    return a


def FNC():
    input_string = input("Entrer votre formule:")
    if(input_string == 'a = b'):
           return dblimplique(input_string)

    elif(input_string=='a > b'):
            return limplique(input_string)

    elif(input_string=='~(a | b)'):
            return  nonAouB(input_string)

    elif(input_string == '~(a & b)'):
            return nonAetB(input_string)

    elif(input_string =='~~a'):
            return  doublenon(input_string)
    elif(input_string =='a & (b | c)'):
        return AetBouc(input_string)
    elif(input_string=='a | (b & c)'):
        return AouBetc(input_string)
    elif(input_string=='a | b' or 'a | b | c' or 'a | b | c | d' or 'a | b | c | d'):
        return input_string
    else:
      for i in input_string:
          if(i == 'a > b' or 'c > d' or 'e > f'):
              return limplique(i)


print(FNC())

Solution

  • Use this module pip install sympy

    from sympy.logic.boolalg import to_cnf
    from sympy.abc import A, B, D
    to_cnf(~(A | B) | D)
    

    This is a good library :https://docs.sympy.org/latest/modules/logic.html

    These are two codes: https://github.com/ldkrsi/cnf_py

    https://github.com/omkarkarande/CNF-Converter