From 91cfd903b3eb34a62303cb6501e5f682c4815ef9 Mon Sep 17 00:00:00 2001
From: Adam Szady <7527999+aszady@users.noreply.github.com>
Date: Fri, 23 Jan 2026 11:38:14 +0100
Subject: [PATCH 1/4] Add `Resource` abstraction to the SAT loader
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Variable generation is separated into two parts:
- extracting `Resource`s provided by the package – data most useful for the `Loader`;
- creating SAT variable related to that resource – data most useful for the `Resolve` (`Model`).

This modularization of code should facilitates future code changes.

The `VarTypeResource` vs. `VarTypeFile` distinction was not used,
therefore these were merged for further simplification.
---
 pkg/sat/loader.go | 75 ++++++++++++++++++++++++-----------------------
 pkg/sat/sat.go    |  3 +-
 2 files changed, 40 insertions(+), 38 deletions(-)

diff --git a/pkg/sat/loader.go b/pkg/sat/loader.go
index f670ee16..5d799966 100644
--- a/pkg/sat/loader.go
+++ b/pkg/sat/loader.go
@@ -56,6 +56,14 @@ func NewLoader() *Loader {
 	}
 }
 
+// Resource is a convenience abstraction over
+// `api.Entry` and `api.ProvidedFile`
+// that captures only the necessary information we need
+type Resource struct {
+	Name    string      // capability name, or file name
+	Version api.Version // empty for files
+}
+
 // Load takes a list of all involved packages to install, a list of regular
 // expressions which denote packages which should be taken into account for
 // solving the problem, but they should then be ignored together with their
@@ -139,7 +147,8 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 
 	// Generate variables
 	for _, pkg := range packages {
-		pkgVar, resourceVars := loader.explodePackageToVars(pkg)
+		providedResources := loader.explodeProvidedResources(pkg)
+		pkgVar, resourceVars := loader.explodePackageToVars(pkg, providedResources)
 		loader.m.packages[pkg.Name] = append(loader.m.packages[pkg.Name], pkgVar)
 		pkgProvides = append(pkgProvides, resourceVars)
 		for _, v := range resourceVars {
@@ -184,52 +193,46 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 	return loader.constructRequirements(matched, archOrder)
 }
 
-func (loader *Loader) explodePackageToVars(pkg *api.Package) (pkgVar *Var, resourceVars []*Var) {
+// explodeProvidedResources collects all resources a `pkg` can provide (package, capabilities, files)
+// and returns them in unified form of Resource.
+func (loader *Loader) explodeProvidedResources(pkg *api.Package) (provided []*Resource) {
+
 	for _, p := range pkg.Format.Provides.Entries {
-		if p.Name == pkg.Name {
-			pkgVar = &Var{
-				satVarName: loader.ticket(),
-				varType:    VarTypePackage,
-				Context: VarContext{
-					PackageKey: pkg.Key(),
-					Provides:   pkg.Name,
-				},
-				Package:         pkg,
-				ResourceVersion: &pkg.Version,
-			}
-			resourceVars = append(resourceVars, pkgVar)
-		} else {
-			resVar := &Var{
-				satVarName: loader.ticket(),
-				varType:    VarTypeResource,
-				Context: VarContext{
-					PackageKey: pkg.Key(),
-					Provides:   p.Name,
-				},
-				ResourceVersion: &api.Version{
-					Rel:   p.Rel,
-					Ver:   p.Ver,
-					Epoch: p.Epoch,
-				},
-				Package: pkg,
-			}
-			resourceVars = append(resourceVars, resVar)
-		}
+		provided = append(provided, &Resource{
+			Name:    p.Name,
+			Version: api.Version{p.Text, p.Epoch, p.Ver, p.Rel},
+		})
 	}
 
 	for _, f := range pkg.Format.Files {
-		resVar := &Var{
+		provided = append(provided, &Resource{
+			Name: f.Text,
+		})
+	}
+
+	return
+}
+
+func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resource) (pkgVar *Var, resourceVars []*Var) {
+	for _, res := range resources {
+		newVar := &Var{
 			satVarName: loader.ticket(),
-			varType:    VarTypeFile,
+			varType:    VarTypeResource,
 			Context: VarContext{
 				PackageKey: pkg.Key(),
-				Provides:   f.Text,
+				Provides:   res.Name,
 			},
+			ResourceVersion: &res.Version,
 			Package:         pkg,
-			ResourceVersion: &api.Version{},
 		}
-		resourceVars = append(resourceVars, resVar)
+
+		if res.Name == pkg.Name {
+			newVar.varType = VarTypePackage
+			pkgVar = newVar
+		}
+		resourceVars = append(resourceVars, newVar)
 	}
+
 	return pkgVar, resourceVars
 }
 
diff --git a/pkg/sat/sat.go b/pkg/sat/sat.go
index 6ca5ced6..4643d2a9 100644
--- a/pkg/sat/sat.go
+++ b/pkg/sat/sat.go
@@ -18,8 +18,7 @@ type VarType string
 
 const (
 	VarTypePackage  = "Package"
-	VarTypeResource = "Resource"
-	VarTypeFile     = "File"
+	VarTypeResource = "Resource" // includes files
 )
 
 // VarContext contains all information to create a unique identifyable hash key which can be traced back to a package

From 3990d92e5fd2f73d2e3ffc55f1e6c174f7c0d008 Mon Sep 17 00:00:00 2001
From: Adam Szady <7527999+aszady@users.noreply.github.com>
Date: Fri, 23 Jan 2026 11:58:03 +0100
Subject: [PATCH 2/4] Wrap Var into ResourceVar

---
 pkg/sat/loader.go | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/pkg/sat/loader.go b/pkg/sat/loader.go
index 5d799966..4ed84e5b 100644
--- a/pkg/sat/loader.go
+++ b/pkg/sat/loader.go
@@ -64,6 +64,12 @@ type Resource struct {
 	Version api.Version // empty for files
 }
 
+// ResourceVar encapsulates a Resource for which we created a Var in our model.
+type ResourceVar struct {
+	Var      *Var
+	Resource Resource
+}
+
 // Load takes a list of all involved packages to install, a list of regular
 // expressions which denote packages which should be taken into account for
 // solving the problem, but they should then be ignored together with their
@@ -143,7 +149,7 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 		}
 	}
 
-	pkgProvides := [][]*Var{}
+	pkgProvides := [][]*ResourceVar{}
 
 	// Generate variables
 	for _, pkg := range packages {
@@ -152,8 +158,8 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 		loader.m.packages[pkg.Name] = append(loader.m.packages[pkg.Name], pkgVar)
 		pkgProvides = append(pkgProvides, resourceVars)
 		for _, v := range resourceVars {
-			loader.provides[v.Context.Provides] = append(loader.provides[v.Context.Provides], v)
-			loader.m.vars[v.satVarName] = v
+			loader.provides[v.Resource.Name] = append(loader.provides[v.Resource.Name], v.Var)
+			loader.m.vars[v.Var.satVarName] = v.Var
 		}
 	}
 
@@ -173,9 +179,9 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 		var ands []bf.Formula
 
 		// Synchronize all the variables for a given package to the same value.
-		pkgVar := resourceVars[len(resourceVars)-1]
+		pkgVar := resourceVars[len(resourceVars)-1].Var
 		for _, res := range resourceVars {
-			ands = append(ands, bf.Eq(bf.Var(pkgVar.satVarName), bf.Var(res.satVarName)))
+			ands = append(ands, bf.Eq(bf.Var(pkgVar.satVarName), bf.Var(res.Var.satVarName)))
 		}
 
 		ands = append(ands, bf.Implies(bf.Var(pkgVar.satVarName), loader.explodePackageRequires(pkgVar)))
@@ -213,7 +219,7 @@ func (loader *Loader) explodeProvidedResources(pkg *api.Package) (provided []*Re
 	return
 }
 
-func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resource) (pkgVar *Var, resourceVars []*Var) {
+func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resource) (pkgVar *Var, resourceVars []*ResourceVar) {
 	for _, res := range resources {
 		newVar := &Var{
 			satVarName: loader.ticket(),
@@ -230,7 +236,7 @@ func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resour
 			newVar.varType = VarTypePackage
 			pkgVar = newVar
 		}
-		resourceVars = append(resourceVars, newVar)
+		resourceVars = append(resourceVars, &ResourceVar{Var: newVar, Resource: *res})
 	}
 
 	return pkgVar, resourceVars

From 3f468a3b5e9c37d8eaf77f6fb76f43628c54459b Mon Sep 17 00:00:00 2001
From: Adam Szady <7527999+aszady@users.noreply.github.com>
Date: Fri, 23 Jan 2026 12:23:25 +0100
Subject: [PATCH 3/4] Remove fields from Var

---
 pkg/sat/loader.go      | 25 ++++++++-----------
 pkg/sat/loader_test.go | 54 +++++++++++++++++++++---------------------
 pkg/sat/sat.go         | 12 ++++------
 3 files changed, 42 insertions(+), 49 deletions(-)

diff --git a/pkg/sat/loader.go b/pkg/sat/loader.go
index 4ed84e5b..e0cae872 100644
--- a/pkg/sat/loader.go
+++ b/pkg/sat/loader.go
@@ -19,7 +19,7 @@ import (
 
 type Loader struct {
 	m         *Model
-	provides  map[string][]*Var
+	provides  map[string][]*ResourceVar
 	varsCount int
 }
 
@@ -51,7 +51,7 @@ func NewLoader() *Loader {
 			bestPackages:                map[BestKey]*api.Package{},
 			forceIgnoreWithDependencies: map[api.PackageKey]*api.Package{},
 		},
-		provides:  map[string][]*Var{},
+		provides:  map[string][]*ResourceVar{},
 		varsCount: 0,
 	}
 }
@@ -158,7 +158,7 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 		loader.m.packages[pkg.Name] = append(loader.m.packages[pkg.Name], pkgVar)
 		pkgProvides = append(pkgProvides, resourceVars)
 		for _, v := range resourceVars {
-			loader.provides[v.Resource.Name] = append(loader.provides[v.Resource.Name], v.Var)
+			loader.provides[v.Resource.Name] = append(loader.provides[v.Resource.Name], v)
 			loader.m.vars[v.Var.satVarName] = v.Var
 		}
 	}
@@ -224,12 +224,7 @@ func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resour
 		newVar := &Var{
 			satVarName: loader.ticket(),
 			varType:    VarTypeResource,
-			Context: VarContext{
-				PackageKey: pkg.Key(),
-				Provides:   res.Name,
-			},
-			ResourceVersion: &res.Version,
-			Package:         pkg,
+			Package:    pkg,
 		}
 
 		if res.Name == pkg.Name {
@@ -362,14 +357,14 @@ func (loader *Loader) resolveNewest(pkgName string, archOrder []string) (*Var, e
 	}
 	newest := pkgs[0]
 	for _, p := range pkgs {
-		if rpm.ComparePackage(p.Package, newest.Package, archOrder) > 0 {
+		if rpm.ComparePackage(p.Var.Package, newest.Var.Package, archOrder) > 0 {
 			newest = p
 		}
 	}
-	return newest, nil
+	return newest.Var, nil
 }
 
-func compareRequires(entry api.Entry, provides []*Var) (accepts []*Var, err error) {
+func compareRequires(entry api.Entry, provides []*ResourceVar) (accepts []*Var, err error) {
 	for _, dep := range provides {
 		entryVer := api.Version{
 			Text:  entry.Text,
@@ -379,7 +374,7 @@ func compareRequires(entry api.Entry, provides []*Var) (accepts []*Var, err erro
 		}
 
 		// Requirement "EQ 2.14" matches 2.14-5.fc33
-		depVer := *dep.ResourceVersion
+		depVer := dep.Resource.Version
 		if entryVer.Rel == "" {
 			depVer.Rel = ""
 		}
@@ -417,13 +412,13 @@ func compareRequires(entry api.Entry, provides []*Var) (accepts []*Var, err erro
 					works = true
 				}
 			case "":
-				return provides, nil
+				works = true
 			default:
 				return nil, fmt.Errorf("can't interprate flags value %s", entry.Flags)
 			}
 		}
 		if works {
-			accepts = append(accepts, dep)
+			accepts = append(accepts, dep.Var)
 		}
 	}
 	return accepts, nil
diff --git a/pkg/sat/loader_test.go b/pkg/sat/loader_test.go
index b560a58f..21cf8074 100644
--- a/pkg/sat/loader_test.go
+++ b/pkg/sat/loader_test.go
@@ -190,7 +190,7 @@ func TestLoader_Load(t *testing.T) {
 			expectedPackages(g, model, map[string][]string{
 				"A": []string{"0:1.0-1"},
 			})
-			expectedVars(g, model, "A-0:1.0-1(A)")
+			expectedVars(g, model, "A-0:1.0-1")
 			expectedBest(g, model, map[string]string{"A": "0:1.0-1"})
 			expectedIgnores(g, model)
 			expectedAnds(g, model,
@@ -206,7 +206,7 @@ func TestLoader_Load(t *testing.T) {
 			expectedPackages(g, model, map[string][]string{
 				"A": []string{"0:2.0-1"},
 			})
-			expectedVars(g, model, "A-0:2.0-1(A)")
+			expectedVars(g, model, "A-0:2.0-1")
 			expectedBest(g, model, map[string]string{"A": "0:2.0-1"})
 			expectedIgnores(g, model)
 			expectedAnds(g, model,
@@ -222,7 +222,7 @@ func TestLoader_Load(t *testing.T) {
 			expectedPackages(g, model, map[string][]string{
 				"A": []string{"0:1.0-1", "0:2.0-1"},
 			})
-			expectedVars(g, model, "A-0:1.0-1(A)", "A-0:2.0-1(A)")
+			expectedVars(g, model, "A-0:1.0-1", "A-0:2.0-1")
 			expectedBest(g, model, map[string]string{"A": "0:2.0-1"})
 			expectedIgnores(g, model)
 			expectedAnds(g, model,
@@ -245,9 +245,9 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				m,
-				"pkg-a-0:1.0(pkg-a)",
-				"pkg-b-0:1.0(pkg-b)",
-				"pkg-c-0:1.0(pkg-c)",
+				"pkg-a-0:1.0",
+				"pkg-b-0:1.0",
+				"pkg-c-0:1.0",
 			)
 			expectedBest(g, m, map[string]string{
 				"pkg-a": "0:1.0",
@@ -346,9 +346,9 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"app-0:1.0(app)",               // x1
-				"toolkit-0:2.0(toolkit)",       // x2
-				"toolkit-0:2.0(/usr/bin/tool)", // x3
+				"app-0:1.0",     // x1
+				"toolkit-0:2.0", // x2 (toolkit)
+				"toolkit-0:2.0", // x3 (/usr/bin/tool)
 			)
 			expectedBest(g, model, map[string]string{
 				"app":     "0:1.0",
@@ -377,11 +377,11 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"apache-0:2.4(apache)",
-				"apache-0:2.4(webserver)",
-				"app-0:1.0(app)",
-				"nginx-0:1.2(nginx)",
-				"nginx-0:1.2(webserver)",
+				"apache-0:2.4", // (apache)
+				"apache-0:2.4", // (webserver)
+				"app-0:1.0",
+				"nginx-0:1.2", // (nginx)
+				"nginx-0:1.2", // (webserver)
 			)
 			expectedBest(g, model, map[string]string{
 				"app":    "0:1.0",
@@ -409,7 +409,7 @@ func TestLoader_Load(t *testing.T) {
 				"B": []string{"0:1.0"},
 				"C": []string{"0:1.0"},
 			})
-			expectedVars(g, model, "A-0:1.0(A)", "B-0:1.0(B)", "C-0:1.0(C)")
+			expectedVars(g, model, "A-0:1.0", "B-0:1.0", "C-0:1.0")
 			expectedBest(g, model, map[string]string{
 				"A": "0:1.0",
 				"B": "0:1.0",
@@ -433,8 +433,8 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"platform-python-0:3.6(platform-python)",
-				"platform-python-0:3.6(/usr/libexec/platform-python)",
+				"platform-python-0:3.6",
+				"platform-python-0:3.6",
 			)
 			expectedBest(
 				g,
@@ -461,7 +461,7 @@ func TestLoader_Load(t *testing.T) {
 			expectedPackages(g, model, map[string][]string{
 				"A": []string{"5:1.0-2"},
 			})
-			expectedVars(g, model, "A-5:1.0-2(A)")
+			expectedVars(g, model, "A-5:1.0-2")
 			expectedBest(g, model, map[string]string{"A": "5:1.0-2"})
 			expectedAnds(g, model,
 				bf.True, // Nothing to install
@@ -483,12 +483,12 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"gcc-0:11.0(gcc)",     // x1
-				"gcc-0:11.0(gcc)",     // x2
-				"gcc11-0:11.0(gcc11)", // x3
-				"gcc11-0:11.0(gcc)",   // x4
-				"gcc11-0:11.0(gcc11)", // x5
-				"pkgX-0:1.0(pkgX)",    // x6
+				"gcc-0:11.0",   // x1 (gcc)
+				"gcc-0:11.0",   // x2 (gcc)
+				"gcc11-0:11.0", // x3 (gcc11)
+				"gcc11-0:11.0", // x4 (gcc)
+				"gcc11-0:11.0", // x5 (gcc11)
+				"pkgX-0:1.0",   // x6
 			)
 			expectedBest(g, model, map[string]string{
 				"gcc":   "0:11.0",
@@ -511,7 +511,7 @@ func TestLoader_Load(t *testing.T) {
 			pkgA := newPackage("A", "1.0", nil, nil, []string{"A"}, nil)
 			model, _ := doLoad([]*api.Package{pkgA}, nil, nil, nil, false)
 
-			expectedVars(g, model, "A-0:1.0(A)")
+			expectedVars(g, model, "A-0:1.0")
 			expectedAnds(g, model,
 				bf.True, // Nothing to install
 			)
@@ -526,7 +526,7 @@ func TestLoader_Load(t *testing.T) {
 			expectedPackages(g, model, map[string][]string{
 				"A": []string{"0:1.0-1"},
 			})
-			expectedVars(g, model, "A-0:1.0-1(A)")
+			expectedVars(g, model, "A-0:1.0-1")
 			expectedAnds(g, model,
 				bf.Not(x1), // Can't install package `A` (missing dependency `B`).
 			)
@@ -582,7 +582,7 @@ func TestLoader_Load(t *testing.T) {
 				expectedPackages(g, model, map[string][]string{
 					"X": []string{selectedVersion},
 				})
-				expectedVars(g, model, "X-"+selectedVersion+"(X)")
+				expectedVars(g, model, "X-"+selectedVersion)
 				expectedBest(g, model, map[string]string{
 					"X": selectedVersion,
 				})
diff --git a/pkg/sat/sat.go b/pkg/sat/sat.go
index 4643d2a9..73185d5f 100644
--- a/pkg/sat/sat.go
+++ b/pkg/sat/sat.go
@@ -29,15 +29,13 @@ type VarContext struct {
 }
 
 type Var struct {
-	satVarName      string
-	varType         VarType
-	Context         VarContext
-	Package         *api.Package
-	ResourceVersion *api.Version
+	satVarName string
+	varType    VarType
+	Package    *api.Package
 }
 
 func (v Var) String() string {
-	return fmt.Sprintf("%s(%s)", v.Package.String(), v.Context.Provides)
+	return v.Package.String()
 }
 
 type Model struct {
@@ -109,7 +107,7 @@ func Resolve(model *Model) (install []*api.Package, excluded []*api.Package, for
 					satVar := match[2]
 					vars.satToPkg[satVar] = pkgVar
 					vars.pkgToSat[pkgVar] = satVar
-					if _, err := fmt.Fprintf(pwMaxSatWriter, "c %s -> %s\n", model.Var(pkgVar).Package.String(), model.Var(pkgVar).Context.Provides); err != nil {
+					if _, err := fmt.Fprintf(pwMaxSatWriter, "c %s\n", model.Var(pkgVar).Package.String()); err != nil {
 						pwMaxSatErrChan <- err
 						return
 					}

From 288e949b14e24011fb3d7711244af96da1a62942 Mon Sep 17 00:00:00 2001
From: Adam Szady <7527999+aszady@users.noreply.github.com>
Date: Fri, 26 Sep 2025 21:33:25 +0200
Subject: [PATCH 4/4] Merge SAT vars for each package
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

SAT construction used an implication that one provided dependency implies all dependencies from that package.
That's effectively an equivalence relation between all these variables and thus can be merged into one.

This reduces generated SAT size a bit.

//pkg/sat:sat_determinsitic_test runs ~3× faster;
//pkg/sat:sat_test runs ~30× faster.
---
 pkg/sat/loader.go      | 55 +++++++++---------------------------------
 pkg/sat/loader_test.go | 40 ++++++++++--------------------
 pkg/sat/sat.go         | 26 ++++++--------------
 3 files changed, 32 insertions(+), 89 deletions(-)

diff --git a/pkg/sat/loader.go b/pkg/sat/loader.go
index e0cae872..a0f4b2a6 100644
--- a/pkg/sat/loader.go
+++ b/pkg/sat/loader.go
@@ -4,7 +4,6 @@ import (
 	"cmp"
 	"fmt"
 	"regexp"
-	"sort"
 	"strconv"
 	"strings"
 
@@ -149,41 +148,29 @@ func (loader *Loader) Load(packages []*api.Package, matched, ignoreRegex, allowR
 		}
 	}
 
-	pkgProvides := [][]*ResourceVar{}
+	pkgVars := []*Var{}
 
 	// Generate variables
 	for _, pkg := range packages {
-		providedResources := loader.explodeProvidedResources(pkg)
-		pkgVar, resourceVars := loader.explodePackageToVars(pkg, providedResources)
+		// Single variable for SAT formula (whether to pick that package or not):
+		pkgVar := &Var{satVarName: loader.ticket(), Package: pkg}
 		loader.m.packages[pkg.Name] = append(loader.m.packages[pkg.Name], pkgVar)
-		pkgProvides = append(pkgProvides, resourceVars)
-		for _, v := range resourceVars {
-			loader.provides[v.Resource.Name] = append(loader.provides[v.Resource.Name], v)
-			loader.m.vars[v.Var.satVarName] = v.Var
-		}
-	}
+		loader.m.vars[pkgVar.satVarName] = pkgVar
+		pkgVars = append(pkgVars, pkgVar)
 
-	packagesKeys := maps.Keys(loader.m.packages)
-	slices.Sort(packagesKeys)
-
-	for _, x := range packagesKeys {
-		sort.SliceStable(loader.m.packages[x], func(i, j int) bool {
-			return rpm.ComparePackage(loader.m.packages[x][i].Package, loader.m.packages[x][j].Package, archOrder) < 0
-		})
+		// Links between packages (individual resources), only for the loader:
+		for _, resource := range loader.explodeProvidedResources(pkgVar.Package) {
+			prVar := &ResourceVar{Var: pkgVar, Resource: *resource}
+			loader.provides[resource.Name] = append(loader.provides[resource.Name], prVar)
+		}
 	}
 
-	logrus.Infof("Loaded %v packages.", len(pkgProvides))
+	logrus.Infof("Loaded %v packages.", len(pkgVars))
 
 	// Generate imply rules
-	for _, resourceVars := range pkgProvides {
+	for _, pkgVar := range pkgVars {
 		var ands []bf.Formula
 
-		// Synchronize all the variables for a given package to the same value.
-		pkgVar := resourceVars[len(resourceVars)-1].Var
-		for _, res := range resourceVars {
-			ands = append(ands, bf.Eq(bf.Var(pkgVar.satVarName), bf.Var(res.Var.satVarName)))
-		}
-
 		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)))
@@ -219,24 +206,6 @@ func (loader *Loader) explodeProvidedResources(pkg *api.Package) (provided []*Re
 	return
 }
 
-func (loader *Loader) explodePackageToVars(pkg *api.Package, resources []*Resource) (pkgVar *Var, resourceVars []*ResourceVar) {
-	for _, res := range resources {
-		newVar := &Var{
-			satVarName: loader.ticket(),
-			varType:    VarTypeResource,
-			Package:    pkg,
-		}
-
-		if res.Name == pkg.Name {
-			newVar.varType = VarTypePackage
-			pkgVar = newVar
-		}
-		resourceVars = append(resourceVars, &ResourceVar{Var: newVar, Resource: *res})
-	}
-
-	return pkgVar, resourceVars
-}
-
 // explodePackageRequires builds a formula that could be a right hand side operand to implication.
 // It consists of all direct requirements of a given package, exploded to resources that can satisfy these requirements.
 // Special cases include:
diff --git a/pkg/sat/loader_test.go b/pkg/sat/loader_test.go
index 21cf8074..6c82de70 100644
--- a/pkg/sat/loader_test.go
+++ b/pkg/sat/loader_test.go
@@ -170,7 +170,6 @@ func TestLoader_Load(t *testing.T) {
 	x3 := bf.Var("x3")
 	x4 := bf.Var("x4")
 	x5 := bf.Var("x5")
-	x6 := bf.Var("x6")
 
 	t.Run("Trivial Loading", func(t *testing.T) {
 		model, _ := doSimpleLoad([]*api.Package{}, false)
@@ -347,8 +346,7 @@ func TestLoader_Load(t *testing.T) {
 				g,
 				model,
 				"app-0:1.0",     // x1
-				"toolkit-0:2.0", // x2 (toolkit)
-				"toolkit-0:2.0", // x3 (/usr/bin/tool)
+				"toolkit-0:2.0", // x2
 			)
 			expectedBest(g, model, map[string]string{
 				"app":     "0:1.0",
@@ -358,7 +356,6 @@ func TestLoader_Load(t *testing.T) {
 			expectedAnds(g, model,
 				x1,                 // Install: app
 				bf.Implies(x1, x2), // Requirement: app => toolkit
-				bf.Eq(x2, x3),      // Equivalence (toolkit)
 			)
 		})
 
@@ -377,11 +374,9 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"apache-0:2.4", // (apache)
-				"apache-0:2.4", // (webserver)
-				"app-0:1.0",
-				"nginx-0:1.2", // (nginx)
-				"nginx-0:1.2", // (webserver)
+				"apache-0:2.4", // x1
+				"app-0:1.0",    // x2
+				"nginx-0:1.2",  // x3
 			)
 			expectedBest(g, model, map[string]string{
 				"app":    "0:1.0",
@@ -390,10 +385,8 @@ func TestLoader_Load(t *testing.T) {
 			})
 			expectedIgnores(g, model)
 			expectedAnds(g, model,
-				x3,                            // Install: app
-				bf.Implies(x3, bf.Or(x1, x4)), // Requirement: app => apache or nginx
-				bf.Eq(x1, x2),                 // Equivalence (apache)
-				bf.Eq(x4, x5),                 // Equivalence (nginx)
+				x2,                            // Install: app
+				bf.Implies(x2, bf.Or(x1, x3)), // Requirement: app => apache or nginx
 			)
 		})
 
@@ -434,7 +427,6 @@ func TestLoader_Load(t *testing.T) {
 				g,
 				model,
 				"platform-python-0:3.6",
-				"platform-python-0:3.6",
 			)
 			expectedBest(
 				g,
@@ -443,7 +435,7 @@ func TestLoader_Load(t *testing.T) {
 			)
 			expectedIgnores(g, model)
 			expectedAnds(g, model,
-				bf.Eq(x1, x2), // Equivalence (platform-python)
+				bf.True, // Nothing to install
 			)
 
 			// verify side effect
@@ -483,12 +475,9 @@ func TestLoader_Load(t *testing.T) {
 			expectedVars(
 				g,
 				model,
-				"gcc-0:11.0",   // x1 (gcc)
-				"gcc-0:11.0",   // x2 (gcc)
-				"gcc11-0:11.0", // x3 (gcc11)
-				"gcc11-0:11.0", // x4 (gcc)
-				"gcc11-0:11.0", // x5 (gcc11)
-				"pkgX-0:1.0",   // x6
+				"gcc-0:11.0",   // x1
+				"gcc11-0:11.0", // x2
+				"pkgX-0:1.0",   // x3
 			)
 			expectedBest(g, model, map[string]string{
 				"gcc":   "0:11.0",
@@ -497,12 +486,9 @@ func TestLoader_Load(t *testing.T) {
 			})
 
 			expectedAnds(g, model,
-				x6,                            // Install: pkgX
-				bf.Implies(x6, bf.Or(x1, x3)), // Requirement: pkgX => gcc or gcc11
-				bf.Implies(x1, x3),            // Requirement: gcc => gcc11
-				bf.Eq(x1, x2),                 // Equivalence (gcc)
-				bf.Eq(x3, x4),                 // Equivalence (gcc11)
-				bf.Eq(x3, x5),                 // Equivalence (gcc11)
+				x3,                            // Install: pkgX
+				bf.Implies(x3, bf.Or(x1, x2)), // Requirement: pkgX => gcc or gcc11
+				bf.Implies(x1, x2),            // Requirement: gcc => gcc11
 			)
 
 		})
diff --git a/pkg/sat/sat.go b/pkg/sat/sat.go
index 73185d5f..125dce9a 100644
--- a/pkg/sat/sat.go
+++ b/pkg/sat/sat.go
@@ -14,13 +14,6 @@ import (
 	"github.com/sirupsen/logrus"
 )
 
-type VarType string
-
-const (
-	VarTypePackage  = "Package"
-	VarTypeResource = "Resource" // includes files
-)
-
 // VarContext contains all information to create a unique identifyable hash key which can be traced back to a package
 // for every resource in a yum repo
 type VarContext struct {
@@ -30,7 +23,6 @@ type VarContext struct {
 
 type Var struct {
 	satVarName string
-	varType    VarType
 	Package    *api.Package
 }
 
@@ -162,16 +154,12 @@ func Resolve(model *Model) (install []*api.Package, excluded []*api.Package, for
 		installSet := map[*api.Package]struct{}{}
 		excludedSet := map[*api.Package]struct{}{}
 		forceIgnoreSet := map[*api.Package]struct{}{}
-		for _, resVar := range model.vars {
-			if resVar.varType != VarTypePackage {
-				continue
-			}
-
-			satVarName, exists := satVars.pkgToSat[resVar.satVarName]
+		for _, pkgVar := range model.vars {
+			satVarName, exists := satVars.pkgToSat[pkgVar.satVarName]
 			if !exists {
 				// A package might have not been used in the SAT formula (e.g. not requested, no requirements, conflicts, etc.)
 				// In such case we assume it's just not selected for installation.
-				excludedSet[resVar.Package] = struct{}{}
+				excludedSet[pkgVar.Package] = struct{}{}
 				continue
 			}
 			modelVarId, err := strconv.Atoi(satVarName)
@@ -181,13 +169,13 @@ func Resolve(model *Model) (install []*api.Package, excluded []*api.Package, for
 			}
 			// Offset of `1`. The model index starts with 0, but the variable sequence starts with 1, since 0 is not allowed
 			if solution.Model[modelVarId-1] {
-				if exists := model.ShouldIgnore(resVar.Package.Key()); !exists {
-					installSet[resVar.Package] = struct{}{}
+				if exists := model.ShouldIgnore(pkgVar.Package.Key()); !exists {
+					installSet[pkgVar.Package] = struct{}{}
 				} else {
-					forceIgnoreSet[resVar.Package] = struct{}{}
+					forceIgnoreSet[pkgVar.Package] = struct{}{}
 				}
 			} else {
-				excludedSet[resVar.Package] = struct{}{}
+				excludedSet[pkgVar.Package] = struct{}{}
 			}
 		}
 		for v := range installSet {