From 0c239c6a1396715ca734d9e2d50cf507161b4eff Mon Sep 17 00:00:00 2001
From: Adam Szady <7527999+aszady@users.noreply.github.com>
Date: Thu, 22 Jan 2026 01:21:51 +0100
Subject: [PATCH] Simplify SAT equivalence formula
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For each package we had this set of implication over all `provided`:
one `provided` is on ⇒  all `provided` are on as well.

This is effectively the equivalence between all these variables,
and therefore can be represented by `bf.Eq` instead.

Such formulation is easier for the used SAT solver, as example runs show:

before:
//pkg/sat:sat_determinsitic_test                                         PASSED in 20.3s
//pkg/sat:sat_test                                                       PASSED in 118.7s

after:
//pkg/sat:sat_determinsitic_test                                         PASSED in 8.9s
//pkg/sat:sat_test                                                       PASSED in 6.8s

Note that tests under `sat/loader_test.go` guarantee that we're still solving the same problem.

This change focuses on improving the performance.
Follow-up changes are recommended to cleanup the code from these redundant variables.
---
 pkg/sat/loader.go | 19 ++++++-------------
 1 file changed, 6 insertions(+), 13 deletions(-)

diff --git a/pkg/sat/loader.go b/pkg/sat/loader.go
index 7f7e4bd4..431ea734 100644
--- a/pkg/sat/loader.go
+++ b/pkg/sat/loader.go
@@ -164,15 +164,15 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 
 	// Generate imply rules
 	for _, provided := range pkgProvideKeys {
-		// Create imply rules for every package and add them to the formula
-		// one provided dependency implies all dependencies from that package
-		resourceVars := pkgProvides[provided]
-		bfVar := bf.And(toBFVars(resourceVars)...)
 		var ands []bf.Formula
+
+		// Synchronize all the variables for a given package to the same value.
+		resourceVars := pkgProvides[provided]
+		pkgVar := resourceVars[len(resourceVars)-1]
 		for _, res := range resourceVars {
-			ands = append(ands, bf.Implies(bf.Var(res.satVarName), bfVar))
+			ands = append(ands, bf.Eq(bf.Var(pkgVar.satVarName), bf.Var(res.satVarName)))
 		}
-		pkgVar := resourceVars[len(resourceVars)-1]
+
 		ands = append(ands, bf.Implies(bf.Var(pkgVar.satVarName), loader.explodePackageRequires(pkgVar)))
 		if conflicts := loader.explodePackageConflicts(pkgVar); conflicts != nil {
 			ands = append(ands, bf.Implies(bf.Var(pkgVar.satVarName), bf.Not(conflicts)))
@@ -375,13 +375,6 @@ func (loader *Loader) resolveNewest(pkgName string, archOrder []string) (*Var, e
 	return newest, nil
 }
 
-func toBFVars(vars []*Var) (bfvars []bf.Formula) {
-	for _, v := range vars {
-		bfvars = append(bfvars, bf.Var(v.satVarName))
-	}
-	return
-}
-
 func compareRequires(entry api.Entry, provides []*Var) (accepts []*Var, err error) {
 	for _, dep := range provides {
 		entryVer := api.Version{