better function handling

This commit is contained in:
Maximilian Keßler 2023-02-28 22:33:06 +01:00
parent aae9dec351
commit 80f9e7bca5
Signed by: max
GPG key ID: BCC5A619923C0BA5

12
sat.py
View file

@ -102,16 +102,16 @@ def solve(deck_str):
) )
constraints = And(*[valid_move(m) for m in range(MAX_MOVES)], win) constraints = And(*[valid_move(m) for m in range(MAX_MOVES)], win)
print('{} variables, {} nodes'.format(len(get_atoms(constraints)), get_formula_size(constraints))) print('Solving instance with {} variables, {} nodes'.format(len(get_atoms(constraints)), get_formula_size(constraints)))
model = get_model(constraints) model = get_model(constraints)
if model: if model:
# print_model(model, deck) # print_model(model, deck)
print(toJSON(model, deck)) solution = toJSON(model, deck)
return True return True, solution
else: else:
print('unsatisfiable') print('unsatisfiable')
return False return False, None
#conj = list(conjunctive_partition(constraints)) #conj = list(conjunctive_partition(constraints))
#print('statements: {}'.format(len(conj))) #print('statements: {}'.format(len(conj)))
#ucore = get_unsat_core(conj) #ucore = get_unsat_core(conj)
@ -177,4 +177,6 @@ def toJSON(model, deck):
} }
return json.dumps(game) return json.dumps(game)
solve(deck_str) solvable, sol = solve(deck_str)
if solvable:
print(sol)