update instance finder to new db. supports timeouts now
This commit is contained in:
parent
9f0f85b604
commit
673e5841a8
1 changed files with 103 additions and 91 deletions
|
@ -1,17 +1,24 @@
|
||||||
|
from typing import Optional
|
||||||
|
import pebble.concurrent
|
||||||
|
import concurrent.futures
|
||||||
|
|
||||||
|
import traceback
|
||||||
|
|
||||||
from sat import solve_sat
|
from sat import solve_sat
|
||||||
from database import conn
|
from database.database import conn, cur
|
||||||
from download_data import export_game
|
from download_data import detailed_export_game
|
||||||
from variants import VARIANTS, variant_name
|
|
||||||
from alive_progress import alive_bar
|
from alive_progress import alive_bar
|
||||||
from compress import decompress_deck, link
|
from compress import decompress_deck, link
|
||||||
import concurrent.futures
|
from hanabi import HanabiInstance
|
||||||
from threading import Lock
|
from threading import Lock
|
||||||
from time import perf_counter
|
from time import perf_counter
|
||||||
from greedy_solver import GameState, GreedyStrategy
|
from greedy_solver import GameState, GreedyStrategy
|
||||||
from log_setup.logger_setup import logger
|
from log_setup import logger
|
||||||
from deck_analyzer import analyze, InfeasibilityReason
|
from deck_analyzer import analyze, InfeasibilityReason
|
||||||
|
from variants import Variant
|
||||||
|
|
||||||
|
MAX_PROCESSES = 6
|
||||||
|
|
||||||
MAX_PROCESSES=4
|
|
||||||
|
|
||||||
def update_seeds_db():
|
def update_seeds_db():
|
||||||
cur2 = conn.cursor()
|
cur2 = conn.cursor()
|
||||||
|
@ -33,51 +40,45 @@ def update_seeds_db():
|
||||||
|
|
||||||
|
|
||||||
def get_decks_of_seeds():
|
def get_decks_of_seeds():
|
||||||
cur = conn.cursor()
|
|
||||||
cur2 = conn.cursor()
|
cur2 = conn.cursor()
|
||||||
cur.execute("SELECT seed FROM seeds WHERE deck is NULL")
|
cur.execute("SELECT seed, variant_id FROM seeds WHERE deck is NULL")
|
||||||
for (seed,) in cur:
|
for (seed, variant_id) in cur:
|
||||||
cur2.execute("SELECT id FROM games WHERE seed = (%s)", (seed,))
|
cur2.execute("SELECT id FROM games WHERE seed = (%s) LIMIT 1", (seed,))
|
||||||
(game_id,) = cur2.fetchone()
|
(game_id,) = cur2.fetchone()
|
||||||
print("Exporting game {} for seed {}.".format(game_id, seed))
|
logger.verbose("Exporting game {} for seed {}.".format(game_id, seed))
|
||||||
export_game(game_id)
|
detailed_export_game(game_id, var_id=variant_id, seed_exists=True)
|
||||||
conn.commit()
|
conn.commit()
|
||||||
|
|
||||||
|
|
||||||
def update_trivially_feasible_games():
|
def update_trivially_feasible_games(variant_id):
|
||||||
cur = conn.cursor()
|
variant: Variant = Variant.from_db(variant_id)
|
||||||
for var in VARIANTS:
|
cur.execute("SELECT seed FROM seeds WHERE variant_id = (%s) AND feasible is null", (variant_id,))
|
||||||
cur.execute("SELECT seed FROM seeds WHERE variant_id = (%s) AND feasible is null", (var['id'],))
|
seeds = cur.fetchall()
|
||||||
seeds = cur.fetchall()
|
print('Checking variant {} (id {}), found {} seeds to check...'.format(variant.name, variant_id, len(seeds)))
|
||||||
print('Checking variant {} (id {}), found {} seeds to check...'.format(var['name'], var['id'], len(seeds)))
|
|
||||||
|
|
||||||
with alive_bar(total=len(seeds), title='{} ({})'.format(var['name'], var['id'])) as bar:
|
|
||||||
for (seed,) in seeds:
|
|
||||||
cur.execute("SELECT id, deck_plays, one_extra_card, one_less_card, all_or_nothing "
|
|
||||||
"FROM games WHERE score = (%s) AND seed = (%s) ORDER BY id;",
|
|
||||||
(5 * len(var['suits']), seed)
|
|
||||||
)
|
|
||||||
res = cur.fetchall()
|
|
||||||
print("Checking seed {}: {:3} results".format(seed, len(res)))
|
|
||||||
for (game_id, a, b, c, d) in res:
|
|
||||||
if None in [a,b,c,d]:
|
|
||||||
print(' Game {} not found in database, exporting...'.format(game_id))
|
|
||||||
succ, valid = export_game(game_id)
|
|
||||||
if not succ:
|
|
||||||
print('Error exporting game {}.'.format(game_id))
|
|
||||||
continue
|
|
||||||
else:
|
|
||||||
valid = not any([a,b,c,d])
|
|
||||||
print(' Game {} already in database, valid: {}'.format(game_id, valid))
|
|
||||||
if valid:
|
|
||||||
print('Seed {:10} (variant {} / {}) found to be feasible via game {:6}'.format(seed, var['id'], var['name'], game_id))
|
|
||||||
cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (True, seed))
|
|
||||||
conn.commit()
|
|
||||||
break
|
|
||||||
else:
|
|
||||||
print(' Cheaty game found')
|
|
||||||
bar()
|
|
||||||
|
|
||||||
|
with alive_bar(total=len(seeds), title='{} ({})'.format(variant.name, variant_id)) as bar:
|
||||||
|
for (seed,) in seeds:
|
||||||
|
cur.execute("SELECT id, deck_plays, one_extra_card, one_less_card, all_or_nothing "
|
||||||
|
"FROM games WHERE score = (%s) AND seed = (%s) ORDER BY id;",
|
||||||
|
(variant.max_score, seed)
|
||||||
|
)
|
||||||
|
res = cur.fetchall()
|
||||||
|
logger.debug("Checking seed {}: {:3} results".format(seed, len(res)))
|
||||||
|
for (game_id, a, b, c, d) in res:
|
||||||
|
if None in [a, b, c, d]:
|
||||||
|
logger.debug(' Game {} not found in database, exporting...'.format(game_id))
|
||||||
|
detailed_export_game(game_id, var_id=variant_id)
|
||||||
|
else:
|
||||||
|
logger.debug(' Game {} already in database'.format(game_id, valid))
|
||||||
|
valid = not any([a, b, c, d])
|
||||||
|
if valid:
|
||||||
|
logger.verbose('Seed {:10} (variant {}) found to be feasible via game {:6}'.format(seed, variant_id, game_id))
|
||||||
|
cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (True, seed))
|
||||||
|
conn.commit()
|
||||||
|
break
|
||||||
|
else:
|
||||||
|
logger.verbose(' Cheaty game found')
|
||||||
|
bar()
|
||||||
|
|
||||||
|
|
||||||
def get_decks_for_all_seeds():
|
def get_decks_for_all_seeds():
|
||||||
|
@ -103,90 +104,101 @@ def get_decks_for_all_seeds():
|
||||||
|
|
||||||
mutex = Lock()
|
mutex = Lock()
|
||||||
|
|
||||||
def solve_instance(num_players, deck):
|
|
||||||
|
def solve_instance(instance: HanabiInstance):
|
||||||
# first, sanity check on running out of pace
|
# first, sanity check on running out of pace
|
||||||
result = analyze(deck, num_players)
|
result = analyze(instance)
|
||||||
if result is not None:
|
if result is not None:
|
||||||
assert type(result) == InfeasibilityReason
|
assert type(result) == InfeasibilityReason
|
||||||
logger.info("found infeasible deck")
|
logger.debug("found infeasible deck")
|
||||||
return False, None, None
|
return False, None, None
|
||||||
for num_remaining_cards in [0, 5, 10, 20, 30]:
|
for num_remaining_cards in [0, 20]:
|
||||||
# logger.info("trying with {} remaining cards".format(num_remaining_cards))
|
# logger.info("trying with {} remaining cards".format(num_remaining_cards))
|
||||||
game = GameState(num_players, deck)
|
game = GameState(instance)
|
||||||
strat = GreedyStrategy(game)
|
strat = GreedyStrategy(game)
|
||||||
|
|
||||||
# make a number of greedy moves
|
# make a number of greedy moves
|
||||||
while not game.is_over() and not game.is_known_lost():
|
while not game.is_over() and not game.is_known_lost():
|
||||||
if num_remaining_cards != 0 and game.progress == game.deck_size - num_remaining_cards:
|
if num_remaining_cards != 0 and game.progress == game.deck_size - num_remaining_cards:
|
||||||
break # stop solution here
|
break # stop solution here
|
||||||
strat.make_move()
|
strat.make_move()
|
||||||
|
|
||||||
# check if we won already
|
# check if we won already
|
||||||
if game.is_won():
|
if game.is_won():
|
||||||
# print("won with greedy strat")
|
# print("won with greedy strat")
|
||||||
return True, game, num_remaining_cards
|
return True, game, num_remaining_cards
|
||||||
|
|
||||||
# now, apply sat solver
|
# now, apply sat solver
|
||||||
if not game.is_over():
|
if not game.is_over():
|
||||||
logger.info("continuing greedy sol with SAT")
|
logger.debug("continuing greedy sol with SAT")
|
||||||
solvable, sol = solve_sat(game)
|
solvable, sol = solve_sat(game)
|
||||||
if solvable:
|
if solvable is None:
|
||||||
return True, sol, num_remaining_cards
|
return True, sol, num_remaining_cards
|
||||||
logger.info("No success with {} remaining cards, reducing number of greedy moves, failed attempt was: {}".format(num_remaining_cards, link(game.to_json())))
|
logger.debug(
|
||||||
# print("Aborting trying with greedy strat")
|
"No success with {} remaining cards, reducing number of greedy moves, failed attempt was: {}".format(
|
||||||
logger.info("Starting full SAT solver")
|
num_remaining_cards, link(game)))
|
||||||
game = GameState(num_players, deck)
|
# print("Aborting trying with greedy strat")
|
||||||
|
logger.debug("Starting full SAT solver")
|
||||||
|
game = GameState(instance)
|
||||||
a, b = solve_sat(game)
|
a, b = solve_sat(game)
|
||||||
return a, b, 99
|
return a, b, instance.draw_pile_size
|
||||||
|
|
||||||
|
|
||||||
def solve_seed(seed, num_players, deck_compressed, var_id):
|
@pebble.concurrent.process(timeout=150)
|
||||||
|
def solve_seed_with_timeout(seed, num_players, deck_compressed, var_name: Optional[str] = None):
|
||||||
try:
|
try:
|
||||||
|
logger.verbose("Starting to solve seed {}".format(seed))
|
||||||
deck = decompress_deck(deck_compressed)
|
deck = decompress_deck(deck_compressed)
|
||||||
t0 = perf_counter()
|
t0 = perf_counter()
|
||||||
solvable, solution, num_remaining_cards = solve_instance(num_players, deck)
|
solvable, solution, num_remaining_cards = solve_instance(HanabiInstance(deck, num_players))
|
||||||
t1 = perf_counter()
|
t1 = perf_counter()
|
||||||
logger.info("Solved instance {} in {} seconds".format(seed, round(t1-t0, 2)))
|
logger.verbose("Solved instance {} in {} seconds: {}".format(seed, round(t1 - t0, 2), solvable))
|
||||||
|
|
||||||
mutex.acquire()
|
mutex.acquire()
|
||||||
if solvable is not None:
|
if solvable is not None:
|
||||||
lcur = conn.cursor()
|
cur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (solvable, seed))
|
||||||
lcur.execute("UPDATE seeds SET feasible = (%s) WHERE seed = (%s)", (solvable, seed))
|
|
||||||
conn.commit()
|
conn.commit()
|
||||||
|
mutex.release()
|
||||||
|
|
||||||
if solvable == True:
|
if solvable == True:
|
||||||
with open("remaining_cards.txt", "a") as f:
|
logger.verbose("Success with {} cards left in draw by greedy solver on seed {}: {}\n".format(
|
||||||
f.write("Success with {} cards left in draw by greedy solver on seed {}: {}\n".format(num_remaining_cards, seed ,link(solution.to_json())))
|
num_remaining_cards, seed, link(solution))
|
||||||
|
)
|
||||||
elif solvable == False:
|
elif solvable == False:
|
||||||
logger.info("seed {} was not solvable".format(seed))
|
logger.debug("seed {} was not solvable".format(seed))
|
||||||
with open('infeasible_instances.txt', 'a') as f:
|
logger.debug('{}-player, seed {:10}, {}\n'.format(num_players, seed, var_name))
|
||||||
f.write('{}-player, seed {:10}, {}\n'.format(num_players, seed, variant_name(var_id)))
|
|
||||||
elif solvable is None:
|
elif solvable is None:
|
||||||
logger.info("seed {} skipped".format(seed))
|
logger.verbose("seed {} skipped".format(seed))
|
||||||
else:
|
else:
|
||||||
raise Exception("Programming Error")
|
raise Exception("Programming Error")
|
||||||
|
|
||||||
mutex.release()
|
except Exception as e:
|
||||||
except Exception:
|
|
||||||
traceback.format_exc()
|
|
||||||
print("exception in subprocess:")
|
print("exception in subprocess:")
|
||||||
|
traceback.print_exc()
|
||||||
|
|
||||||
|
|
||||||
def solve_unknown_seeds():
|
def solve_seed(seed, num_players, deck_compressed, var_name: Optional[str] = None):
|
||||||
cur = conn.cursor()
|
f = solve_seed_with_timeout(seed, num_players, deck_compressed, var_name)
|
||||||
for var in VARIANTS:
|
try:
|
||||||
cur.execute("SELECT seed, num_players, deck FROM seeds WHERE variant_id = (%s) AND feasible IS NULL AND deck IS NOT NULL", (var['id'],))
|
return f.result()
|
||||||
res = cur.fetchall()
|
except TimeoutError:
|
||||||
|
logger.verbose("Solving on seed {} timed out".format(seed))
|
||||||
# for r in res:
|
return
|
||||||
# solve_seed(r[0], r[1], r[2], var['id'])
|
|
||||||
|
|
||||||
with concurrent.futures.ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
|
|
||||||
fs = [executor.submit(solve_seed, r[0], r[1], r[2], var['id']) for r in res]
|
|
||||||
with alive_bar(len(res), title='Seed solving on {}'.format(var['name'])) as bar:
|
|
||||||
for f in concurrent.futures.as_completed(fs):
|
|
||||||
bar()
|
|
||||||
break
|
|
||||||
|
|
||||||
|
|
||||||
solve_unknown_seeds()
|
def solve_unknown_seeds(variant_id, variant_name: Optional[str] = None):
|
||||||
|
cur.execute("SELECT seed, num_players, deck FROM seeds WHERE variant_id = (%s) AND feasible IS NULL", (variant_id,))
|
||||||
|
res = cur.fetchall()
|
||||||
|
|
||||||
|
# for r in res:
|
||||||
|
# solve_seed(r[0], r[1], r[2], variant_name)
|
||||||
|
|
||||||
|
with concurrent.futures.ProcessPoolExecutor(max_workers=MAX_PROCESSES) as executor:
|
||||||
|
fs = [executor.submit(solve_seed, r[0], r[1], r[2], variant_name) for r in res]
|
||||||
|
with alive_bar(len(res), title='Seed solving on {}'.format(variant_name)) as bar:
|
||||||
|
for f in concurrent.futures.as_completed(fs):
|
||||||
|
bar()
|
||||||
|
|
||||||
|
|
||||||
|
update_trivially_feasible_games(0)
|
||||||
|
solve_unknown_seeds(0, "No Variant")
|
Loading…
Reference in a new issue