Merge pull request #4 from olarozenfeld/or-fork

Solve speedup ~7.5 times using key_variables

Author: olarozenfeld

WORKSPACE

@@ -106,9 +106,6 @@ cc_library(
 
 git_repository(
     name = "com_google_ortools",
-    #branch = "master",
-    commit = "525162feaadaeef640783b2eaea38cf4b623877f",
-    shallow_since = "1647023481 +0100",
-    #tag = "v9.3",
-    remote = "https://github.com/google/or-tools.git",
+    branch = "key-vars",  # My patch to OR-Tools for the key_variables feature.
+    remote = "https://github.com/olarozenfeld/or-tools.git",
 )

src/game_sat_solver.cc

@@ -1387,18 +1387,6 @@ void GameSatSolver::FillWorldFromSolverResponse(
 }
 
 SolverResponse GameSatSolver::Solve(const SolverRequest& request) {
-  switch (request.strategy()) {
-    case ITERATE_ROLE_ASSIGNMENTS:
-      return SolveIteration(request);
-    case EXPLORE_ALL_SOLUTIONS:
-      return SolveFull(request);
-    default:
-      return (g_.NumMinions() > 1 && g_.GetPerspective() != STORYTELLER ?
-              SolveIteration(request) : SolveFull(request));
-  }
-}
-
-SolverResponse GameSatSolver::SolveFull(const SolverRequest& request) {
   SolverResponse result;
   // Making a copy to add assumptions.
   const auto assumptions = CollectAssumptionLiterals(request.assumptions());
@@ -1413,13 +1401,19 @@ SolverResponse GameSatSolver::SolveFull(const SolverRequest& request) {
     WriteProtoToFile(cp_model.Build(), tmp_dir / "model.pbtxt");
   }
   CpSolverResponse response;
-  unordered_map<string, SolverResponse::World*> worlds_per_key;
   map<string, int> num_worlds_per_demon;
   int solutions = 0;
   operations_research::sat::Model model;
   SatParameters parameters;
   parameters.set_enumerate_all_solutions(!request.stop_after_first_solution());
   parameters.set_symmetry_level(0);  // Empirically, this is faster.
+  // We only care about current (and starting?) role assignments, so add them
+  // as key variables:
+  for (int i = 0; i < g_.NumPlayers(); ++i) {
+    for (Role role : AllRoles(script_)) {
+      parameters.add_key_variables(RoleVar(i, role, g_.CurrentTime()).index());
+    }
+  }
   model.Add(NewSatParameters(parameters));
   auto log_progress = [&](bool force) {
     string progress = absl::StrFormat("Found %d solutions ", solutions);
@@ -1440,14 +1434,10 @@ SolverResponse GameSatSolver::SolveFull(const SolverRequest& request) {
     SolverResponse::World cur_world;
     FillWorldFromSolverResponse(r, &cur_world);
     const int demon = SolutionAliveDemon(r);
-    const string key = cur_world.DebugString();
-    if (!worlds_per_key.contains(key)) {
-      worlds_per_key[key] = result.add_worlds();
-      *(worlds_per_key[key]) = cur_world;
-      const string demon_name =
-          demon == kNoPlayer ? "<Dead player>" : g_.PlayerName(demon);
-      num_worlds_per_demon[demon_name]++;
-    }
+    *(result.add_worlds()) = cur_world;
+    const string demon_name =
+        demon == kNoPlayer ? "<Dead player>" : g_.PlayerName(demon);
+    num_worlds_per_demon[demon_name]++;
     log_progress(false);
     if (debug_mode) {
       const path sat_filename = absl::StrFormat("sat_solution_%d", solutions);
@@ -1466,79 +1456,6 @@ SolverResponse GameSatSolver::SolveFull(const SolverRequest& request) {
   return result;
 }
 
-SolverResponse GameSatSolver::SolveIteration(const SolverRequest& request) {
-  SolverResponse result;
-  // Making a copy to add assumptions repeatedly.
-  const auto assumptions = CollectAssumptionLiterals(request.assumptions());
-  CpModelBuilder model(model_.Model());
-  model.AddBoolAnd(assumptions);
-  path tmp_dir = "./tmp";
-  path solution_dir = tmp_dir / "solutions";
-  const bool debug_mode = request.debug_mode();
-  if (debug_mode) {
-    // Create the ./tmp/solutions directory, if not present.
-    create_directories(solution_dir);
-    WriteProtoToFile(model.Build(), tmp_dir / "model.pbtxt");
-  }
-  CpSolverResponse response;
-  map<string, int> num_worlds_per_demon;
-  int solutions = 0;
-  while (true) {
-    response = operations_research::sat::Solve(model.Build());
-    CHECK(response.status() != CpSolverStatus::MODEL_INVALID);
-    if (response.status() == CpSolverStatus::UNKNOWN) {
-      LOG(WARNING) << "Solver was interrupted, returning partial solution";
-      break;
-    }
-    if (response.status() == CpSolverStatus::INFEASIBLE) {
-      break;
-    }
-    ++solutions;
-    if (debug_mode) {
-      const path resp_filename = absl::StrFormat("resp_%d.pbtxt", solutions);
-      WriteProtoToFile(response, solution_dir / resp_filename);
-    }
-    const int demon = SolutionAliveDemon(response);
-    SolverResponse::World *world = result.add_worlds();
-    FillWorldFromSolverResponse(response, world);
-    const string demon_name =
-        demon == kNoPlayer ? "<Dead player>" : g_.PlayerName(demon);
-    num_worlds_per_demon[demon_name]++;
-    vector<BoolVar> current;
-    for (int i = 0; i < g_.NumPlayers(); ++i) {
-      for (Role role : AllRoles(script_)) {
-        const BoolVar& current_i_role = RoleVar(i, role, g_.CurrentTime());
-        if (SolutionBooleanValue(response, current_i_role)) {
-          current.push_back(current_i_role);
-        }
-      }
-    }
-    string progress = absl::StrFormat("Found %d solutions ", solutions);
-    for (const auto& it : num_worlds_per_demon) {
-      absl::StrAppend(
-          &progress, absl::StrFormat("%s: %d ", it.first, it.second));
-    }
-    cout << progress << endl;
-    if (debug_mode) {
-      const path sat_filename = absl::StrFormat("sat_solution_%d", solutions);
-      model_.WriteSatSolutionToFile(response, solution_dir / sat_filename);
-      const path world_filename = absl::StrFormat("world_%d.pbtxt", solutions);
-      WriteProtoToFile(*world, solution_dir / world_filename);
-    }
-    if (request.stop_after_first_solution()) {
-      break;
-    }
-    // Limit further solutions to different role assignments.
-    model.AddBoolOr(Not(current));  // At least one literal is different.
-  }
-  for (const auto& it : num_worlds_per_demon) {
-    auto* ado = result.add_alive_demon_options();
-    ado->set_name(it.first);
-    ado->set_count(it.second);
-  }
-  return result;
-}
-
 // Solves the game and returns all valid worlds.
 SolverResponse Solve(const GameState& g) {
   return GameSatSolver(g).Solve();

src/game_sat_solver.h

@@ -211,13 +211,6 @@ class GameSatSolver {
                                    SolverResponse::World* world);
   int SolutionAliveDemon(const CpSolverResponse& response);
 
-  // Calls sat::Solve in a loop while updating the model.
-  SolverResponse SolveIteration(const SolverRequest& request);
-
-  // Calls sat::Solve once to iterate over all boolean solutions. Can be faster,
-  // but can also be prohibitively slow at this point.
-  SolverResponse SolveFull(const SolverRequest& request);
-
   const GameState& g_;  // Current game state.
   const Script script_;  // Part of g_, replicated for convenience.
   // Preprocessed game state variables.

src/solver.proto

@@ -17,20 +17,6 @@ package botc;
 
 import "src/game_log.proto";
 
-enum SolverStrategy {
-  // Will choose based on game size.
-  SOLVER_STRATEGY_UNSPECIFIED = 0;
-
-  // Will iteratively solve from scratch with the previously found role
-  // assignment disallowed. This is slow, but reliably slow.
-  ITERATE_ROLE_ASSIGNMENTS = 1;
-
-  // Will use the SAT solver to explore all SAT solutions and map them to role
-  // assignments. This is sometimes faster than the previous option, but can be
-  // prohibitively slow.
-  EXPLORE_ALL_SOLUTIONS = 2;
-}
-
 message SolverRequest {
   message Assumptions {
     message PlayerRole {
@@ -76,10 +62,6 @@ message SolverRequest {
   // variable assignment files alongside world assignments for each solution
   // under the "./tmp/" directory.
   bool debug_mode = 3;
-
-  // Which solver strategy to use. A default one tries to estimate which will be
-  // faster for the current game, but it may be wrong.
-  SolverStrategy strategy = 4;
 }
 
 message SolverResponse {