-
Notifications
You must be signed in to change notification settings - Fork 0
/
sat_solver.py
97 lines (79 loc) · 3.16 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
import numpy as np
from variable import reset_calls, increment_calls, value_calls
from FORM import FORM, PROP
def naive_solve(formula):
props = list(formula.get_prop_set())#list of labels for props
assignment = {}
for i in range(2 ** len(props)):
assignment_array = sat_solver.num_to_vec_bitstring(i,len(props))
for ii in range(len(props)):
assignment[props[ii]] = (assignment_array[ii] == True)
if formula.evaluate(assignment):
return assignment
return 'UNSAT'
def tree_solve_random(formula):
props = list(formula.get_prop_set())
for bool in [True, False]:
assignment = {props[0]:bool}
set_result = formula.set(assignment)
#base case
if set_result == True:
return assignment
elif set_result == False:
continue
#recursive case
else: #isinstance(set_result, FORM):
result = tree_solve_random(set_result)
if isinstance(result, dict):
result.update({props[0]:bool})
result.update({key: False for key in list(set(props).difference(set(result.keys())))})
return result
return 'UNSAT'
def tree_solve(formula, unit_preference = False, two_clause = False, polarity = False):
increment_calls()
if isinstance(formula, PROP):
return {formula.label: formula.operator != 'NOT'}
prop, booleans = formula.heuristic_assignment(unit_preference,two_clause,polarity)
for bool in booleans:
assignment = {prop:bool}
set_result = formula.set(assignment)
#base case
if set_result == True:
return assignment
elif set_result == False:
continue
#recursive case
else: #isinstance(set_result, FORM):
result = tree_solve(set_result, unit_preference, two_clause, polarity)
if isinstance(result, dict):
result.update({prop:bool})
return result
return 'UNSAT'
class sat_solver():
def __init__(self) -> None:
pass
def num_to_vec_bitstring(number, width):
return np.array([int(i) for i in (list(np.binary_repr(number,width=width)))])
def find_unit(formula):#and formula of cnf form
if isinstance(formula,PROP):
return formula
for clause in formula.sub_formulas:
if clause.sub_formulas != None and len(clause.sub_formulas) == 1:
return clause.sub_formulas[0]
return None
def unit_assignment(formula):
if formula.operator == 'OR':
return False
unit = sat_solver.find_unit(formula)
if unit != None:
return {unit.label: unit.operator != 'NOT'}
return False
def find_contradiction(formula):
units = []
for clause in formula.sub_formulas:
if isinstance(clause, PROP):
label = clause.label if clause.operator != 'NOT' else -clause.label
if -label in units:
return True
units.append(label)
return False