Davis putnam algorithm for satisfiability...

[varun7rs at gmail.com]

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!"