Davis putnam algorithm for satisfiability...

Cameron Simpson cs at zip.com.au
Mon Aug 4 19:22:02 EDT 2014


On 04Aug2014 04:51, varun7rs at gmail.com <varun7rs at 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 <cs at 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



More information about the Python-list mailing list