On 04Aug2014 04:51, varun...@gmail.com <varun...@gmail.com> wrote:
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.
At a glance, in the bottom part of the sat(cnf) function.
The top part of the function performs some simple operations and possibly
returns.
The bottom part, executed if the earlier code does not return, copies cnf to
deep_copy, removes list2 from deep_copy and -list2 from cnf, and runs the sat()
function on each.
To my mind, that constitutes a backtrack: back up, and try a different way (on
the modified cnf and deep_copy).
Cheers,
Cameron Simpson <c...@zip.com.au>
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
--
https://mail.python.org/mailman/listinfo/python-list
