summaryrefslogtreecommitdiff
path: root/apt-pkg
diff options
context:
space:
mode:
authorJulian Andres Klode <julian.klode@canonical.com>2025-01-30 15:34:51 +0100
committerJulian Andres Klode <julian.klode@canonical.com>2025-01-30 15:36:10 +0100
commit945ead2ab03b7c83b3fbaecf3e1e543525e476f0 (patch)
tree3e5befe56363c6253264e2513902d82536621cdb /apt-pkg
parent6425f211c0c85863232afb2d8e7eff95d150bddd (diff)
solver3: Credit MiniSAT
Gbp-Dch: ignore
Diffstat (limited to 'apt-pkg')
-rw-r--r--apt-pkg/solver3.cc11
1 files changed, 11 insertions, 0 deletions
diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index 6f445328c..73f7fd0c4 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -5,6 +5,17 @@
* Copyright (c) 2023 Canonical Ltd
*
* SPDX-License-Identifier: GPL-2.0+
+ *
+ * This solver started from scratch but turns slowly into a variant of
+ * MiniSat as documented in the paper
+ * "An extensible SAT-solver [extended version 1.2]."
+ * by Niklas Eén, and Niklas Sörensson.
+ *
+ * It extends MiniSAT with support for optional clauses, and differs
+ * in that it removes non-deterministic aspects like the activity based
+ * ordering. Instead it uses a more nuanced static ordering that, to
+ * some extend, preserves some greediness and sub-optimality of the
+ * classic APT solver.
*/
#define APT_COMPILING_APT