-
Notifications
You must be signed in to change notification settings - Fork 0
/
SAT_Solver.py
218 lines (174 loc) · 6.91 KB
/
SAT_Solver.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
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
'''
SAT Solver based on Davis–Putnam–Logemann–Loveland (DPLL) algorithm
Uses Jersolow-Wang 2-sided method (consider only positive literals)
Returns -
* SATISFIABLE followed by the model if the formula is satisfiable
* UNSATISFIABLE if the formula is unsatisfiable
'''
# Import necessary libraries
import argparse
import os
import textwrap
import time
# Parse the clauses in the input DIMACs file and store them in a list
def parse_dimacs(filename):
'''
Argument(s) : filename - name of the DIMACs CNF file
Return value : a tuple consisting of a list - the clauses in
the input file and the number of variables
'''
clauses = []
for line in open(filename):
if line.startswith('c'):
continue
if line.startswith('p'):
n_vars = line.split()[2] # Number of variables present
continue
clause = [int(x) for x in line[:-2].split()]
clauses.append(clause)
return clauses, int(n_vars)
# Jersolow-Wang 2-sided method considers only positive literals
# This is faster than Jersolow-Wang method by 50% improvement in speed
# Calculating Literal Weights
def get_weighted_abs_counter(formula, weight=2):
counter = {}
for clause in formula:
for literal in clause:
if abs(literal) in counter:
counter[abs(literal)] += weight ** -len(clause)
else:
counter[abs(literal)] = weight ** -len(clause)
return counter
# JW2S method implementation
def jeroslow_wang_2_sided(formula):
counter = get_weighted_abs_counter(formula)
return max(counter, key=counter.get)
# Boolean Constrain Propagation
# We set unit to true and so we need to update the cnf by the following rules:
# - Clauses that contain unit are removed (due to "or")
# - Update clauses by removing -unit from them if it exist (due to "or")
def bcp(formula, unit):
modified = []
for clause in formula:
if unit in clause:
continue
if -unit in clause:
new_clause = [x for x in clause if x != -unit]
# Base case: Conjunct containing an empty disjunct so False
# but we should continue later because there might be another path
if not new_clause:
return -1
modified.append(new_clause)
else:
modified.append(clause)
return modified
# The DPLL algorithm works by choosing an assignment of true or false
# for a variable, simplifying the formula based on that choice, then
# recursively checking the satisfiability of the simplified formula.
# Perform unit propagation - formula simplification
'''
If a clause is a unit clause (one with only one variable),
then the only way for the formula to be satisfiable is for
that variable to be assigned consistently with its sign in
that clause. Thus, we know that variable must take on that
assignment, which tells us that all other clauses with that
literal are now satisfied. In addition, we know that clauses
with the literal's negation will not be satisfied by that
component, so we can remove the negation from all clauses.
'''
def unit_propagation(formula):
assignment = []
unit_clauses = [c for c in formula if len(c) == 1]
# Iterate through all unit clauses
while unit_clauses:
unit = unit_clauses[0]
formula = bcp(formula, unit[0])
assignment += [unit[0]]
if formula == -1:
return -1, []
if not formula: # If no more unit clauses are present, return current formula
return formula, assignment
unit_clauses = [c for c in formula if len(c) == 1]
return formula, assignment
# Implement the DPLL algorithm - recursive backtracking
'''
The algorithm "guesses" a variable to be true, recursively
determines if that subproblem is satisfiable; if it is not,
the algorithm then "guesses" the variable to be false and
tries again.
'''
def backtracking(formula, assignment):
formula, unit_assignment = unit_propagation(formula)
assignment = assignment + unit_assignment
if formula == - 1:
return []
if not formula:
return assignment
variable = jeroslow_wang_2_sided(formula)
solution = backtracking(bcp(formula, variable), assignment + [variable])
# If no solution when assigning to True, try to assign to False
if not solution:
solution = backtracking(bcp(formula, -variable), assignment + [-variable])
return solution
##### Utilities function #####
# Benchmarks Tester
# Test a folder of CNF formulas and get the average time with the SAT-solver
def run_benchmarks(fname, folder):
print('Running on benchmarks...')
start_time = time.time() # Start the Timer
with open(fname, 'w') as out_file:
for filename in os.listdir(folder):
clauses, n_vars = parse_dimacs(os.path.join(folder, filename)) # Get the clauses
solution = backtracking(clauses, [])
out_file.write(filename + ' : ') # Write the filename for clarity
if solution:
solution += [x for x in range(1, n_vars + 1) if x not in solution and -x not in solution]
solution.sort(key=abs) # Sort based on absolute value
out_file.write('SAT')
out_file.write(' [')
for cl in solution:
out_file.write(f'{cl},')
out_file.write(']')
else:
out_file.write('UNSAT')
out_file.write('\n')
end_time = time.time() # Stop the Timer
print('Execution time: %.2f seconds' % (end_time - start_time))
# Main Function
def main():
# Command-line interfaces
parser = argparse.ArgumentParser(
formatter_class=argparse.RawDescriptionHelpFormatter,
description=textwrap.dedent('''\
SAT Solver based on DPLL Algorithm
-----------------------------------
Returns
1. A model if the formula is satisfiable
2. Reports that the formula is unsatisfiable'''))
parser.add_argument('--input_file', default=None,
help='runs the sat solver over the input file (must be in DIMACs format)')
parser.add_argument('--run_benchmarks', default=None,
help='runs the sat solver over all files in the input folder (provide only the folder name)')
args = parser.parse_args()
if args.run_benchmarks is not None:
# Runs the SAT Solver over all the files and creates a log
run_benchmarks('benchmarks-results.log', args.run_benchmarks)
elif args.input_file is not None:
f = args.input_file
assert os.path.exists(f), '{} does not exists'.format(f)
start_time = time.time() # Start the Timer
clauses, n_vars = parse_dimacs(f)
solution = backtracking(clauses, []) # Check for solution
if solution:
solution += [x for x in range(1, n_vars + 1) if x not in solution and -x not in solution]
solution.sort(key=abs)
print ('s SATISFIABLE')
print ('v ' + ' '.join([str(x) for x in solution]) + ' 0')
else:
print ('s UNSATISFIABLE')
end_time = time.time() # Stop the Timer
print('Execution time: %.2f seconds' % (end_time - start_time))
else:
print('Please either choose an input file or run the benchmarks. Type --help or --h for more details')
if __name__ == '__main__':
main()