Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.python > #75683 > unrolled thread

Davis putnam algorithm for satisfiability...

Back to article view | Back to comp.lang.python

Contents

  Davis putnam algorithm for satisfiability... varun7rs@gmail.com - 2014-08-04 04:51 -0700
    Re: Davis putnam algorithm for satisfiability... Cameron Simpson <cs@zip.com.au> - 2014-08-05 09:22 +1000
      Re: Davis putnam algorithm for satisfiability... varun7rs@gmail.com - 2014-08-05 07:03 -0700
        Re: Davis putnam algorithm for satisfiability... Cameron Simpson <cs@zip.com.au> - 2014-08-07 09:09 +1000

#75683 — Davis putnam algorithm for satisfiability...

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

[toc] | [next] | [standalone]

#75713

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

[toc] | [prev] | [next] | [standalone]

#75740

Thank you Cameron. Your post was very helpful. If you don't mind I'd like to ask you the purpose of the final list in the very beginning of the code. It is being updated and then checked for the presence of a literal. If a literal is found it returns not equivalent. Could you brief me the use of a final list?

[toc] | [prev] | [next] | [standalone]

#75816

On 05Aug2014 07:03, varun7rs@gmail.com <varun7rs@gmail.com> wrote:
>Thank you Cameron. Your post was very helpful. If you don't mind I'd like to ask you the purpose of the final list in the very beginning of the code. It is being updated and then checked for the presence of a literal. If a literal is found it returns not equivalent. Could you brief me the use of a final list?

Not entirely, no. The python code is not very good, so the subtleties of the 
algorithm are harder to see on inspection. We can talk about those issues later 
if you like.

It looks to me as though this is a truncated version of the full algorithm. It 
is currently written to abort the whole program if it decides that the cnf is 
not satisfiable. Maybe.

In the (I am guessing hacked) code in your email, any single element sub-cnf 
has its components appended to the final_list and then the list is scanned for 
nonempty items; if one is found the whole program aborts. Otherwise the list 
itself is returned (and universally ignored, which is why I think this code is 
modified from a more complete original).

I think in the original the final_list is supposed to be a list of things to 
examine later, possibly a list of subexpressions not yet determined to be 
satisfiable. In this code it is never examined and you could possibly get away 
with a direct examination of cnf[0][0] at that point, ignoring final_list. The 
only reason I have any uncertainty is that the cnf trees get modified by the 
del_sat() function, and so I'm not sure that the stuff put on final_list is 
unchanged later.

So the short answer is: final_list is almost unused in this version of the code 
and could possibly be removed, but the code is sufficiently uncommented and 
clearly not the original algorithm, and the cnf structured modified in place, 
that I am not entirely sure.

It is further complicated by the fact that this is not just the davis-putnam 
algorithm on its own, it is that algorithm being used (I think) to compare two 
boolean logic circuits for equivalence, possibly by assembling a cnf 
representing circuit1 xor circuit2: if they are equivalent then I would expect 
that to be not satisfiable but I have not thought it through completely.

You'd better hope those two circuits have no loops; I would not expect the 
algorithm to be sufficient in the face of a loop.

Cheers,
Cameron Simpson <cs@zip.com.au>

If I had thought about it, I wouldn't have done the experiment.
The literature was full of examples that said you can't do this.
       --Spencer Silver on the work that led to the unique adhesives
         for 3-M "Post-It" Notepads.

[toc] | [prev] | [standalone]

Back to top | Article view | comp.lang.python

csiph-web