SAT Solver in Python

SAT Solver in Python Homework Sample

DIMACS CNF format allows you to specify a satisfiability problem. Clauses can be separated by AND or OR and you can invert a condition with NOT. Write a program to generate CNF clauses for a game of Suduko. Each cell contains a number between 1-9, each group of 3×3 contains each digit one, each horizontal and vertical line of 9 contains each digit. Write another program that takes in clauses and checks if they can be satisfied. For more Python programming assignments contact us for a quote.

Solution:

sudoku.py

#!/usr/bin/python3

import sys, getopt
#####################################################
#####################################################
# Please enter the number of hours you spent on this
# assignment here
# num_hours_i_spent_on_this_assignment = 0
#####################################################
#####################################################

#####################################################
#####################################################
# Give one short piece of feedback about the course so far. What
# have you found most interesting? Is there a topic that you had trouble
# understanding? Are there any changes that could improve the value of the
# course to you? (We will anonymize these before reading them.)
# <Your feedback goes here>
“””

“””
#####################################################
#####################################################

def main(argv):
inputfile = ”
N=0
try:
opts, args = getopt.getopt(argv,”hn:i:”,[“N=”,”ifile=”])
except getopt.GetoptError:
print (‘sudoku.py -n <size of Sodoku> -i <inputputfile>’)
sys.exit(2)
for opt, arg in opts:
if opt == ‘-h’:
print (‘sudoku.py -n <size of Sodoku> -i <inputputfile>’)
sys.exit()
elif opt in (“-n”, “–N”):
N = int(arg)
elif opt in (“-i”, “–ifile”):
inputfile = arg
instance = readInstance(N, inputfile)
toCNF(N,instance,inputfile+str(N)+”.cnf”)

def readInstance (N, inputfile):
if inputfile == ”:
return [[0 for j in range(N)] for i in range(N)]
with open(inputfile, “r”) as input_file:
instance =[]
for line in input_file:
number_strings = line.split() # Split the line on runs of whitespace
numbers = [int(n) for n in number_strings] # Convert to integers
if len(numbers) == N:
instance.append(numbers) # Add the “row” to your list.
else:
print(“Invalid Sudoku instance!”)
sys.exit(3)
return instance # a 2d list: [[1, 3, 4], [5, 5, 6]]

“”” Question 1 “””
def toCNF (N, instance, outputfile):
“”” Constructs the CNF formula C in Dimacs format from a sudoku grid.”””
“”” OUTPUT: Write Dimacs CNF to output_file “””
output_file = open(outputfile, “w”)
“*** YOUR CODE HERE ***”
clauses = []

for row in range(N):
for col in range(N):
# all values in main grid is on the solution:
if instance[row][col] != 0:
clauses.append(f'{N*N*row + N*col + instance[row][col]} 0′)
# make sure same cell will take onlt one value:
same_cell = [N*N*row + N*col + v for v in range(1, N+1) if v != instance[row][col]]
for ele in same_cell:
clauses.append(f’-{ele} 0′)
else:
cell = [N*N*row + N*col + v for v in range(1, N+1)]
# make sure every cell takes at least one value:
clauses.append(str(cell)[1: -1].replace(‘,’, ”)+’ 0′)
# make sure every cell takes at most one value:
for val in range(N):
for n_val in range(val+1, N):
clauses.append(f'{-cell[val]} {-cell[n_val]} 0′)

# make sure there’s no two cells in same row or column with same value:
rows = [N*N*col + N*cr + (row+1) for cr in range(N)]
cols = [N*N*cr + N*col + (row+1) for cr in range(N)]

for val in range(N):
for n_val in range(val+1, N):
clauses.append(f'{-rows[val]} {-rows[n_val]} 0′)
clauses.append(f'{-cols[val]} {-cols[n_val]} 0′)

# add first line:
clauses.insert(0, f’p cnf {N*N*N} {len(clauses)}’)
# write data in the file:
for line in clauses:
output_file.write(“%s\n” % line)
“*** YOUR CODE ENDS HERE ***”
output_file.close()
“*** YOUR CODE ENDS HERE ***”
output_file.close()

if __name__ == “__main__”:
main(sys.argv[1:])

DPLLsat.py

#!/usr/bin/python3

import sys, getopt

class SatInstance:
def __init__(self):
pass
def from_file(self, inputfile):
self.clauses = list()
self.VARS = set()
self.p = 0
self.cnf = 0
with open(inputfile, “r”) as input_file:
self.clauses.append(list())
maxvar = 0
for line in input_file:
tokens = line.split()
if len(tokens) != 0 and tokens[0] not in (“p”, “c”):
for tok in tokens:
lit = int(tok)
maxvar = max(maxvar, abs(lit))
if lit == 0:
self.clauses.append(list())
else:
self.clauses[-1].append(lit)
if tokens[0] == “p”:
self.p = int(tokens[2])
self.cnf = int(tokens[3])
assert len(self.clauses[-1]) == 0
self.clauses.pop()
if not (maxvar == self.p):
print(“Non-standard CNF encoding!”)
sys.exit(5)
# Variables are numbered from 1 to p
for i in range(1,self.p+1):
self.VARS.add(i)
def __str__(self):
s = “”
for clause in self.clauses:
s += str(clause)
s += “\n”
return s

def main(argv):
inputfile = ”
verbosity=False
inputflag=False
try:
opts, args = getopt.getopt(argv,”hi:v”,[“ifile=”])
except getopt.GetoptError:
print (‘DPLLsat.py -i <inputCNFfile> [-v] ‘)
sys.exit(2)
for opt, arg in opts:
if opt == ‘-h’:
print (‘DPLLsat.py -i <inputCNFfile> [-v]’)
sys.exit()
##-v sets the verbosity of informational output
## (set to true for output veriable assignments, defaults to false)
elif opt == ‘-v’:
verbosity = True
elif opt in (“-i”, “–ifile”):
inputfile = arg
inputflag = True
if inputflag:
instance = SatInstance()
instance.from_file(inputfile)
solve_dpll(instance, verbosity)
else:
print(“You must have an input file!”)
print (‘DPLLsat.py -i <inputCNFfile> [-v]’)

“”” Question 2 “””
# Finds a satisfying assignment to a SAT instance,
# using the DPLL algorithm.
# Input: a SAT instance and verbosity flag
# Output: print “UNSAT” or
# “SAT”
# list of true literals (if verbosity == True)
# list of false literals (if verbosity == True)
#
# You will need to define your own
# solve(VARS, F), pure-elim(F), propagate-units(F), and
# any other auxiliary functions
def deduction(F, unit):
deducted = []
for clause in F:
if unit in clause:
continue
if -unit in clause:
new_clause = [x for x in clause if x != -unit]
if not new_clause:
return -1
deducted.append(new_clause)
else:
deducted.append(clause)

return deducted

def propagate_units(F):
assignment = []
unit_clauses = [c for c in F if len(c) == 1]
while unit_clauses:
unit = unit_clauses[0]
F = deduction(F, unit[0])
assignment += [unit[0]]
if F == -1:
return -1, []
if not F:
return F, assignment
unit_clauses = [c for c in F if len(c) == 1]
return F, assignment

def pure_elim(F):
literals = set([lit for clause in F for lit in clause])
pures = []
assignment = []

for lit in literals:
if -lit not in literals:
pures.append(lit)

for pure in pures:
F = deduction(F, pure)

assignment += pures
return F, assignment

def solve(VARS, F, assignment):
F, pure_assignment = pure_elim(F)
F, unit_assignment = propagate_units(F)
assignment = assignment + unit_assignment + pure_assignment

if F == -1:
return []

if len(assignment) == len(VARS):
return assignment

lits = [abs(x) for clause in F for x in clause]
p = max(lits, key=lambda ele: lits.count(abs(ele)))

solution = solve(VARS, deduction(F, p), assignment+[p])
if not solution:
solution = solve(VARS, deduction(F, -p), assignment+[-p])

return solution

def solve_dpll(instance, verbosity):
#print(instance)
#print(instance.VARS)
#print(verbosity)
###########################################
# Start your code

solution = solve(instance.VARS, instance.clauses, [])

if not solution:
print(“UNSAT”)
else:
print(“SAT”)
if verbosity:
true_lit = []
false_lit = []
for lit in solution:
if lit == abs(lit):
true_lit.append(lit)
else:
false_lit.append(lit)

print(f”{str(true_lit)[1: -1].replace(‘,’, ”)}\n {str(false_lit)[1: -1].replace(‘,’, ”)}”)

# End your code
return True
###########################################

if __name__ == “__main__”:
main(sys.argv[1:])