From 80f9e7bca551b0f8d91ad611b030476518b8101c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Tue, 28 Feb 2023 22:33:06 +0100 Subject: [PATCH] better function handling --- sat.py | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/sat.py b/sat.py index 05a0f9b..874201d 100644 --- a/sat.py +++ b/sat.py @@ -102,16 +102,16 @@ def solve(deck_str): ) 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) if model: # print_model(model, deck) - print(toJSON(model, deck)) - return True + solution = toJSON(model, deck) + return True, solution else: print('unsatisfiable') - return False + return False, None #conj = list(conjunctive_partition(constraints)) #print('statements: {}'.format(len(conj))) #ucore = get_unsat_core(conj) @@ -177,4 +177,6 @@ def toJSON(model, deck): } return json.dumps(game) -solve(deck_str) +solvable, sol = solve(deck_str) +if solvable: + print(sol)