Use New Solver Interface (#8)

Uses the new helper functions for clause construction.

go.mod

@@ -9,7 +9,7 @@ require (
 	github.com/google/uuid v1.6.0
 	github.com/oapi-codegen/runtime v1.1.1
 	github.com/spf13/pflag v1.0.5
-	github.com/spjmurray/go-sat v0.1.1
+	github.com/spjmurray/go-sat v0.1.4
 	github.com/stretchr/testify v1.9.0
 	github.com/unikorn-cloud/core v0.1.80
 	github.com/unikorn-cloud/identity v0.2.44

go.sum

@@ -126,8 +126,10 @@ github.com/rogpeppe/go-internal v1.13.1 h1:KvO1DLK/DRN07sQ1LQKScxyZJuNnedQ5/wKSR
 github.com/rogpeppe/go-internal v1.13.1/go.mod h1:uMEvuHeurkdAXX61udpOXGD/AzZDWNMNyH2VO9fmH0o=
 github.com/spf13/pflag v1.0.5 h1:iy+VFUOCP1a+8yFto/drg2CJ5u0yRoB7fZw3DKv/JXA=
 github.com/spf13/pflag v1.0.5/go.mod h1:McXfInJRrz4CZXVZOBLb0bTZqETkiAhM9Iw0y3An2Bg=
-github.com/spjmurray/go-sat v0.1.1 h1:XWptzXLXu5XRt1xPnl1WpF+lKy2/YebetDBS9aazTMs=
-github.com/spjmurray/go-sat v0.1.1/go.mod h1:PfXzQbyb3Tucoyw9jNb3/Kj0VQUrK2KQ8F1NWBvCPPk=
+github.com/spjmurray/go-sat v0.1.3 h1:IGOyIzAakh14QxrZNFbkWiASTr86Xss4HL5BQEe4bO0=
+github.com/spjmurray/go-sat v0.1.3/go.mod h1:PfXzQbyb3Tucoyw9jNb3/Kj0VQUrK2KQ8F1NWBvCPPk=
+github.com/spjmurray/go-sat v0.1.4 h1:/vwYhTbCsQE5VctcjScMPH6sNsuc7+AdHKTeeWA+joA=
+github.com/spjmurray/go-sat v0.1.4/go.mod h1:PfXzQbyb3Tucoyw9jNb3/Kj0VQUrK2KQ8F1NWBvCPPk=
 github.com/spkg/bom v0.0.0-20160624110644-59b7046e48ad/go.mod h1:qLr4V1qq6nMqFKkMo8ZTx3f+BZEkzsRUY10Xsm2mwU0=
 github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME=
 github.com/stretchr/testify v1.3.0/go.mod h1:M5WIy9Dh21IEIfnGCwXGc5bZfKNJtfHm1UVUgZn+9EI=

pkg/provisioners/managers/application/provisioner.go

@@ -175,8 +175,11 @@ func (q *Queue[T]) Pop() T {
 	return value
 }
 
-func varName(applicationID string, version *unikornv1core.SemanticVersion) string {
-	return applicationID + "=" + version.String()
+// AppVersion wraps up applicationID and version tuples in a comparable
+// and easy to use form when interacting with the SAT solver.
+type AppVersion struct {
+	applicationID string
+	version       unikornv1core.SemanticVersion
 }
 
 // SolveApplicationSet walks the graph Dykstra style loading in referenced dependencies.
@@ -187,15 +190,15 @@ func varName(applicationID string, version *unikornv1core.SemanticVersion) strin
 // effect of changing its dependencies!
 //
 //nolint:cyclop,gocognit
-func SolveApplicationSet(ctx context.Context, client client.Client, namespace string, applicationset *unikornv1.ApplicationSet) error {
+func SolveApplicationSet(ctx context.Context, client client.Client, namespace string, applicationset *unikornv1.ApplicationSet) ([]AppVersion, error) {
 	applications, err := getApplications(ctx, client, namespace)
 	if err != nil {
-		return err
+		return nil, err
 	}
 
-	solver := sat.NewCDCLSolver()
+	solver := sat.NewCDCLSolver[AppVersion]()
 
-	// Pass 1 is going to do an exhaustive walk of the dependency graph gathering
+	// We're going to do an exhaustive walk of the dependency graph gathering
 	// all application/version tuples as variables, and also create any clauses along the way.
 	queue := Queue[string]{}
 
@@ -204,7 +207,7 @@ func SolveApplicationSet(ctx context.Context, client client.Client, namespace st
 	for _, ref := range applicationset.Spec.Applications {
 		application, ok := applications[ref.Application.Name]
 		if !ok {
-			return fmt.Errorf("%w: requested application %s not in catalog", ErrResourceDependency, ref.Application.Name)
+			return nil, fmt.Errorf("%w: requested application %s not in catalog", ErrResourceDependency, ref.Application.Name)
 		}
 
 		queue.Push(ref.Application.Name)
@@ -213,27 +216,30 @@ func SolveApplicationSet(ctx context.Context, client client.Client, namespace st
 		if ref.Version != nil {
 			// Non existent version asked for.
 			if _, err := application.GetVersion(*ref.Version); err != nil {
-				return err
+				return nil, err
 			}
 
-			solver.Clause(solver.Literal(varName(ref.Application.Name, ref.Version)))
+			solver.Unary(AppVersion{ref.Application.Name, *ref.Version})
 
 			continue
 		}
 
 		// Otherise we must install at least one version.
+		// NOTE: we cheat a bit here, when making a choice the solver will pick
+		// the first undefined variable and set it to true, so we implicitly
+		// choose the most recent version by adding them in a descending order.
 		versions := slices.Collect(application.Versions())
 		if len(versions) == 0 {
-			return fmt.Errorf("%w: requested application %s has no versions", ErrResourceDependency, application.Name)
+			return nil, fmt.Errorf("%w: requested application %s has no versions", ErrResourceDependency, application.Name)
 		}
 
-		l := make([]*sat.Literal, 0, len(application.Spec.Versions))
+		l := make([]AppVersion, len(versions))
 
-		for _, version := range slices.Backward(slices.Collect(application.Versions())) {
-			l = append(l, solver.Literal(varName(application.Name, &version.Version)))
+		for i, version := range slices.Backward(versions) {
+			l[i] = AppVersion{application.Name, version.Version}
 		}
 
-		solver.Clause(l...)
+		solver.AtLeastOneOf(l...)
 	}
 
 	visited := map[string]bool{}
@@ -249,54 +255,68 @@ func SolveApplicationSet(ctx context.Context, client client.Client, namespace st
 
 		application, ok := applications[id]
 		if !ok {
-			return fmt.Errorf("%w: unable to locate application %s", ErrResourceDependency, id)
+			return nil, fmt.Errorf("%w: unable to locate application %s", ErrResourceDependency, id)
 		}
 
-		for i, version := range application.Spec.Versions {
-			name := varName(application.Name, &version.Version)
+		appVersions := make([]AppVersion, 0, len(application.Spec.Versions))
 
-			// Only one version of the application may be installed at any time...
-			// We basically do a permute of all possible combinations and if both
-			// are true, we want a false, so ^(A ^ B) or ^A v ^B.
-			for _, other := range application.Spec.Versions[i+1:] {
-				solver.Clause(solver.NegatedLiteral(name), solver.NegatedLiteral(varName(application.Name, &other.Version)))
-			}
+		for version := range application.Versions() {
+			appVersions = append(appVersions, AppVersion{application.Name, version.Version})
+		}
 
-			// Next if an application version is installed, we need to ensure any
-			// dependent applications are also installed, but constrained to the allowed
-			// set for this application.  So A => B v C v D becomes ^A v B v C v D.
-			// This also has the property that if a version has no satisfiable deps e.g.
-			// A => , then it will add a unit clause ^A to ensure it cannot be installed.
-			for _, dependency := range version.Dependencies {
-				dependantApplication := applications[dependency.Name]
+		// Only one version of the application may be installed at any time...
+		solver.AtMostOneOf(appVersions...)
+
+		// Next if an application version is installed, we need to ensure any
+		// dependent applications are also installed, but constrained to the allowed
+		// set for this application. This also has the property that if a version has
+		// no satisfiable deps e.g. then it will add a unary clause that prevents the
+		// version from being used.
+		for version := range application.Versions() {
+			av := AppVersion{application.Name, version.Version}
 
-				l := []*sat.Literal{
-					solver.NegatedLiteral(name),
+			for _, dependency := range version.Dependencies {
+				dependantApplication, ok := applications[dependency.Name]
+				if !ok {
+					return nil, fmt.Errorf("%w: requested application %s not in catalog", ErrResourceDependency, dependency.Name)
 				}
 
+				depVersions := make([]AppVersion, 0, len(dependantApplication.Spec.Versions))
+
 				for _, depVersion := range slices.Backward(slices.Collect(dependantApplication.Versions())) {
 					if dependency.Constraints == nil || dependency.Constraints.Check(&depVersion.Version) {
-						l = append(l, solver.Literal(varName(dependency.Name, &depVersion.Version)))
+						depVersions = append(depVersions, AppVersion{dependency.Name, depVersion.Version})
 					}
 				}
 
-				solver.Clause(l...)
+				solver.ImpliesAtLeastOneOf(av, depVersions...)
 
-				queue.Push(dependency.Name)
+				if len(depVersions) > 0 {
+					queue.Push(dependency.Name)
+				}
 			}
 		}
 	}
 
-	// Pass 2 does the actual solving...
+	// Solve the problem.
 	if !solver.Solve(sat.DefaultChooser) {
-		return fmt.Errorf("%w: unsolvable", ErrConstraint)
+		return nil, fmt.Errorf("%w: unsolvable", ErrConstraint)
 	}
 
-	return nil
+	// Get the result.
+	result := []AppVersion{}
+
+	for av, b := range solver.Variables() {
+		if b.Value() {
+			result = append(result, av)
+		}
+	}
+
+	return result, nil
 }
 
 func GenerateProvisioner(ctx context.Context, client client.Client, namespace string, applicationset *unikornv1.ApplicationSet) (provisioners.Provisioner, error) {
-	err := SolveApplicationSet(ctx, client, namespace, applicationset)
+	_, err := SolveApplicationSet(ctx, client, namespace, applicationset)
 	if err != nil {
 		return nil, err
 	}

pkg/provisioners/managers/application/provisioner_test.go

@@ -199,33 +199,6 @@ func (b *applicationSetBuilder) get() *unikornv1.ApplicationSet {
 	}
 }
 
-/*
-// validate checks each node in the graph, every dependency should have been
-// defined already, have its constraints satisfied.
-// TODO: given all the constraints on an application, have we selected the
-// most recent?
-func validate(t *testing.T, graph *application.Graph) {
-	t.Helper()
-
-	applications := map[string]*unikornv1core.HelmApplication{}
-	versions := map[string]*unikornv1core.HelmApplicationVersion{}
-
-	for a, v := range graph.All() {
-		applications[a.Name] = a
-		versions[a.Name] = v
-
-		for _, dependency := range v.Dependencies {
-			_, ok := applications[dependency.Name]
-			require.True(t, ok, "application dependency should be defined already")
-
-			if dependency.Constraints != nil {
-				require.True(t, dependency.Constraints.Check(&versions[dependency.Name].Version), "application constraints should be satisfied")
-			}
-		}
-	}
-}
-*/
-
 // TestProvisionSingle tests a single app is solved.
 func TestProvisionSingle(t *testing.T) {
 	t.Parallel()
@@ -235,7 +208,8 @@ func TestProvisionSingle(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }
 
 // TestProvisionSingleMostRecent tests a single app is solved with the most recent version
@@ -248,7 +222,8 @@ func TestProvisionSingleMostRecent(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }
 
 // TestProvisionSingleNoMatch tests single app failure when a version constraint doesn't exist.
@@ -260,7 +235,8 @@ func TestProvisionSingleNoMatch(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app).Build()
 
-	require.Error(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.Error(t, err)
 }
 
 // TestProvisionSingleWithDependency tests a single application with a met dependency.
@@ -273,7 +249,8 @@ func TestProvisionSingleWithDependency(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app, dep).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }
 
 // TestProvisionSingleWithDependencyNoMatch tests a single application with an unmet dependency.
@@ -286,7 +263,8 @@ func TestProvisionSingleWithDependencyNoMatch(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app, dep).Build()
 
-	require.Error(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.Error(t, err)
 }
 
 // TestProvisionMultipleWithDependencyConflict tests that two apps with conflicting dependency
@@ -305,7 +283,8 @@ func TestProvisionMultipleWithDependencyConflict(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app1, app2, dep).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }
 
 // TestProvisionSingleWithConflictingTransitveDependency tests that two apps with conflicting dependency
@@ -328,7 +307,8 @@ func TestProvisionSingleWithConflictingTransitveDependency(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app, dep, intermediateDep).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }
 
 func TestProvisionSingleWithChoice(t *testing.T) {
@@ -362,5 +342,6 @@ func TestProvisionSingleWithChoice(t *testing.T) {
 
 	client := fake.NewClientBuilder().WithScheme(scheme(t)).WithObjects(app, dep, idep1, idep2).Build()
 
-	require.NoError(t, application.SolveApplicationSet(context.Background(), client, namespace, applicationset))
+	_, err := application.SolveApplicationSet(context.Background(), client, namespace, applicationset)
+	require.NoError(t, err)
 }