Hello friends, I have some trouble understanding the davis putnam algorithm for satisfiability. I understood most of the code but I don't know where exactly backtracking is happening here. Your assistance would be very helpful to me.
import sys import math import copy final_list = [] def sat(cnf): while( len(cnf) > 1 ): in_item = single_clause(cnf) #in_item: the first single_clause in cnf if in_item != None: del_sat(cnf, in_item) else: break for i in cnf: if len(i) == 0: cnf.remove(i) return if len(cnf) == 1: final_list.extend( [cnf[0][0]] ) # like a watchlist for i in range(0, len(final_list)): if final_list[i] > 0: print "Not equivalent!" sys.exit(0) return final_list deep_copy = copy.deepcopy(cnf) list2 = cnf[0][0] del_sat(deep_copy,list2) # recursion to delete and then find another way and the proceed or delete more like a tree sat(deep_copy) del_sat(cnf,-list2) sat(cnf) return def parseXml(file_1, file_2): global cnf readfile_1 = open(file_1, "r") readfile_2 = open(file_2, "r") sum_a = int(readfile_1.readline()) sum_b = int(readfile_2.readline()) inputs_1 = readfile_1.readline().split() inputs_1.sort() inputs_2 = readfile_2.readline().split() inputs_2.sort() outputs_1 = readfile_1.readline().split() outputs_1.sort() outputs_2 = readfile_2.readline().split() outputs_2.sort() inputmap_1 = {} inputmap_2 = {} outputmap_1 = [] outputmap_2 = [] while True: line = readfile_1.readline().strip() if not line: break net,item = line.split() inputmap_1[item] = int(net) while True: line = readfile_2.readline().strip() if not line: break net,item = line.split() inputmap_2[item] = int(net) #print inputmap_2 for line in readfile_1.readlines(): inp1 = line.split() gate = inp1.pop(0) mapping = map(int, inp1) outputmap_1.extend([(gate, mapping)]) print 'outputmap_1' print outputmap_1 for line in readfile_2.readlines(): inp2 = line.split() gate = inp2.pop(0) mapping = map(int, inp2) outputmap_2.extend([(gate, mapping)]) return inputs_1, inputs_2, outputs_1, outputs_2, inputmap_1, inputmap_2, outputmap_1, outputmap_2 def single_clause(cnf): for i in cnf: if len(i) == 1: return i[0] return None def del_sat(cnf,in_item): cnf2 = cnf[:] for k in cnf2: if k.count(in_item): cnf.remove(k) for i in cnf: if i.count( -in_item): i.remove(-in_item) def cnf_out(miter): miter_len = len(miter) cnf = [] while (miter_len > 0): x = miter.pop(0) if ( x[0] == "and" ): cnf.extend( [[x[1][0], -x[1][2]]] ) cnf.extend( [[x[1][1], -x[1][2]]] ) cnf.extend( [[-x[1][0], -x[1][1], x[1][2]]] ) elif ( x[0] == "or" ): cnf.extend( [[x[1][0], x[1][1], -x[1][2]]] ) cnf.extend( [[-x[1][0], x[1][2]]] ) cnf.extend( [[-x[1][1], x[1][2]]] ) elif ( x[0] == "xor" ): cnf.extend( [[x[1][0], x[1][1], -x[1][2]]] ) cnf.extend( [[-x[1][0], -x[1][1], -x[1][2]]] ) cnf.extend( [[-x[1][0], x[1][1], x[1][2]]] ) cnf.extend( [[x[1][0], -x[1][1], x[1][2]]] ) else: cnf.extend( [[x[1][0], x[1][1]]] ) cnf.extend( [[-x[1][0], -x[1][1]]] ) miter_len = miter_len - 1 return cnf inputs_1, inputs_2, outputs_1, outputs_2, inputmap_1, inputmap_2, outputmap_1, outputmap_2 = parseXml(sys.argv[1], sys.argv[2]) incoming1=[] incoming2=[] outgoing1=[] outgoing2=[] for i in inputs_1: incoming1.extend([inputmap_1[i]]) for j in inputs_2: incoming2.extend([inputmap_2[j]]) for k in outputs_1: outgoing1.extend([inputmap_1[k]]) for l in outputs_2: outgoing2.extend([inputmap_2[l]]) gate_num = 0 for output in outputmap_1: for j in output[1]: if gate_num < j: gate_num = j # gate_num: first line of netlist file. Total number of nets always need max no.. map2 = outputmap_2 num = len( map2 ) #No. of gates in netlist 2 for i in range(1, num + 1): j = len( map2[i-1][1] ) # Total No. of inputs and outputs of a gate for k in range(0, j): if map2[i-1][1][k] not in incoming2: total = 0 for l in incoming2: if map2[i-1][1][k] > l: total = total + 1 # Total no. of nets minus total no. of input nets like an offset map2[i-1][1][k] = map2[i-1][1][k] + gate_num - total else: x = incoming2.index( map2[i-1][1][k] ) map2[i-1][1][k] = incoming1[x] miter = outputmap_1 miter.extend(map2) #Combine gate lists of the two netlists to 'miter' out_len = len(outgoing1) #No. of outputs from each netlist (netlist1's out_len should be equal to netlist2's) for i in range(out_len): total = 0 for j in incoming2: # e.g: incoming2 = [1,2] if outgoing2[i] > j: # e.g outgoing2 = [10] total = total + 1 # should be the size of incoming2 outgoing2[i] = outgoing2[i] + gate_num - total xor_gate = [( 'xor', [outgoing1[i], outgoing2[i], 9000+i] )] miter.extend(xor_gate) if out_len > 1: or_gate_1 = [( 'or', [9000, 9000+1, 9000 + out_len] )] miter.extend(or_gate_1) for i in range(out_len - 2): or_gate=[( 'or', [9000 + out_len + i, 9000 +i + 2, 9000 + i + out_len + 1] )] miter.extend(or_gate) # 9000 just a random no. for the no. of nets used in order to prevent overlap of two nos. built_cnf = cnf_out(miter) count = 0 built_len = len(built_cnf) for i in range(0, built_len): built_leni = len(built_cnf[i]) for j in range(0, built_leni): if abs( built_cnf[i][j] ) > count: #count is the total number of nets in the miter circuit count = abs( built_cnf[i][j]) value = sat(built_cnf) print value print "Equivalent!" -- https://mail.python.org/mailman/listinfo/python-list