-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathconvert2CNF.py
168 lines (147 loc) · 4.91 KB
/
convert2CNF.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
import sys
import copy
import subprocess
count = 0
def parse_file(filepath):
# read the layout file to the board array
board = []
fin = open(filepath)
file_content = fin.readline().strip().split('\n')
#print file_content
board_config = file_content[0].split(' ')
row = int(board_config[0])
col = int(board_config[1])
#print "Row : Col " + str(row) + " " + str(col)
board = [[0 for x in range(col)] for x in range(row)]
for i in range(row):
line = fin.readline().strip().split('\n')
nos = line[0].split(',')
#print line
for j in range(col):
token = nos[j]
if token == 'X':
token = -1
token = int(token)
#print token
#print i,j
board[i][j] = token
fin.close()
return board,row,col
def find_all_clauses(input_array,
input_len,
combi_len,
indi_tup,
ans_index,
next_start,
clause_tup):
global count
for iter in range(next_start,input_len+1):
#print "Combi len " + str(combi_len)
if combi_len <= 0:
clause_tup.append(copy.copy(indi_tup))
count = count + 1
return
#print "Ans index " + str(ans_index) + "Iter " + str(iter)
indi_tup[ans_index] = input_array[iter]
find_all_clauses(input_array,
input_len,
combi_len-1,
indi_tup,
ans_index + 1,
iter + 1,
clause_tup)
def find_cell_no(i, j, row, col):
return i*col + j + 1
def find_adjacent_cells(board, i, j, row, col):
output = []
if i >= 1 and j >= 1:
output.append(find_cell_no(i-1,j-1,row,col))
if i >= 1:
output.append(find_cell_no(i-1,j,row,col))
if i >= 1 and j < (col - 1):
output.append(find_cell_no(i-1,j+1,row,col))
if j < (col - 1):
output.append(find_cell_no(i,j+1,row,col))
if i < (row - 1) and j < (col - 1):
output.append(find_cell_no(i+1,j+1,row,col))
if i < (row - 1):
output.append(find_cell_no(i+1,j,row,col))
if i < (row - 1) and j >= 1:
output.append(find_cell_no(i+1,j-1,row,col))
if j >= 1:
output.append(find_cell_no(i,j-1,row,col))
return output
def convert2CNF(board, row, col, output):
# interpret the number constraints
global count
count_clause = 0
fout = open(output, 'w')
ftemp = open("temp", 'w')
for i in range(row):
for j in range(col):
if board[i][j] != -1:
first_adjacent_cells = find_adjacent_cells(board, i ,j,
row, col)
count_adj = len(first_adjacent_cells)
if ((board[i][j] > count_adj) or (board[i][j] < -1)):
print "Invalid board at postion Row: " + str(i) + " Col: " + str(j) + " !!!"
sys.exit(1)
first_adjacent_cells.append(0)
#input_array = [0,1,2,3,4,0]
#print "Adjacent cells = " + str(first_adjacent_cells)
#print "Count = " + str(count_adj)
#sys.exit(1);
indi_tup = []
for k in range(board[i][j] + 1):
indi_tup.append(0);
#print indi_tup
first_tup = []
count = 0
find_all_clauses(first_adjacent_cells,count_adj,board[i][j]+1,indi_tup,0,0,first_tup)
#print "Clause tuple " + str(first_tup)
#print "Count " + str(count)
count_clause = count_clause + count
for k in range(len(first_tup)):
for l in range(board[i][j] + 1):
ftemp.write(str(-1*first_tup[k][l]) + " ")
ftemp.write("0\n")
#sys.exit(1)
indi_tup = []
for k in range(count_adj - board[i][j] + 1):
indi_tup.append(0);
#print indi_tup
count = 0
second_tup = []
find_all_clauses(first_adjacent_cells,count_adj,count_adj-board[i][j]+1,indi_tup,0,0,second_tup)
#print "Second clause tuple " + str(second_tup)
#print "Second Count " + str(count)
count_clause = count_clause + count
for k in range(len(second_tup)):
for l in range(count_adj-board[i][j] + 1):
ftemp.write(str(second_tup[k][l]) + " ")
ftemp.write("0\n")
#print "Count clause = " + str(count_clause)
#sys.exit(1)
else:
ftemp.write(str(find_cell_no(i,j,row,col)) + " 0\n")
count_clause = count_clause + 1
ftemp.close()
fout.write("c This file is generated by python program in CNF form for SAT evaluation\n")
fout.write("p cnf " + str(row*col) + " " + str(count_clause) + "\n")
fclause = open("temp", 'r')
fout.write(fclause.read())
fclause.close()
fout.close()
subprocess.call(["rm","temp"])
subprocess.call(["/home/neeraj/Artificial_Intelligence/minisat/core/minisat","cnf","SAT_OUTPUT"])
print "The status of variables after SAT evaluation is:"
subprocess.call(["cat","SAT_OUTPUT"])
subprocess.call(["rm","SAT_OUTPUT"])
if __name__ == '__main__':
if len(sys.argv) < 3:
print 'Layout or output file not specified.'
exit(-1)
board,row,col = parse_file(sys.argv[1])
#print "Row : Col " + str(row) + " " + str(col)
#print "Input array is : " + str(board)
convert2CNF(board, row, col, sys.argv[2])