-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.py
115 lines (93 loc) · 2.84 KB
/
main.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
import os
import sys
import string
import re
from methodCNF import generateRowCNF, generateColumnCNF, generate3X3CNF, generatePrefilledCNF, generateIndivCNF
from utils import convertBase9
from subprocess import call
#-----parseFile(filename)-----#
#Purpose: encodes input file into one string
def parseFile(filename):
try:
open_file = open(filename)
except:
print("Error: File not found")
print("Unable to open file: " + filename)
sys.exit(-1)
content = open_file.readlines()
encodedLine = ""
for line in content:
encodedLine += ''.join(line.split())
encodedLine = encodedLine.replace('.', '*').replace('0', '*').replace('?', '*')
return encodedLine
#-----genGrid(filename)-----#
#Purpose: create a 2 by 2 array of the input puzzle
def genGrid(string):
arr = [[0 for x in range(9)] for x in range(9)]
for i in range(9):
for j in range(9):
arr[i][j] = string[ i * 9 + j ]
return arr
#-----MAIN-----#
#Purpose: Controls the main flow of the program
print("Starting the SAT Solver!\n")
if len(sys.argv) < 3:
print("Error: Incorrect arguments")
print("To run: python main.py <input> <minisat path>")
sys.exit(-1)
line = parseFile(sys.argv[1])
grid = genGrid(line) #generate grid
#generate minimal clauses
clauses = 0
f = open('tempOutput.txt', 'w')
clauses += generatePrefilledCNF(f, grid) #generate prefilled stuff
clauses += generateIndivCNF(f, grid) #generate individual stuff
clauses += generateColumnCNF(f, grid) #generate a list of columns
clauses += generateRowCNF(f, grid) #generate a list of rows
clauses += generate3X3CNF(f, grid) #generate a list of boxes (3x3)
f.close()
f = open('tempOutput.txt','r')
temp = f.read()
f.close()
f = open('tempOutput.txt', 'w')
f.write("p cnf 729 " + str(clauses) + "\n")
f.write(temp)
f.close()
# input into minisat
call([sys.argv[2], "tempOutput.txt", "SATOutput.txt"])
# Decode output file
f = open('SATOutput.txt','r')
sat = f.readline().strip()
print("\nInput puzzle:\n")
# print input puzzle
open_file = open("SolvedPuzzle.txt", 'w')
open_file.write("SAT Solver: Sudoku!\n\n")
open_file.write("\nInput puzzle:\n")
for x in range(0, 9):
line = ''
for y in range(0, 9):
line = line + grid[x][y] + " "
print(line + "\n")
open_file.write(line + "\n")
open_file.write("\n\n")
# output solved sudoku solver.
if(sat == 'SAT'):
print('\nProblem is Satisfiable!')
print('\nSolved Puzzle:\n')
numbers = f.readline()
asArr = numbers.split(' ')
for i in range(len(asArr)):
asArr[i] = int(asArr[i])
open_file.write("Solved Puzzle: \n")
for y in range(9):
line = ''
for x in range(9):
for z in range(9):
if(asArr[y*81 + 9*x + z] >= 0):
line = line + str(z + 1) + ' '
break
print(line + '\n')
open_file.write(line + '\n')
else:
print('\nProblem is unsatisfiable.')
open_file.write("'\nProblem is unsatisfiable.'")