Expose parameters of EvalMaxSAT in our API

MICS-Lab · Feb 5, 2024 · 3c986c4 · 3c986c4
1 parent 86a38e2
commit 3c986c4
Show file tree

Hide file tree

Showing 13 changed files with 276 additions and 25 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -12,13 +12,14 @@ namespace lincs {
 template<typename MaxSatProblem>
 class MaxSatCoalitionsUcncsLearning {
  public:
-  MaxSatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_) :
+  template<class... U>
+  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>(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
@@ -12,15 +12,16 @@ namespace lincs {
 template<typename MaxSatProblem>
 class MaxSatSeparationUcncsLearning {
  public:
-  MaxSatSeparationUcncsLearning(const Problem& problem, const Alternatives& learning_set_) :
+  template<class... U>
+  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),
     better_alternative_indexes(),
     worse_alternative_indexes(),
     better(),
     separates(),
-    sat()
+    sat(std::forward<U>(u)...)
   {}
 
  public:

diff --git 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<typename SatProblem>
 class SatCoalitionsUcncsLearning {
  public:
-  SatCoalitionsUcncsLearning(const Problem& problem, const Alternatives& learning_set_) :
+  template<class... U>
+  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>(u)...)
   {}
 
   // Not copyable