From ba90594ea59be5cfbcbfe81cf9510dab1efc3130 Mon Sep 17 00:00:00 2001 From: mcjuneho <63680275+mcjuneho@users.noreply.github.com> Date: Fri, 5 Mar 2021 11:51:23 -0800 Subject: [PATCH] Initial implementation of an optimization solver with unit tests. (#5849) --- src/CMakeLists.txt | 2 + src/smt/optimization_solver.cpp | 137 ++++++++++++++++++++++ src/smt/optimization_solver.h | 116 ++++++++++++++++++ test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/theory_int_opt_white.cpp | 126 ++++++++++++++++++++ 5 files changed, 382 insertions(+) create mode 100644 src/smt/optimization_solver.cpp create mode 100644 src/smt/optimization_solver.h create mode 100644 test/unit/theory/theory_int_opt_white.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c438d9a4f..419b6ff75 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -242,6 +242,8 @@ libcvc4_add_sources( smt/model_blocker.h smt/node_command.cpp smt/node_command.h + smt/optimization_solver.cpp + smt/optimization_solver.h smt/options_manager.cpp smt/options_manager.h smt/output_manager.cpp diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp new file mode 100644 index 000000000..609ed9813 --- /dev/null +++ b/src/smt/optimization_solver.cpp @@ -0,0 +1,137 @@ +/********************* */ +/*! \file optimization_solver.cpp + ** \verbatim + ** Top contributors (to current version): + ** Michael Chang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for optimization queries + **/ + +#include "smt/optimization_solver.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/smt_engine_subsolver.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace smt { + +/** + * d_activatedObjective is initialized to a default objective: + * default objective constructed with Null Node and OBJECTIVE_UNDEFINED + * + * d_savedValue is initialized to a default node (Null Node) + */ + +OptimizationSolver::OptimizationSolver(SmtEngine* parent) + : d_parent(parent), + d_activatedObjective(Node(), OBJECTIVE_UNDEFINED), + d_savedValue() +{ +} + +OptimizationSolver::~OptimizationSolver() {} + +OptResult OptimizationSolver::checkOpt() +{ + // Make sure that the objective is not the default one + Assert(d_activatedObjective.getType() != OBJECTIVE_UNDEFINED); + Assert(!d_activatedObjective.getNode().isNull()); + + // the smt engine to which we send intermediate queries + // for the linear search. + std::unique_ptr optChecker; + initializeSubsolver(optChecker); + NodeManager* nm = optChecker->getNodeManager(); + + // we need to be in incremental mode for multiple objectives since we need to + // push pop we need to produce models to inrement on our objective + optChecker->setOption("incremental", "true"); + optChecker->setOption("produce-models", "true"); + + // Move assertions from the parent solver to the subsolver + std::vector p_assertions = d_parent->getExpandedAssertions(); + for (const Node& e : p_assertions) + { + optChecker->assertFormula(e); + } + + // We need to checksat once before the optimization loop so we have a + // baseline value to increment + Result loop_r = optChecker->checkSat(); + + if (loop_r.isUnknown()) + { + return OPT_UNKNOWN; + } + if (!loop_r.isSat()) + { + return OPT_UNSAT; + } + + // Model-value of objective (used in optimization loop) + Node value; + // asserts objective > old_value (used in optimization loop) + Node increment; + + // Workhorse of linear optimization: + // This loop will keep incrmenting the objective until unsat + // When unsat is hit, the optimized value is the model value just before the + // unsat call + while (loop_r.isSat()) + { + // get the model-value of objective in last sat call + value = optChecker->getValue(d_activatedObjective.getNode()); + + // We need to save the value since we need the model value just before the + // unsat call + Assert(!value.isNull()); + d_savedValue = value; + + // increment on the model-value of objective: + // if we're maximizing increment = objective > old_objective value + // if we're minimizing increment = objective < old_objective value + if (d_activatedObjective.getType() == OBJECTIVE_MAXIMIZE) + { + increment = nm->mkNode(kind::GT, d_activatedObjective.getNode(), value); + } + else + { + increment = nm->mkNode(kind::LT, d_activatedObjective.getNode(), value); + } + optChecker->assertFormula(increment); + loop_r = optChecker->checkSat(); + } + + return OPT_OPTIMAL; +} + +void OptimizationSolver::activateObj(const Node& obj, const int& type) +{ + d_activatedObjective = Objective(obj, (ObjectiveType)type); +} + +Node OptimizationSolver::objectiveGetValue() +{ + Assert(!d_savedValue.isNull()); + return d_savedValue; +} + +Objective::Objective(Node obj, ObjectiveType type) : d_type(type), d_node(obj) +{ +} + +ObjectiveType Objective::getType() { return d_type; } + +Node Objective::getNode() { return d_node; } + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h new file mode 100644 index 000000000..c8a024505 --- /dev/null +++ b/src/smt/optimization_solver.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file optimization_solver.h + ** \verbatim + ** Top contributors (to current version): + ** Michael Chang + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The solver for optimization queries + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__OPTIMIZATION_SOLVER_H +#define CVC4__SMT__OPTIMIZATION_SOLVER_H + +#include "expr/node.h" +#include "expr/type_node.h" +#include "smt/assertions.h" +#include "util/result.h" + +namespace CVC4 { +namespace smt { + +/** + * An enum for optimization queries. + * + * Represents whether an objective should be minimized or maximized + */ +enum CVC4_PUBLIC ObjectiveType +{ + OBJECTIVE_MINIMIZE, + OBJECTIVE_MAXIMIZE, + OBJECTIVE_UNDEFINED +}; + +/** + * An enum for optimization queries. + * + * Represents the result of a checkopt query + * (unimplemented) OPT_OPTIMAL: if value was found + */ +enum CVC4_PUBLIC OptResult +{ + // the original set of assertions has result UNKNOWN + OPT_UNKNOWN, + // the original set of assertions has result UNSAT + OPT_UNSAT, + // the optimization loop finished and optimal + OPT_OPTIMAL, + + // The last value is here as a preparation for future work + // in which pproximate optimizations will be supported. + + // if the solver halted early and value is only approximate + OPT_SAT_APPROX +}; + +class Objective +{ + public: + Objective(Node n, ObjectiveType type); + ~Objective(){}; + + /** A getter for d_type **/ + ObjectiveType getType(); + /** A getter for d_node **/ + Node getNode(); + + private: + /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR + * OBJECTIVE_MINIMIZE **/ + ObjectiveType d_type; + /** The node associated to the term that was used to construct the objective. + * **/ + Node d_node; + }; + + /** + * A solver for optimization queries. + * + * This class is responsible for responding to optmization queries. It + * spawns a subsolver SmtEngine that captures the parent assertions and + * implements a linear optimization loop. Supports activateObjective, + * checkOpt, and objectiveGetValue in that order. + */ + class OptimizationSolver + { + public: + /** parent is the smt_solver that the user added their assertions to **/ + OptimizationSolver(SmtEngine* parent); + ~OptimizationSolver(); + + /** Runs the optimization loop for the activated objective **/ + OptResult checkOpt(); + /** Activates an objective: will be optimized for **/ + void activateObj(const Node& obj, const int& type); + /** Gets the value of the optimized objective after checkopt is called **/ + Node objectiveGetValue(); + + private: + /** The parent SMT engine **/ + SmtEngine* d_parent; + /** The objectives to optimize for **/ + Objective d_activatedObjective; + /** A saved value of the objective from the last sat call. **/ + Node d_savedValue; + }; + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__OPTIMIZATION_SOLVER_H */ diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index f3c340a74..9a8bc4dee 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -21,6 +21,7 @@ cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) +cvc4_add_unit_test_white(theory_int_opt_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp new file mode 100644 index 000000000..1e5c2c437 --- /dev/null +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -0,0 +1,126 @@ +#include +#include "smt/optimization_solver.h" +#include "test_smt.h" + +namespace CVC4 { + +using namespace theory; +using namespace smt; + +namespace test { + +class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-assertions", "true"); + d_smtEngine->finishInit(); + + d_optslv.reset(new OptimizationSolver(d_smtEngine.get())); + d_intType.reset(new TypeNode(d_nodeManager->integerType())); + } + + std::unique_ptr d_optslv; + std::unique_ptr d_intType; +}; + +TEST_F(TestTheoryWhiteIntOpt, max) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb); + + /* Result of asserts is: + 0 < max_cost < 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, max_type); + + OptResult r = d_optslv->checkOpt(); + + // We expect max_cost == 99 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(Rational("99"))); + + std::cout << "Result is :" << r << std::endl; + std::cout << "Optimized max value is: " + << d_optslv->objectiveGetValue() << std::endl; +} + +TEST_F(TestTheoryWhiteIntOpt, min) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb); + + /* Result of asserts is: + 0 < max_cost < 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType min_type = OBJECTIVE_MINIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, min_type); + + OptResult r = d_optslv->checkOpt(); + + // We expect max_cost == 99 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(Rational("1"))); + + std::cout << "Result is :" << r << std::endl; + std::cout << "Optimized max value is: " + << d_optslv->objectiveGetValue() << std::endl; +} + +TEST_F(TestTheoryWhiteIntOpt, result) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub); + + /* Result of asserts is: + 0 > max_cost > 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, max_type); + + // This should return OPT_UNSAT since 0 > x > 100 is impossible. + OptResult r = d_optslv->checkOpt(); + + // We expect our check to have returned UNSAT + ASSERT_EQ(r, OPT_UNSAT); + + std::cout << "Result is :" << r << std::endl; +} +} // namespace test +} // namespace CVC4 -- 2.30.2