Hanabi/Py-Hanabi
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

set z3 as default solver because it is fastest

Browse source
This commit is contained in:
Maximilian Keßler 2024-11-23 15:32:36 +01:00
parent 898d8ed88c
commit 1027184c59
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/hanabi/solvers/sat.py
View file

@ -328,7 +328,7 @@ def solve_sat(starting_state: hanab_game.GameState | hanab_game.HanabiInstance,
constraints = And(*[valid_move(m) for m in range(first_turn, instance.max_winning_moves)], win) constraints = And(*[valid_move(m) for m in range(first_turn, instance.max_winning_moves)], win)
# print('Solving instance with {} 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, solver_name="z3")
if model: if model:
log_model(model, game_state, ls) log_model(model, game_state, ls)
solution = evaluate_model(model, copy.deepcopy(game_state), ls) solution = evaluate_model(model, copy.deepcopy(game_state), ls)