Davis putnam algorithm for satisfiability...
varun7rs at gmail.com
varun7rs at gmail.com
Mon Aug 4 07:51:14 EDT 2014
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!"
More information about the Python-list
mailing list