From 3c986c4c9f56248f770287bc020e1268d53cbb2f Mon Sep 17 00:00:00 2001 From: Vincent Jacques Date: Mon, 5 Feb 2024 16:01:57 +0000 Subject: [PATCH] Expose parameters of EvalMaxSAT in our API --- doc-sources/reference/lincs.rst | 4 +- .../sat-learning/sat-learning.ipynb | 2 +- .../eval-max-sat-parallelization/.gitignore | 3 + .../eval-max-sat-parallelization.ipynb | 78 ++++++++++++++++ integration-tests/help-all/help-all.ipynb | 70 ++++++++++++++ .../virtual-cost/virtual-cost.ipynb | 12 +-- lincs/command_line_interface.py | 93 ++++++++++++++++++- .../ucncs-by-max-sat-by-coalitions.hpp | 5 +- .../ucncs-by-max-sat-by-separation.hpp | 5 +- .../learning/ucncs-by-sat-by-coalitions.hpp | 5 +- .../learning/ucncs-by-sat-by-separation.hpp | 5 +- .../liblincs-module/learning-classes.cpp | 10 +- lincs/liblincs/sat/eval-max-sat.hpp | 9 +- 13 files changed, 276 insertions(+), 25 deletions(-) create mode 100644 integration-tests/eval-max-sat-parallelization/.gitignore create mode 100644 integration-tests/eval-max-sat-parallelization/eval-max-sat-parallelization.ipynb diff --git a/doc-sources/reference/lincs.rst b/doc-sources/reference/lincs.rst index 96299f2d..e17ce245 100644 --- a/doc-sources/reference/lincs.rst +++ b/doc-sources/reference/lincs.rst @@ -662,7 +662,7 @@ @todo(Documentation, v1.1) Add a docstring. - .. method:: __init__(problem: Problem, learning_set: Alternatives) + .. method:: __init__(problem: Problem, learning_set: Alternatives [, nb_minimize_threads: int=0 [, timeout_fast_minimize: int=60 [, coef_minimize_time: int=2]]]) @todo(Documentation, v1.1) Add a docstring. @@ -674,7 +674,7 @@ @todo(Documentation, v1.1) Add a docstring. - .. method:: __init__(problem: Problem, learning_set: Alternatives) + .. method:: __init__(problem: Problem, learning_set: Alternatives [, nb_minimize_threads: int=0 [, timeout_fast_minimize: int=60 [, coef_minimize_time: int=2]]]) @todo(Documentation, v1.1) Add a docstring. diff --git a/doc-sources/user-guide/sat-learning/sat-learning.ipynb b/doc-sources/user-guide/sat-learning/sat-learning.ipynb index 29817ec5..a0879a35 100644 --- a/doc-sources/user-guide/sat-learning/sat-learning.ipynb +++ b/doc-sources/user-guide/sat-learning/sat-learning.ipynb @@ -58,7 +58,7 @@ "name": "stdout", "output_type": "stream", "text": [ - "# Reproduction command (with lincs version 1.1.0a6.dev0): lincs learn classification-model problem.yml learning-set.csv --model-type ucncs --ucncs.strategy max-sat-by-separation\n", + "# Reproduction command (with lincs version 1.1.0a6.dev0): lincs learn classification-model problem.yml learning-set.csv --model-type ucncs --ucncs.strategy max-sat-by-separation --ucncs.max-sat-by-separation.solver eval-max-sat --ucncs.max-sat-by-separation.eval-max-sat.nb-minimize-threads 0 --ucncs.max-sat-by-separation.eval-max-sat.timeout-fast-minimize 60 --ucncs.max-sat-by-separation.eval-max-sat.coef-minimize-time 2\n", "kind: ncs-classification-model\n", "format_version: 1\n", "accepted_values:\n", diff --git a/integration-tests/eval-max-sat-parallelization/.gitignore b/integration-tests/eval-max-sat-parallelization/.gitignore new file mode 100644 index 00000000..ef61e872 --- /dev/null +++ b/integration-tests/eval-max-sat-parallelization/.gitignore @@ -0,0 +1,3 @@ +/problem.yml +/model.yml +/learning-set.csv diff --git a/integration-tests/eval-max-sat-parallelization/eval-max-sat-parallelization.ipynb b/integration-tests/eval-max-sat-parallelization/eval-max-sat-parallelization.ipynb new file mode 100644 index 00000000..39801e88 --- /dev/null +++ b/integration-tests/eval-max-sat-parallelization/eval-max-sat-parallelization.ipynb @@ -0,0 +1,78 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 1, + "id": "6fae8c93-2039-447b-9dcc-fd8f82f22801", + "metadata": {}, + "outputs": [], + "source": [ + "lincs generate classification-problem 4 3 --output-problem problem.yml --random-seed 400\n", + "lincs generate classification-model problem.yml --output-model model.yml --random-seed 410\n", + "lincs generate classified-alternatives problem.yml model.yml 300 --output-alternatives learning-set.csv --random-seed 420 --misclassified-count 30" + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "dd849cc1-a955-420f-b870-09e76dc513bd", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "real\t0m22.556s\n", + "user\t0m22.706s\n", + "sys\t0m2.022s\n" + ] + } + ], + "source": [ + "time lincs learn classification-model problem.yml learning-set.csv \\\n", + " --model-type ucncs --ucncs.strategy max-sat-by-separation \\\n", + " >/dev/null" + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "2e755c41-5f27-42e4-8bfb-172baa3cd216", + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "real\t0m22.462s\n", + "user\t0m58.862s\n", + "sys\t0m2.100s\n" + ] + } + ], + "source": [ + "time lincs learn classification-model problem.yml learning-set.csv \\\n", + " --model-type ucncs --ucncs.strategy max-sat-by-separation \\\n", + " --ucncs.max-sat-by-separation.eval-max-sat.nb-minimize-threads 14 \\\n", + " >/dev/null" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Bash", + "language": "bash", + "name": "bash" + }, + "language_info": { + "codemirror_mode": "shell", + "file_extension": ".sh", + "mimetype": "text/x-sh", + "name": "bash" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} diff --git a/integration-tests/help-all/help-all.ipynb b/integration-tests/help-all/help-all.ipynb index 505fa0a4..438909b8 100644 --- a/integration-tests/help-all/help-all.ipynb +++ b/integration-tests/help-all/help-all.ipynb @@ -304,6 +304,76 @@ " - '--model-type' is 'ucncs'\n", " \n", " [default: sat-by-coalitions]\n", + " --ucncs.max-sat-by-separation.solver [eval-max-sat]\n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-separation'\n", + " \n", + " [default: eval-max-sat]\n", + " --ucncs.max-sat-by-separation.eval-max-sat.nb-minimize-threads INTEGER RANGE\n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-separation'\n", + " - '--ucncs.max-sat-by-separation.solver' is 'eval-max-sat'\n", + " \n", + " [default: 0; x>=0]\n", + " --ucncs.max-sat-by-separation.eval-max-sat.timeout-fast-minimize INTEGER RANGE\n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-separation'\n", + " - '--ucncs.max-sat-by-separation.solver' is 'eval-max-sat'\n", + " \n", + " [default: 60; x>=0]\n", + " --ucncs.max-sat-by-separation.eval-max-sat.coef-minimize-time INTEGER RANGE\n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-separation'\n", + " - '--ucncs.max-sat-by-separation.solver' is 'eval-max-sat'\n", + " \n", + " [default: 2; x>=0]\n", + " --ucncs.max-sat-by-coalitions.solver [eval-max-sat]\n", + " The solver to use to solve the MaxSAT\n", + " problem.\n", + " \n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-coalitions'\n", + " \n", + " [default: eval-max-sat]\n", + " --ucncs.max-sat-by-coalitions.eval-max-sat.nb-minimize-threads INTEGER RANGE\n", + " The number of threads to use to minimize the\n", + " MaxSAT problem. Passed directly to the\n", + " EvalMaxSAT solver.\n", + " \n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-coalitions'\n", + " - '--ucncs.max-sat-by-coalitions.solver' is 'eval-max-sat'\n", + " \n", + " [default: 0; x>=0]\n", + " --ucncs.max-sat-by-coalitions.eval-max-sat.timeout-fast-minimize INTEGER RANGE\n", + " The maximum duration of the \"fast minimize\"\n", + " phase of solving the MaxSAT problem, in\n", + " seconds. Passed directly to the EvalMaxSAT\n", + " solver.\n", + " \n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-coalitions'\n", + " - '--ucncs.max-sat-by-coalitions.solver' is 'eval-max-sat'\n", + " \n", + " [default: 60; x>=0]\n", + " --ucncs.max-sat-by-coalitions.eval-max-sat.coef-minimize-time INTEGER RANGE\n", + " The coefficient to use to multiply the time\n", + " spent minimizing the MaxSAT problem. Passed\n", + " directly to the EvalMaxSAT solver.\n", + " \n", + " Only valid if:\n", + " - '--model-type' is 'ucncs'\n", + " - '--ucncs.strategy' is 'max-sat-by-coalitions'\n", + " - '--ucncs.max-sat-by-coalitions.solver' is 'eval-max-sat'\n", + " \n", + " [default: 2; x>=0]\n", " --mrsort.strategy [weights-profiles-breed]\n", " The top-level strategy to use to learn the\n", " MRSort model. See https://mics-\n", diff --git a/integration-tests/virtual-cost/virtual-cost.ipynb b/integration-tests/virtual-cost/virtual-cost.ipynb index 85515736..7bbf4a5d 100644 --- a/integration-tests/virtual-cost/virtual-cost.ipynb +++ b/integration-tests/virtual-cost/virtual-cost.ipynb @@ -23,9 +23,9 @@ "output_type": "stream", "text": [ "\n", - "real\t0m0.947s\n", - "user\t0m0.947s\n", - "sys\t0m0.001s\n" + "real\t0m1.145s\n", + "user\t0m1.137s\n", + "sys\t0m0.008s\n" ] } ], @@ -44,9 +44,9 @@ "output_type": "stream", "text": [ "\n", - "real\t0m1.174s\n", - "user\t0m1.170s\n", - "sys\t0m0.004s\n" + "real\t0m1.331s\n", + "user\t0m1.330s\n", + "sys\t0m0.000s\n" ] } ], diff --git a/lincs/command_line_interface.py b/lincs/command_line_interface.py index 2bf63f82..87e0b0ce 100644 --- a/lincs/command_line_interface.py +++ b/lincs/command_line_interface.py @@ -530,6 +530,54 @@ def learn(): pass +max_sat_options = [ + ( + "solver", + dict( + help="The solver to use to solve the MaxSAT problem.", + type=click.Choice(["eval-max-sat"]), + default="eval-max-sat", + show_default=True, + ), + { + "eval-max-sat": [ + # These three options correspond to EvalMaxSAT's command-line options here: + # https://github.com/normal-account/EvalMaxSAT2022/blob/main/main.cpp#L43-L50 + ( + "nb-minimize-threads", + dict( + help="The number of threads to use to minimize the MaxSAT problem. Passed directly to the EvalMaxSAT solver.", + type=click.IntRange(min=0), + default=0, + show_default=True, + ), + {}, + ), + ( + "timeout-fast-minimize", + dict( + help="The maximum duration of the \"fast minimize\" phase of solving the MaxSAT problem, in seconds. Passed directly to the EvalMaxSAT solver.", + type=click.IntRange(min=0), + default=60, + show_default=True, + ), + {}, + ), + ( + "coef-minimize-time", + dict( + help="The coefficient to use to multiply the time spent minimizing the MaxSAT problem. Passed directly to the EvalMaxSAT solver.", + type=click.IntRange(min=0), + default=2, + show_default=True, + ), + {}, + ), + ], + }, + ), +] + @learn.command( help=""" Learn a classification model. @@ -754,7 +802,10 @@ def learn(): default="sat-by-coalitions", show_default=True, ), - {}, + { + "max-sat-by-coalitions": max_sat_options, + "max-sat-by-separation": max_sat_options, + }, ), ], }, @@ -782,6 +833,14 @@ def classification_model( mrsort__weights_profiles_breed__verbose, mrsort__weights_profiles_breed__output_metadata, ucncs__strategy, + ucncs__max_sat_by_coalitions__solver, + ucncs__max_sat_by_coalitions__eval_max_sat__nb_minimize_threads, + ucncs__max_sat_by_coalitions__eval_max_sat__timeout_fast_minimize, + ucncs__max_sat_by_coalitions__eval_max_sat__coef_minimize_time, + ucncs__max_sat_by_separation__solver, + ucncs__max_sat_by_separation__eval_max_sat__nb_minimize_threads, + ucncs__max_sat_by_separation__eval_max_sat__timeout_fast_minimize, + ucncs__max_sat_by_separation__eval_max_sat__coef_minimize_time, ): command_line = ["lincs", "learn", "classification-model", get_input_file_name(problem), get_input_file_name(learning_set), "--model-type", model_type] @@ -890,13 +949,37 @@ def before_return(self): if ucncs__strategy == "sat-by-coalitions": learning = lincs.classification.LearnUcncsBySatByCoalitionsUsingMinisat(problem, learning_set) elif ucncs__strategy == "sat-by-separation": - # @todo(Feature, later) Consider adding parameters to EvalMaxSAT corresponding to the three command-line options here: - # https://github.com/normal-account/EvalMaxSAT2022/blob/main/main.cpp#L43-L50 learning = lincs.classification.LearnUcncsBySatBySeparationUsingMinisat(problem, learning_set) elif ucncs__strategy == "max-sat-by-coalitions": - learning = lincs.classification.LearnUcncsByMaxSatByCoalitionsUsingEvalmaxsat(problem, learning_set) + command_line += ["--ucncs.max-sat-by-coalitions.solver", ucncs__max_sat_by_coalitions__solver] + if ucncs__max_sat_by_coalitions__solver == "eval-max-sat": + command_line += [ + "--ucncs.max-sat-by-coalitions.eval-max-sat.nb-minimize-threads", ucncs__max_sat_by_coalitions__eval_max_sat__nb_minimize_threads, + "--ucncs.max-sat-by-coalitions.eval-max-sat.timeout-fast-minimize", ucncs__max_sat_by_coalitions__eval_max_sat__timeout_fast_minimize, + "--ucncs.max-sat-by-coalitions.eval-max-sat.coef-minimize-time", ucncs__max_sat_by_coalitions__eval_max_sat__coef_minimize_time, + ] + learning = lincs.classification.LearnUcncsByMaxSatByCoalitionsUsingEvalmaxsat( + problem, + learning_set, + ucncs__max_sat_by_coalitions__eval_max_sat__nb_minimize_threads, + ucncs__max_sat_by_coalitions__eval_max_sat__timeout_fast_minimize, + ucncs__max_sat_by_coalitions__eval_max_sat__coef_minimize_time, + ) elif ucncs__strategy == "max-sat-by-separation": - learning = lincs.classification.LearnUcncsByMaxSatBySeparationUsingEvalmaxsat(problem, learning_set) + command_line += ["--ucncs.max-sat-by-separation.solver", ucncs__max_sat_by_separation__solver] + if ucncs__max_sat_by_separation__solver == "eval-max-sat": + command_line += [ + "--ucncs.max-sat-by-separation.eval-max-sat.nb-minimize-threads", ucncs__max_sat_by_separation__eval_max_sat__nb_minimize_threads, + "--ucncs.max-sat-by-separation.eval-max-sat.timeout-fast-minimize", ucncs__max_sat_by_separation__eval_max_sat__timeout_fast_minimize, + "--ucncs.max-sat-by-separation.eval-max-sat.coef-minimize-time", ucncs__max_sat_by_separation__eval_max_sat__coef_minimize_time, + ] + learning = lincs.classification.LearnUcncsByMaxSatBySeparationUsingEvalmaxsat( + problem, + learning_set, + ucncs__max_sat_by_separation__eval_max_sat__nb_minimize_threads, + ucncs__max_sat_by_separation__eval_max_sat__timeout_fast_minimize, + ucncs__max_sat_by_separation__eval_max_sat__coef_minimize_time, + ) try: model = learning.perform() diff --git a/lincs/liblincs/learning/ucncs-by-max-sat-by-coalitions.hpp b/lincs/liblincs/learning/ucncs-by-max-sat-by-coalitions.hpp index 7c0fafeb..1e36c352 100644 --- a/lincs/liblincs/learning/ucncs-by-max-sat-by-coalitions.hpp +++ b/lincs/liblincs/learning/ucncs-by-max-sat-by-coalitions.hpp @@ -12,13 +12,14 @@ namespace lincs { template class MaxSatCoalitionsUcncsLearning { public: - MaxSatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_) : + template + MaxSatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_, U&&... u) : learning_set(problem, learning_set_), coalitions_count(1 << learning_set.criteria_count), goal_weight(1), better(), sufficient(), - sat() + sat(std::forward(u)...) {} // Not copyable diff --git a/lincs/liblincs/learning/ucncs-by-max-sat-by-separation.hpp b/lincs/liblincs/learning/ucncs-by-max-sat-by-separation.hpp index 971c1bfc..487835a1 100644 --- a/lincs/liblincs/learning/ucncs-by-max-sat-by-separation.hpp +++ b/lincs/liblincs/learning/ucncs-by-max-sat-by-separation.hpp @@ -12,7 +12,8 @@ namespace lincs { template class MaxSatSeparationUcncsLearning { public: - MaxSatSeparationUcncsLearning(const Problem& problem, const Alternatives& learning_set_) : + template + MaxSatSeparationUcncsLearning(const Problem& problem, const Alternatives& learning_set_, U&&... u) : learning_set(problem, learning_set_), subgoal_weight(1), goal_weight(learning_set.boundaries_count * learning_set.alternatives_count), @@ -20,7 +21,7 @@ class MaxSatSeparationUcncsLearning { worse_alternative_indexes(), better(), separates(), - sat() + sat(std::forward(u)...) {} public: diff --git a/lincs/liblincs/learning/ucncs-by-sat-by-coalitions.hpp b/lincs/liblincs/learning/ucncs-by-sat-by-coalitions.hpp index 076be3ec..11eeecb1 100644 --- a/lincs/liblincs/learning/ucncs-by-sat-by-coalitions.hpp +++ b/lincs/liblincs/learning/ucncs-by-sat-by-coalitions.hpp @@ -12,12 +12,13 @@ namespace lincs { template class SatCoalitionsUcncsLearning { public: - SatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_) : + template + SatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_, U&&... u) : learning_set(problem, learning_set_), coalitions_count(1 << learning_set.criteria_count), better(), sufficient(), - sat() + sat(std::forward(u)...) {} // Not copyable diff --git a/lincs/liblincs/learning/ucncs-by-sat-by-separation.hpp b/lincs/liblincs/learning/ucncs-by-sat-by-separation.hpp index 6e0f3e66..d6fd7323 100644 --- a/lincs/liblincs/learning/ucncs-by-sat-by-separation.hpp +++ b/lincs/liblincs/learning/ucncs-by-sat-by-separation.hpp @@ -12,13 +12,14 @@ namespace lincs { template class SatSeparationUcncsLearning { public: - SatSeparationUcncsLearning(const Problem& problem, const Alternatives& learning_set_) : + template + SatSeparationUcncsLearning(const Problem& problem, const Alternatives& learning_set_, U&&... u) : learning_set(problem, learning_set_), better_alternative_indexes(), worse_alternative_indexes(), better(), separates(), - sat() + sat(std::forward(u)...) {} public: diff --git a/lincs/liblincs/liblincs-module/learning-classes.cpp b/lincs/liblincs/liblincs-module/learning-classes.cpp index 09b20ac1..5c0629b8 100644 --- a/lincs/liblincs/liblincs-module/learning-classes.cpp +++ b/lincs/liblincs/liblincs-module/learning-classes.cpp @@ -397,7 +397,10 @@ void define_learning_classes() { "@todo(Documentation, v1.1) Add a docstring.", bp::no_init ) - .def(bp::init((bp::arg("self"), "problem", "learning_set"), "@todo(Documentation, v1.1) Add a docstring.")[bp::with_custodian_and_ward<1, 2 /* No reference kept on 'learning_set' => no custodian_and_ward */>()]) + .def(bp::init( + (bp::arg("self"), "problem", "learning_set", bp::arg("nb_minimize_threads") = 0, bp::arg("timeout_fast_minimize") = 60, bp::arg("coef_minimize_time") = 2), + "@todo(Documentation, v1.1) Add a docstring." + )[bp::with_custodian_and_ward<1, 2 /* No reference kept on 'learning_set' => no custodian_and_ward */>()]) .def("perform", &lincs::LearnUcncsByMaxSatByCoalitionsUsingEvalmaxsat::perform, (bp::arg("self")), "@todo(Documentation, v1.1) Add a docstring.") ; @@ -406,7 +409,10 @@ void define_learning_classes() { "@todo(Documentation, v1.1) Add a docstring.", bp::no_init ) - .def(bp::init((bp::arg("self"), "problem", "learning_set"), "@todo(Documentation, v1.1) Add a docstring.")[bp::with_custodian_and_ward<1, 2 /* No reference kept on 'learning_set' => no custodian_and_ward */>()]) + .def(bp::init( + (bp::arg("self"), "problem", "learning_set", bp::arg("nb_minimize_threads") = 0, bp::arg("timeout_fast_minimize") = 60, bp::arg("coef_minimize_time") = 2), + "@todo(Documentation, v1.1) Add a docstring." + )[bp::with_custodian_and_ward<1, 2 /* No reference kept on 'learning_set' => no custodian_and_ward */>()]) .def("perform", &lincs::LearnUcncsByMaxSatBySeparationUsingEvalmaxsat::perform, (bp::arg("self")), "@todo(Documentation, v1.1) Add a docstring.") ; } diff --git a/lincs/liblincs/sat/eval-max-sat.hpp b/lincs/liblincs/sat/eval-max-sat.hpp index f4061417..6ec06719 100644 --- a/lincs/liblincs/sat/eval-max-sat.hpp +++ b/lincs/liblincs/sat/eval-max-sat.hpp @@ -24,7 +24,14 @@ namespace lincs { class EvalmaxsatMaxSatProblem { public: - EvalmaxsatMaxSatProblem() : solver(0) {} + EvalmaxsatMaxSatProblem( + unsigned nb_minimize_threads = 0, + unsigned timeout_fast_minimize = 60, // Seconds. Documented as "Magic number" in EvalMaxSAT source code. + unsigned coef_minimize_time = 2 // Documented as "Magic number" in EvalMaxSAT source code. + ) : solver(nb_minimize_threads) { + solver.setTimeOutFast(timeout_fast_minimize); + solver.setCoefMinimize(coef_minimize_time); + } public: typedef int variable_type;