From 3a1aee15027c012dd38c08041bc925ca8ecd27f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maximilian=20Ke=C3=9Fler?= Date: Wed, 10 May 2023 17:44:41 +0200 Subject: [PATCH] sat: fix equivalence of clue incrementation --- sat.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/sat.py b/sat.py index e3a689e..1866658 100644 --- a/sat.py +++ b/sat.py @@ -192,7 +192,7 @@ def solve_sat(starting_state: GameState | HanabiInstance) -> Tuple[bool, Optiona Iff(ls.play5[m], And(ls.play[m], Or(ls.discard[m][i] for i in range(instance.deck_size) if instance.deck[i].rank == 5))), # definition of ls.incr_clues - Iff(ls.incr_clues[m], And(ls.discard_any[m], Implies(ls.play[m], And(ls.play5[m], Not(ls.clues[m-1][8]))))), + Iff(ls.incr_clues[m], And(ls.discard_any[m], Not(ls.clues[m-1][8]), Implies(ls.play[m], ls.play5[m]))), # change of ls.clues *[Iff(ls.clues[m][i], Or(ls.clues[m-1][i+1], And(ls.clues[m-1][i], Or(ls.discard_any[m], ls.dummyturn[m])), And(ls.clues[m-1][i-1], ls.incr_clues[m]))) for i in range(1, 9)],