Give explaination when formulas are unsat

Fixes #168

Signed-off-by: Ettore Di Giacinto <[email protected]>

go.mod

@@ -10,7 +10,7 @@ require (
 	github.com/briandowns/spinner v1.12.1-0.20201220203425-e201aaea0a31
 	github.com/cavaliercoder/grab v1.0.1-0.20201108051000-98a5bfe305ec
 	github.com/containerd/containerd v1.4.1-0.20201117152358-0edc412565dc
-	github.com/crillab/gophersat v1.3.2-0.20201023142334-3fc2ac466765
+	github.com/crillab/gophersat v1.3.2-0.20210701121804-72b19f5b6b38
 	github.com/docker/cli v20.10.0-beta1.0.20201029214301-1d20b15adc38+incompatible
 	github.com/docker/distribution v2.7.1+incompatible
 	github.com/docker/docker v20.10.0-beta1.0.20201110211921-af34b94a78a1+incompatible

go.sum

@@ -339,6 +339,8 @@ github.com/creack/pty v1.1.7/go.mod h1:lj5s0c3V2DBrqTV7llrYr5NG6My20zk30Fl46Y7Do
 github.com/creack/pty v1.1.9/go.mod h1:oKZEueFk5CKHvIhNR5MUki03XCEU+Q6VDXinZuGJ33E=
 github.com/crillab/gophersat v1.3.2-0.20201023142334-3fc2ac466765 h1:EO5Dm7O50aaEwv1GTFWNLAj7vNQ1OjW3+DeJCy1vTMk=
 github.com/crillab/gophersat v1.3.2-0.20201023142334-3fc2ac466765/go.mod h1:S91tHga1PCZzYhCkStwZAhvp1rCc+zqtSi55I+vDWGc=
+github.com/crillab/gophersat v1.3.2-0.20210701121804-72b19f5b6b38 h1:sOsE90v/iPmouqh4d3cKQl8JuqTOEXg+fP+7YuY7R6U=
+github.com/crillab/gophersat v1.3.2-0.20210701121804-72b19f5b6b38/go.mod h1:S91tHga1PCZzYhCkStwZAhvp1rCc+zqtSi55I+vDWGc=
 github.com/cyphar/filepath-securejoin v0.2.2 h1:jCwT2GTP+PY5nBz3c/YL5PAIbusElVrPujOBSCj8xRg=
 github.com/cyphar/filepath-securejoin v0.2.2/go.mod h1:FpkQEhXnPnOthhzymB7CGsFk2G9VLXONKD9G7QGMM+4=
 github.com/davecgh/go-spew v0.0.0-20151105211317-5215b55f46b2/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=

pkg/compiler/compiler.go

@@ -758,7 +758,6 @@ func (cs *LuetCompiler) inheritSpecBuildOptions(p *compilerspec.LuetCompilationS
 func (cs *LuetCompiler) getSpecHash(pkgs pkg.DefaultPackages, salt string) (string, error) {
 	ht := NewHashTree(cs.Database)
 	overallFp := ""
-
 	for _, p := range pkgs {
 		compileSpec, err := cs.FromPackage(p)
 		if err != nil {

pkg/config/config.go

@@ -93,7 +93,7 @@ func (opts LuetSolverOptions) Resolver() solver.PackageResolver {
 		return solver.SimpleQLearningSolver()
 	}
 
-	return &solver.DummyPackageResolver{}
+	return &solver.Explainer{}
 }
 
 func (opts *LuetSolverOptions) CompactString() string {

pkg/solver/resolver.go

@@ -1,4 +1,4 @@
-// Copyright © 2020 Ettore Di Giacinto <mudler@gentoo.org>
+// Copyright © 2020-2021 Ettore Di Giacinto <mudler@mocaccino.org>
 //
 // This program is free software; you can redistribute it and/or modify
 // it under the terms of the GNU General Public License as published by
@@ -16,11 +16,16 @@
 package solver
 
 import (
+	"bufio"
+	"bytes"
 	"encoding/json"
 	"fmt"
+	"io"
 	"strconv"
+	"strings"
 
 	"github.com/crillab/gophersat/bf"
+	"github.com/crillab/gophersat/explain"
 	"github.com/mudler/luet/pkg/helpers"
 	"gopkg.in/yaml.v2"
 
@@ -51,18 +56,115 @@ const (
 	QLearningResolverType = "qlearning"
 )
 
-//. "github.com/mudler/luet/pkg/logger"
-
 // PackageResolver assists PackageSolver on unsat cases
 type PackageResolver interface {
 	Solve(bf.Formula, PackageSolver) (PackagesAssertions, error)
 }
 
-type DummyPackageResolver struct {
+type Explainer struct{}
+
+func decodeDimacs(vars map[string]string, dimacs string) (string, error) {
+	res := ""
+	sc := bufio.NewScanner(bytes.NewBufferString(dimacs))
+	lines := strings.Split(dimacs, "\n")
+	linenum := 1
+SCAN:
+	for sc.Scan() {
+
+		line := sc.Text()
+		fields := strings.Fields(line)
+		if len(fields) == 0 {
+			continue
+		}
+		switch fields[0] {
+		case "p":
+			continue SCAN
+		default:
+			for i := 0; i < len(fields)-1; i++ {
+				v := fields[i]
+				negative := false
+				if strings.HasPrefix(fields[i], "-") {
+					v = strings.TrimLeft(fields[i], "-")
+					negative = true
+				}
+				variable := vars[v]
+				if negative {
+					res += fmt.Sprintf("!(%s)", variable)
+				} else {
+					res += variable
+				}
+
+				if i != len(fields)-2 {
+					res += fmt.Sprintf(" or ")
+				}
+			}
+			if linenum != len(lines)-1 {
+				res += fmt.Sprintf(" and \n")
+			}
+		}
+		linenum++
+	}
+	if err := sc.Err(); err != nil {
+		return res, fmt.Errorf("could not parse problem: %v", err)
+	}
+	return res, nil
 }
 
-func (*DummyPackageResolver) Solve(bf.Formula, PackageSolver) (PackagesAssertions, error) {
-	return nil, errors.New("Could not satisfy the constraints. Try again by removing deps ")
+func parseVars(r io.Reader) (map[string]string, error) {
+	sc := bufio.NewScanner(r)
+	res := map[string]string{}
+	for sc.Scan() {
+		line := sc.Text()
+		fields := strings.Fields(line)
+		if len(fields) == 0 {
+			continue
+		}
+		switch fields[0] {
+		case "c":
+			data := strings.Split(fields[1], "=")
+			res[data[1]] = data[0]
+
+		default:
+			continue
+
+		}
+	}
+	if err := sc.Err(); err != nil {
+		return nil, fmt.Errorf("could not parse problem: %v", err)
+	}
+	return res, nil
+}
+
+// Solve tries to find the MUS (minimum unsat) formula from the original problem.
+// it returns an error with the decoded dimacs
+func (*Explainer) Solve(f bf.Formula, s PackageSolver) (PackagesAssertions, error) {
+	buf := bytes.NewBufferString("")
+	if err := bf.Dimacs(f, buf); err != nil {
+		return nil, errors.Wrap(err, "cannot extract dimacs from formula")
+	}
+
+	copy := *buf
+
+	pb, err := explain.ParseCNF(&copy)
+	if err != nil {
+		return nil, errors.Wrap(err, "could not parse problem")
+	}
+	pb2, err := pb.MUS()
+	if err != nil {
+		return nil, errors.Wrap(err, "could not extract subset")
+	}
+
+	variables, err := parseVars(buf)
+	if err != nil {
+		return nil, errors.Wrap(err, "could not parse variables")
+	}
+
+	res, err := decodeDimacs(variables, pb2.CNF())
+	if err != nil {
+		return nil, errors.Wrap(err, "could not parse dimacs")
+	}
+
+	return nil, fmt.Errorf("could not satisfy the constraints: \n%s", res)
 }
 
 type QLearningResolver struct {
@@ -103,8 +205,8 @@ func (resolver *QLearningResolver) Solve(f bf.Formula, s PackageSolver) (Package
 	//	Info("Using QLearning solver to resolve conflicts. Please be patient.")
 	resolver.Solver = s
 
-	s.SetResolver(&DummyPackageResolver{}) // Set dummy. Otherwise the attempts will run again a QLearning instance.
-	defer s.SetResolver(resolver)          // Set back ourselves as resolver
+	s.SetResolver(&Explainer{})   // Set dummy. Otherwise the attempts will run again a QLearning instance.
+	defer s.SetResolver(resolver) // Set back ourselves as resolver
 
 	resolver.Formula = f
 

pkg/solver/resolver_test.go

@@ -38,7 +38,7 @@ var _ = Describe("Resolver", func() {
 	})
 
 	Context("Conflict set", func() {
-		Context("DummyPackageResolver", func() {
+		Context("Explainer", func() {
 			It("is unsolvable - as we something we ask to install conflict with system stuff", func() {
 				C := pkg.NewPackage("C", "", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
 				B := pkg.NewPackage("B", "", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{C})
@@ -152,7 +152,7 @@ var _ = Describe("Resolver", func() {
 			})
 		})
 
-		Context("DummyPackageResolver", func() {
+		Context("Explainer", func() {
 			It("cannot find a solution", func() {
 				C := pkg.NewPackage("C", "", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
 				B := pkg.NewPackage("B", "", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{C})
@@ -171,6 +171,11 @@ var _ = Describe("Resolver", func() {
 
 				solution, err := s.Install([]pkg.Package{A, D})
 				Expect(err).To(HaveOccurred())
+				Expect(err.Error()).To(Equal(`could not satisfy the constraints: 
+A-- and 
+C-- and 
+!(A--) or B-- and 
+!(B--) or !(C--)`))
 
 				Expect(len(solution)).To(Equal(0))
 			})

pkg/solver/solver.go

@@ -71,7 +71,7 @@ type Options struct {
 // NewSolver accepts as argument two lists of packages, the first is the initial set,
 // the second represent all the known packages.
 func NewSolver(t Options, installed pkg.PackageDatabase, definitiondb pkg.PackageDatabase, solverdb pkg.PackageDatabase) PackageSolver {
-	return NewResolver(t, installed, definitiondb, solverdb, &DummyPackageResolver{})
+	return NewResolver(t, installed, definitiondb, solverdb, &Explainer{})
 }
 
 // NewResolver accepts as argument two lists of packages, the first is the initial set,