Add Lexicographic + Pareto Optimizations (#6626)

Lexicographic optimizations: Optimize the objectives one-by-one, in the order they are pushed.
Pareto optimizations: Optimize the objectives to the extend that further optimization on any objective will worsen the other objective.
Units tests are of course added.

Lexicographic optimization is using iterative implementation, pretty similar to the naive box optimization.

3 files changed, 351 insertions, 3 deletions

diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index f73bc90b7..5f50c76c1 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -31,18 +31,26 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
       d_optChecker(),
       d_objectives(),
       d_results(),
-      d_objectiveCombination(BOX)
+      d_objectiveCombination(LEXICOGRAPHIC)
 {
 }
 
 OptimizationResult::ResultType OptimizationSolver::checkOpt()
 {
+  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+  {
+    // reset the optimization results
+    d_results[i] = OptimizationResult();
+  }
   switch (d_objectiveCombination)
   {
     case BOX: return optimizeBox(); break;
+    case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
+    case PARETO: return optimizeParetoNaiveGIA(); break;
     default:
-      Unimplemented()
-          << "Only BOX objective combination is supported in current version";
+      CVC5_FATAL()
+          << "Unknown objective combination, "
+          << "valid objective combinations are BOX, LEXICOGRAPHIC and PARETO";
   }
   Unreachable();
 }
@@ -150,5 +158,153 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
   return aggregatedResultType;
 }
 
+OptimizationResult::ResultType
+OptimizationSolver::optimizeLexicographicIterative()
+{
+  // resets the optChecker
+  d_optChecker = createOptCheckerWithTimeout(d_parent);
+  OptimizationResult partialResult;
+  std::unique_ptr<OMTOptimizer> optimizer;
+  for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+  {
+    optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]);
+    // checks if the objective is maximize or minimize
+    switch (d_objectives[i].getType())
+    {
+      case OptimizationObjective::MAXIMIZE:
+        partialResult = optimizer->maximize(d_optChecker.get(),
+                                            d_objectives[i].getTarget());
+        break;
+      case OptimizationObjective::MINIMIZE:
+        partialResult = optimizer->minimize(d_optChecker.get(),
+                                            d_objectives[i].getTarget());
+        break;
+      default:
+        CVC5_FATAL()
+            << "Optimization objective is neither MAXIMIZE nor MINIMIZE";
+    }
+
+    d_results[i] = partialResult;
+
+    // checks the optimization result of the current objective
+    switch (partialResult.getType())
+    {
+      case OptimizationResult::OPTIMAL:
+        // assert target[i] == value[i] and proceed
+        d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
+            kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
+        break;
+      case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED;
+      case OptimizationResult::UNSAT: return OptimizationResult::UNSAT;
+      case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN;
+      default: Unreachable();
+    }
+  }
+  // kill optChecker in case pareto misuses it
+  d_optChecker.reset();
+  // now all objectives are OPTIMAL, just return OPTIMAL as overall result
+  return OptimizationResult::OPTIMAL;
+}
+
+OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
+{
+  // initial call to Pareto optimizer, create the checker
+  if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
+  NodeManager* nm = d_optChecker->getNodeManager();
+
+  // checks whether the current set of assertions are satisfied or not
+  Result satResult = d_optChecker->checkSat();
+
+  switch (satResult.isSat())
+  {
+    case Result::Sat::UNSAT: return OptimizationResult::UNSAT;
+    case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN;
+    case Result::Sat::SAT:
+    {
+      // if satisfied, use d_results to store the initial results
+      // they will be gradually updated and optimized
+      // until no more optimal value could be found
+      for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+      {
+        d_results[i] = OptimizationResult(
+            OptimizationResult::OPTIMAL,
+            d_optChecker->getValue(d_objectives[i].getTarget()));
+      }
+      break;
+    }
+    default: Unreachable();
+  }
+
+  // a vector storing assertions saying that no objective is worse
+  std::vector<Node> noWorseObj;
+  // a vector storing assertions saying that there is at least one objective
+  // that could be improved
+  std::vector<Node> someObjBetter;
+  d_optChecker->push();
+
+  while (satResult.isSat() == Result::Sat::SAT)
+  {
+    noWorseObj.clear();
+    someObjBetter.clear();
+
+    for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+    {
+      // for maximize value[i] <= obj[i],
+      // for minimize obj[i] <= value[i]
+      noWorseObj.push_back(
+          OMTOptimizer::mkWeakIncrementalExpression(nm,
+                                                    d_objectives[i].getTarget(),
+                                                    d_results[i].getValue(),
+                                                    d_objectives[i]));
+      // for maximize value[i] < obj[i],
+      // for minimize obj[i] < value[i]
+      someObjBetter.push_back(OMTOptimizer::mkStrongIncrementalExpression(
+          nm,
+          d_objectives[i].getTarget(),
+          d_results[i].getValue(),
+          d_objectives[i]));
+    }
+    d_optChecker->assertFormula(nm->mkAnd(noWorseObj));
+    d_optChecker->assertFormula(nm->mkOr(someObjBetter));
+    // checks if previous assertions + noWorseObj + someObjBetter are satisfied
+    satResult = d_optChecker->checkSat();
+
+    switch (satResult.isSat())
+    {
+      case Result::Sat::UNSAT:
+        // if result is UNSAT, it means no more improvement could be made,
+        // then the results stored in d_results are one of the Pareto optimal
+        // results
+        break;
+      case Result::Sat::SAT_UNKNOWN:
+        // if result is UNKNOWN, abort the current session and return UNKNOWN
+        d_optChecker.reset();
+        return OptimizationResult::UNKNOWN;
+      case Result::Sat::SAT:
+      {
+        // if result is SAT, update d_results to the more optimal values
+        for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
+        {
+          d_results[i] = OptimizationResult(
+              OptimizationResult::OPTIMAL,
+              d_optChecker->getValue(d_objectives[i].getTarget()));
+        }
+        break;
+      }
+      default: Unreachable();
+    }
+  }
+
+  d_optChecker->pop();
+
+  // before we return:
+  // assert that some objective could be better
+  // in order not to get the same optimal solution
+  // for the next run.
+  d_optChecker->assertFormula(nm->mkOr(someObjBetter));
+
+  return OptimizationResult::OPTIMAL;
+}
+
 }  // namespace smt
 }  // namespace cvc5
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 0a1883737..b0f4de1c5 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -195,6 +195,9 @@ class OptimizationSolver
 
   /**
    * Run the optimization loop for the pushed objective
+   * For multiple objective combination, it defaults to lexicographic,
+   * and combination could be set by calling
+   *   setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO)
    */
   OptimizationResult::ResultType checkOpt();
 
@@ -250,6 +253,39 @@ class OptimizationSolver
    **/
   OptimizationResult::ResultType optimizeBox();
 
+  /**
+   * Optimize multiple goals in Lexicographic order,
+   * using iterative implementation
+   * @return OPTIMAL if all objectives are OPTIMAL and bounded;
+   *   UNBOUNDED if one of the objectives is UNBOUNDED
+   *     and optimization will stop at that objective;
+   *   UNSAT if one of the objectives is UNSAT
+   *     and optimization will stop at that objective;
+   *   UNKNOWN if one of the objectives is UNKNOWN
+   *     and optimization will stop at that objective;
+   *   If the optimization is stopped at an objective,
+   *     all objectives following that objective will be UNKNOWN.
+   **/
+  OptimizationResult::ResultType optimizeLexicographicIterative();
+
+  /**
+   * Optimize multiple goals in Pareto order
+   * Using a variant of linear search called Guided Improvement Algorithm
+   * Could be called multiple times to iterate through the Pareto front
+   *
+   * Definition:
+   * Pareto front: Set of all possible Pareto optimal solutions
+   *
+   * Reference:
+   * D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
+   *  Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
+   *
+   * @return if it finds a new Pareto optimal result it will return OPTIMAL;
+   *   if it exhausts the results in the Pareto front it will return UNSAT;
+   *   if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN.
+   **/
+  OptimizationResult::ResultType optimizeParetoNaiveGIA();
+
   /** A pointer to the parent SMT engine **/
   SmtEngine* d_parent;
 
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 3bffc9af1..ed3de10a9 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -84,5 +84,161 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
             BitVector(32u, (unsigned)0xFFFFFFFF));
 }
 
+TEST_F(TestTheoryWhiteOptMultigoal, lex)
+{
+  d_smtEngine->resetAssertions();
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+  Node y = d_nodeManager->mkVar(*d_BV32Type);
+  Node z = d_nodeManager->mkVar(*d_BV32Type);
+
+  // 18 <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(
+      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+
+  // y <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+  OptimizationSolver optSolver(d_smtEngine.get());
+
+  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
+
+  // minimize x
+  optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false);
+  // maximize y with `signed` comparison over bit-vectors.
+  optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true);
+  // maximize z
+  optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false);
+
+  OptimizationResult::ResultType r = optSolver.checkOpt();
+
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+
+  std::vector<OptimizationResult> results = optSolver.getValues();
+
+  // x == 18
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // y == 18
+  ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // z == 0xFFFFFFFF
+  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+            BitVector(32u, (unsigned)0xFFFFFFFF));
+}
+
+TEST_F(TestTheoryWhiteOptMultigoal, pareto)
+{
+  d_smtEngine->resetAssertions();
+  TypeNode bv4ty(d_nodeManager->mkBitVectorType(4u));
+  Node a = d_nodeManager->mkVar(bv4ty);
+  Node b = d_nodeManager->mkVar(bv4ty);
+
+  Node bv1 = d_nodeManager->mkConst(BitVector(4u, 1u));
+  Node bv2 = d_nodeManager->mkConst(BitVector(4u, 2u));
+  Node bv3 = d_nodeManager->mkConst(BitVector(4u, 3u));
+
+  std::vector<Node> stmts = {
+      // (and (= a 1) (= b 1))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
+      // (and (= a 2) (= b 1))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv2),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
+      // (and (= a 1) (= b 2))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
+      // (and (= a 2) (= b 2))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv2),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv2)),
+      // (and (= a 3) (= b 1))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv3),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv1)),
+      // (and (= a 1) (= b 3))
+      d_nodeManager->mkNode(kind::AND,
+                            d_nodeManager->mkNode(kind::EQUAL, a, bv1),
+                            d_nodeManager->mkNode(kind::EQUAL, b, bv3)),
+  };
+  /*
+  (assert (or
+    (and (= a 1) (= b 1))
+    (and (= a 2) (= b 1))
+    (and (= a 1) (= b 2))
+    (and (= a 2) (= b 2))
+    (and (= a 3) (= b 1))
+    (and (= a 1) (= b 3))
+  ))
+  */
+  d_smtEngine->assertFormula(d_nodeManager->mkOr(stmts));
+
+  /*
+    (maximize a)
+    (maximize b)
+   */
+  OptimizationSolver optSolver(d_smtEngine.get());
+  optSolver.setObjectiveCombination(OptimizationSolver::PARETO);
+  optSolver.pushObjective(a, OptimizationObjective::MAXIMIZE);
+  optSolver.pushObjective(b, OptimizationObjective::MAXIMIZE);
+
+  OptimizationResult::ResultType r;
+
+  // all possible result pairs <a, b>
+  std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
+      {1, 3}, {2, 2}, {3, 1}};
+
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  std::vector<OptimizationResult> results = optSolver.getValues();
+  std::pair<uint32_t, uint32_t> res = {
+      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
+      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
+  for (auto& rn : results)
+  {
+    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
+              << " ";
+  }
+  std::cout << std::endl;
+  ASSERT_EQ(possibleResults.count(res), 1);
+  possibleResults.erase(res);
+
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  res = {
+      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
+      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
+  for (auto& rn : results)
+  {
+    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
+              << " ";
+  }
+  std::cout << std::endl;
+  ASSERT_EQ(possibleResults.count(res), 1);
+  possibleResults.erase(res);
+
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  res = {
+      results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
+      results[1].getValue().getConst<BitVector>().toInteger().toUnsignedInt()};
+  for (auto& rn : results)
+  {
+    std::cout << rn.getValue().getConst<BitVector>().toInteger().toUnsignedInt()
+              << " ";
+  }
+  std::cout << std::endl;
+  ASSERT_EQ(possibleResults.count(res), 1);
+  possibleResults.erase(res);
+
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::UNSAT);
+  ASSERT_EQ(possibleResults.size(), 0);
+}
+
 }  // namespace test
 }  // namespace cvc5