Initial Commit

Author: safwankdb

README.md

@@ -0,0 +1,70 @@
+# SAT Solver using DPLL
+
+This code was for assignment for the course **EE677: Foundations of VLSI CAD** at IIT Bombay. The code attempts to solve a satisfiabilty problem in Conjuctive Normal Form (CNF). If the problem is satisfiable, one possible solution is returned.
+
+## Algorithm
+The code is written in Python 3, it might not be compatible with previous versions. I have used DPLL Algorithm to solve the SAT problem. The problem is defined in CNF form. The algorithm can be explained by the following pseudocode.
+
+```python
+def solve_dpll(cnf)
+    while(cnf has a unit clause {X}):
+        delete clauses contatining {X}
+        delete {!X} from all clauses
+    if null clause exists:
+        return False
+    if CNF is null:
+        return True
+    select a literal {X}
+    cnf1 = cnf + {X}
+    cnf2 = cnf + {!X}
+    return solve_dpll(cnf1)+solve_dpll(cnf2)
+```
+
+## How to Use
+- Please write the CNF form problem in a text file in the following way.
+- For Example: (!B+A+!C)(B+A+!C)(!B+!A+!C)(B)(C) will be written as
+
+```
+!B A !C
+B A !C
+!B !A !C
+B
+C
+```
+- Save it in \<filename\> (example input.txt).
+- Run the following command
+```bash
+python3 DPLL.py <filename>
+```
+```
+python3 DPLL.py input.txt
+```
+
+
+
+
+## Example
+For CNF = (!B+A+!C)(B+A+!C)(!B+!A+!C)(B)(C), we get
+```bash
+
+CNF = (!B+A+!C)(B+A+!C)(!B+!A+!C)(B)(C)
+Units = ['C', 'B']
+CNF after unit propogation = (!A)(A)
+
+CNF = (!A)(A)(A)
+Units = ['!A', 'A']
+CNF after unit propogation = ()
+Null clause found, backtracking...
+
+CNF = (!A)(A)(!A)
+Units = ['!A', 'A']
+CNF after unit propogation = ()
+Null clause found, backtracking...
+
+Reached starting node!
+Number of Splitss = 3
+Unit Propogations = 6
+
+Result: UNSATISFIABLE
+
+```

SATSolver.py

@@ -0,0 +1,113 @@
+import sys
+from copy import deepcopy
+
+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()
+
+if __name__=='__main__':
+    dpll()

sampleCNF/7-20.txt

@@ -0,0 +1,8 @@
+!A B E
+A !B
+A !E
+!E D
+!C !F !B
+!E B
+!B F
+!B C

sampleCNF/input.txt

@@ -0,0 +1,4 @@
+A B C
+A !B C
+!A B !C
+!C

sampleCNF/output.txt

@@ -0,0 +1,3 @@
+B C !B
+C D !D
+!A !C !D

sampleCNF/sample1.txt

@@ -0,0 +1,5 @@
+!B A !C
+B A !C
+!B !A !C
+B
+C

sampleCNF/sample2.txt

@@ -0,0 +1,5 @@
+!A B
+!B !C
+C !D
+!D A
+A B !C

sampleCNF/sample3.txt

@@ -0,0 +1,5 @@
+A B !C !D
+D !C !A
+B C D
+C !D
+!A !B C