SATSolver.py

import sys
from copy import deepcopy
import re

assign_true = set()
assign_false = set()
n_props, n_splits = 0, 0


def print_cnf(cnf):
    s = ''
    for i in cnf:
        if len(i) > 0:
            s += '(' + i.replace(' ', '+') + ')'
    if s == '':
        s = '()'
    print(s)


def solve(cnf, literals):
    print('\nCNF = ', end='')
    print_cnf(cnf)
    new_true = []
    new_false = []
    global assign_true, assign_false, n_props, n_splits
    assign_true = set(assign_true)
    assign_false = set(assign_false)
    n_splits += 1
    cnf = list(set(cnf))
    units = [i for i in cnf if len(i)<3]
    units = list(set(units))
    if len(units):
        for unit in units:
            n_props += 1
            if '!' in unit:
                assign_false.add(unit[-1])
                new_false.append(unit[-1])
                i = 0
                while True:
                    if unit in cnf[i]:
                        cnf.remove(cnf[i])
                        i -= 1
                    elif unit[-1] in cnf[i]:
                        cnf[i] = cnf[i].replace(unit[-1], '').strip()
                    i += 1
                    if i >= len(cnf):
                        break
            else:
                assign_true.add(unit)
                new_true.append(unit)
                i = 0
                while True:
                    if '!'+unit in cnf[i]:
                        cnf[i] = cnf[i].replace('!'+unit, '').strip()
                        if '  ' in cnf[i]:
                            cnf[i] = cnf[i].replace('  ', ' ')
                    elif unit in cnf[i]:
                        cnf.remove(cnf[i])
                        i -= 1
                    i += 1
                    if i >= len(cnf):
                        break
    print('Units =', units)
    print('CNF after unit propogation = ', end = '')
    print_cnf(cnf)

    if len(cnf) == 0:
        return True

    if sum(len(clause)==0 for clause in cnf):
        for i in new_true:
            assign_true.remove(i)
        for i in new_false:
            assign_false.remove(i)
        print('Null clause found, backtracking...')
        return False
    literals = [k for k in list(set(''.join(cnf))) if k.isalpha()]

    x = literals[0]
    if solve(deepcopy(cnf)+[x], deepcopy(literals)):
        return True
    elif solve(deepcopy(cnf)+['!'+x], deepcopy(literals)):
        return True
    else:
        for i in new_true:
            assign_true.remove(i)
        for i in new_false:
            assign_false.remove(i)
        return False


def dpll():
    global assign_true, assign_false, n_props, n_splits
    input_cnf = open(sys.argv[1], 'r').read()
    literals = [i for i in list(set(input_cnf)) if i.isalpha()]
    cnf = input_cnf.splitlines()
    if solve(cnf, literals):
        print('\nNumber of Splits =', n_splits)
        print('Unit Propogations =', n_props)
        print('\nResult: SATISFIABLE')
        print('Solution:')
        for i in assign_true:
            print('\t\t'+i, '= True')
        for i in assign_false:
            print('\t\t'+i, '= False')
    else:
        print('\nReached starting node!')
        print('Number of Splitss =', n_splits)
        print('Unit Propogations =', n_props)
        print('\nResult: UNSATISFIABLE')
    print()

# New function to solve a single CNF at a time when called from the command line (must use "~" for negation)
def dpll(cnf_argument):
    global assign_true, assign_false, n_props, n_splits
    literals = [i for i in list(set(cnf_argument)) if i.isalpha()]
    if not re.match(r'^(\s*(!?[A-Z]\s*)+)$', cnf_argument):
        print('Invalid input format; please submit one formula at a time in CNF (e.g., ~A B ~C). Please try again.')
        return
    elif solve([cnf_argument], literals):
        print('\nNumber of Splits =', n_splits)
        print('Unit Propogations =', n_props)
        print('\nResult: SATISFIABLE')
        print('Solution:')
        for i in assign_true:
            print('\t\t'+i, '= True')
        for i in assign_false:
            print('\t\t'+i, '= False')
    else:
        print('\nReached starting node!')
        print('Number of Splitss =', n_splits)
        print('Unit Propogations =', n_props)
        print('\nResult: UNSATISFIABLE')
    print()

# Modified main function to allow for command line input
if __name__=='__main__':
    if len(sys.argv)==2:
        dpll()
    elif len(sys.argv)==3 and sys.argv[1] == 'solve':
        formula = sys.argv[2].replace("~", "!")
        print('Solving CNF:', formula)
        dpll(formula)