From a9c6824f36aa4ed2efeaef5023bb5cba8c3940a3 Mon Sep 17 00:00:00 2001 From: perdasilva Date: Tue, 11 Oct 2022 11:44:44 +0200 Subject: [PATCH] Refactor solver to remove variables Signed-off-by: perdasilva --- internal/solver/bench_test.go | 34 ++- internal/solver/constraints.go | 348 ++++++++++++++++++++-------- internal/solver/constraints_test.go | 8 +- internal/solver/lit_mapping.go | 160 ++++++------- internal/solver/search.go | 14 +- internal/solver/search_test.go | 24 +- internal/solver/solve.go | 20 +- internal/solver/solve_test.go | 280 ++++++++-------------- internal/solver/tracer.go | 10 +- internal/solver/variable.go | 4 +- 10 files changed, 480 insertions(+), 422 deletions(-) diff --git a/internal/solver/bench_test.go b/internal/solver/bench_test.go index 289a016..59f46f3 100644 --- a/internal/solver/bench_test.go +++ b/internal/solver/bench_test.go @@ -7,7 +7,7 @@ import ( "testing" ) -var BenchmarkInput = func() []Variable { +var BenchmarkConstraints = func() []Constraint { const ( length = 256 seed = 9 @@ -22,10 +22,11 @@ var BenchmarkInput = func() []Variable { return Identifier(strconv.Itoa(i)) } - variable := func(i int) TestVariable { + input := func(i int) []Constraint { var c []Constraint + subject := id(i) if rand.Float64() < pMandatory { - c = append(c, Mandatory()) + c = append(c, Mandatory(subject)) } if rand.Float64() < pDependency { n := rand.Intn(nDependency-1) + 1 @@ -37,7 +38,7 @@ var BenchmarkInput = func() []Variable { } d = append(d, id(y)) } - c = append(c, Dependency(d...)) + c = append(c, Dependency(subject, d...)) } if rand.Float64() < pConflict { n := rand.Intn(nConflict-1) + 1 @@ -46,39 +47,34 @@ var BenchmarkInput = func() []Variable { for y == i { y = rand.Intn(length) } - c = append(c, Conflict(id(y))) + c = append(c, Conflict(subject, id(y))) } } - return TestVariable{ - identifier: id(i), - constraints: c, - } + return c } rand.Seed(seed) - result := make([]Variable, length) - for i := range result { - result[i] = variable(i) + constraints := make([]Constraint, 0) + for i := 0; i < length; i++ { + constrs := input(i) + constraints = append(constraints, constrs...) } - return result + return constraints }() func BenchmarkSolve(b *testing.B) { for i := 0; i < b.N; i++ { - s, err := New(WithInput(BenchmarkInput)) - if err != nil { - b.Fatalf("failed to initialize solver: %s", err) - } - _, err = s.Solve(context.Background()) + s, err := New(WithInput(BenchmarkConstraints)) if err != nil { b.Fatalf("failed to initialize solver: %s", err) } + s.Solve(context.Background()) } } func BenchmarkNewInput(b *testing.B) { for i := 0; i < b.N; i++ { - _, err := New(WithInput(BenchmarkInput)) + _, err := New(WithInput(BenchmarkConstraints)) if err != nil { b.Fatalf("failed to initialize solver: %s", err) } diff --git a/internal/solver/constraints.go b/internal/solver/constraints.go index b2b0b77..70e23ce 100644 --- a/internal/solver/constraints.go +++ b/internal/solver/constraints.go @@ -8,176 +8,173 @@ import ( "github.com/go-air/gini/z" ) -// Constraint implementations limit the circumstances under which a -// particular Variable can appear in a solution. type Constraint interface { - String(subject Identifier) string - apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit order() []Identifier anchor() bool + apply(c *logic.C, lm *litMapping) z.Lit + String() string + Subject() Identifier } -// zeroConstraint is returned by ConstraintOf in error cases. -type zeroConstraint struct{} - -var _ Constraint = zeroConstraint{} - -func (zeroConstraint) String(subject Identifier) string { - return "" +type mandatory struct { + subject Identifier } -func (zeroConstraint) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit { - return z.LitNull +func (constraint *mandatory) String() string { + return fmt.Sprintf("%s is mandatory", constraint.subject) } -func (zeroConstraint) order() []Identifier { - return nil +func (constraint *mandatory) apply(_ *logic.C, lm *litMapping) z.Lit { + return lm.LitOf(constraint.subject) } -func (zeroConstraint) anchor() bool { - return false +func (constraint *mandatory) order() []Identifier { + return nil } -// AppliedConstraint values compose a single Constraint with the -// Variable it applies to. -type AppliedConstraint struct { - Variable Variable - Constraint Constraint +func (constraint *mandatory) anchor() bool { + return true } -// String implements fmt.Stringer and returns a human-readable message -// representing the receiver. -func (a AppliedConstraint) String() string { - return a.Constraint.String(a.Variable.Identifier()) +func (constraint *mandatory) Subject() Identifier { + return constraint.subject } -type mandatory struct{} - -func (constraint mandatory) String(subject Identifier) string { - return fmt.Sprintf("%s is mandatory", subject) +func Mandatory(subject Identifier) Constraint { + return &mandatory{ + subject: subject, + } } -func (constraint mandatory) apply(_ *logic.C, lm *litMapping, subject Identifier) z.Lit { - return lm.LitOf(subject) +type prohibited struct { + subject Identifier } -func (constraint mandatory) order() []Identifier { +func (constraint *prohibited) order() []Identifier { return nil } -func (constraint mandatory) anchor() bool { - return true -} - -// Mandatory returns a Constraint that will permit only solutions that -// contain a particular Variable. -func Mandatory() Constraint { - return mandatory{} +func (constraint *prohibited) anchor() bool { + return false } -type prohibited struct{} - -func (constraint prohibited) String(subject Identifier) string { - return fmt.Sprintf("%s is prohibited", subject) +func (constraint *prohibited) apply(c *logic.C, lm *litMapping) z.Lit { + return lm.LitOf(constraint.subject).Not() } -func (constraint prohibited) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit { - return lm.LitOf(subject).Not() +func (constraint *prohibited) String() string { + return fmt.Sprintf("%s is prohibited", constraint.subject) } -func (constraint prohibited) order() []Identifier { - return nil +func (constraint *prohibited) Subject() Identifier { + return constraint.subject } -func (constraint prohibited) anchor() bool { - return false +func Prohibited(subject Identifier) Constraint { + return &prohibited{ + subject: subject, + } } -// Prohibited returns a Constraint that will reject any solution that -// contains a particular Variable. Callers may also decide to omit -// an Variable from input to Solve rather than apply such a -// Constraint. -func Prohibited() Constraint { - return prohibited{} +type dependency struct { + subject Identifier + dependencies []Identifier } -type dependency []Identifier - -func (constraint dependency) String(subject Identifier) string { - if len(constraint) == 0 { - return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", subject) +func (constraint *dependency) String() string { + if len(constraint.dependencies) == 0 { + return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", constraint.subject) } - s := make([]string, len(constraint)) - for i, each := range constraint { + s := make([]string, len(constraint.dependencies)) + for i, each := range constraint.dependencies { s[i] = string(each) } - return fmt.Sprintf("%s requires at least one of %s", subject, strings.Join(s, ", ")) + return fmt.Sprintf("%s requires at least one of %s", constraint.subject, strings.Join(s, ", ")) } -func (constraint dependency) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit { - m := lm.LitOf(subject).Not() - for _, each := range constraint { - m = c.Or(m, lm.LitOf(each)) +func (constraint *dependency) apply(c *logic.C, lm *litMapping) z.Lit { + m := lm.LitOf(constraint.subject).Not() + ms := make([]z.Lit, len(constraint.dependencies)) + for i, each := range constraint.dependencies { + ms[i] = lm.LitOf(each) } - return m + return c.Ors(append(ms, m)...) } -func (constraint dependency) order() []Identifier { - return constraint +func (constraint *dependency) order() []Identifier { + return constraint.dependencies } -func (constraint dependency) anchor() bool { +func (constraint *dependency) anchor() bool { return false } +func (constraint *dependency) Subject() Identifier { + return constraint.subject +} + // Dependency returns a Constraint that will only permit solutions -// containing a given Variable on the condition that at least one -// of the Variables identified by the given Identifiers also +// containing a given *DeppyEntity on the condition that at least one +// of the Entities identified by the given Identifiers also // appears in the solution. Identifiers appearing earlier in the // argument list have higher preference than those appearing later. -func Dependency(ids ...Identifier) Constraint { - return dependency(ids) +func Dependency(subject Identifier, dependencies ...Identifier) Constraint { + return &dependency{ + subject: subject, + dependencies: dependencies, + } } -type conflict Identifier +type conflict struct { + subject Identifier + conflict Identifier +} -func (constraint conflict) String(subject Identifier) string { - return fmt.Sprintf("%s conflicts with %s", subject, constraint) +func (constraint *conflict) String() string { + return fmt.Sprintf("%s conflicts with %s", constraint.subject, constraint.conflict) } -func (constraint conflict) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit { - return c.Or(lm.LitOf(subject).Not(), lm.LitOf(Identifier(constraint)).Not()) +func (constraint *conflict) apply(c *logic.C, lm *litMapping) z.Lit { + return c.Or(lm.LitOf(constraint.subject).Not(), lm.LitOf(constraint.conflict).Not()) } -func (constraint conflict) order() []Identifier { +func (constraint *conflict) order() []Identifier { return nil } -func (constraint conflict) anchor() bool { +func (constraint *conflict) anchor() bool { return false } +func (constraint *conflict) Subject() Identifier { + return constraint.subject +} + // Conflict returns a Constraint that will permit solutions containing -// either the constrained Variable, the Variable identified by +// either the constrained *DeppyEntity, the *DeppyEntity identified by // the given Identifier, or neither, but not both. -func Conflict(id Identifier) Constraint { - return conflict(id) +func Conflict(subject Identifier, conlict Identifier) Constraint { + return &conflict{ + subject: subject, + conflict: conlict, + } } -type leq struct { - ids []Identifier - n int +type atMost struct { + subject Identifier + ids []Identifier + n int } -func (constraint leq) String(subject Identifier) string { +func (constraint *atMost) String() string { s := make([]string, len(constraint.ids)) for i, each := range constraint.ids { s[i] = string(each) } - return fmt.Sprintf("%s permits at most %d of %s", subject, constraint.n, strings.Join(s, ", ")) + return fmt.Sprintf("at most %d of %s are permitted", constraint.n, strings.Join(s, ", ")) } -func (constraint leq) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit { +func (constraint *atMost) apply(c *logic.C, lm *litMapping) z.Lit { ms := make([]z.Lit, len(constraint.ids)) for i, each := range constraint.ids { ms[i] = lm.LitOf(each) @@ -185,20 +182,171 @@ func (constraint leq) apply(c *logic.C, lm *litMapping, subject Identifier) z.Li return c.CardSort(ms).Leq(constraint.n) } -func (constraint leq) order() []Identifier { +func (constraint *atMost) order() []Identifier { return nil } -func (constraint leq) anchor() bool { +func (constraint *atMost) anchor() bool { return false } +func (constraint *atMost) Subject() Identifier { + return "" +} + // AtMost returns a Constraint that forbids solutions that contain -// more than n of the Variables identified by the given +// more than n of the Entities identified by the given // Identifiers. -func AtMost(n int, ids ...Identifier) Constraint { - return leq{ - ids: ids, - n: n, +func AtMost(subject Identifier, n int, ids ...Identifier) Constraint { + return &atMost{ + subject: subject, + ids: ids, + n: n, + } +} + +type and struct { + clauses []Constraint +} + +func And(clauses ...Constraint) Constraint { + return &and{ + clauses: clauses, + } +} + +func (constraint *and) String() string { + collectIds := func() []string { + ids := make([]string, len(constraint.clauses)) + for i, clause := range constraint.clauses { + ids[i] = clause.String() + } + return ids + } + return fmt.Sprintf("%s are required", strings.Join(collectIds(), " and ")) +} + +func (constraint *and) apply(c *logic.C, lm *litMapping) z.Lit { + collectTerms := func() []z.Lit { + terms := make([]z.Lit, len(constraint.clauses)) + for i, clause := range constraint.clauses { + terms[i] = clause.apply(c, lm) + } + return terms } + return c.Ands(collectTerms()...) +} + +func (constraint *and) order() []Identifier { + return nil +} + +func (constraint *and) anchor() bool { + return false +} + +func (constraint *and) Subject() Identifier { + return "" +} + +type or struct { + clauses []Constraint +} + +func Or(clauses ...Constraint) Constraint { + return &or{ + clauses: clauses, + } +} + +func (constraint *or) String() string { + collectIds := func() []string { + ids := make([]string, len(constraint.clauses)) + for i, clause := range constraint.clauses { + ids[i] = clause.String() + } + return ids + } + return fmt.Sprintf("%s are required", strings.Join(collectIds(), " or ")) +} + +func (constraint *or) apply(c *logic.C, lm *litMapping) z.Lit { + collectTerms := func() []z.Lit { + terms := make([]z.Lit, len(constraint.clauses)) + for i, clause := range constraint.clauses { + terms[i] = clause.apply(c, lm) + } + return terms + } + return c.Ors(collectTerms()...) +} + +func (constraint *or) order() []Identifier { + return nil +} + +func (constraint *or) anchor() bool { + return false +} + +func (constraint *or) Subject() Identifier { + return "" +} + +type not struct { + clause Constraint +} + +func Not(clause Constraint) Constraint { + return ¬{ + clause: clause, + } +} + +func (constraint *not) String() string { + return fmt.Sprintf("not %s", constraint.clause.String()) +} + +func (constraint *not) apply(c *logic.C, lm *litMapping) z.Lit { + return constraint.clause.apply(c, lm).Not() +} + +func (constraint *not) order() []Identifier { + return nil +} + +func (constraint *not) anchor() bool { + return false +} + +func (constraint *not) Subject() Identifier { + return "" +} + +// zeroConstraint is returned by ConstraintOf in error cases. +type zeroConstraint struct { +} + +var _ Constraint = &zeroConstraint{} + +var ZeroConstraint = &zeroConstraint{} + +func (*zeroConstraint) String() string { + return "" +} + +func (*zeroConstraint) apply(_ *logic.C, _ *litMapping) z.Lit { + return z.LitNull +} + +func (*zeroConstraint) order() []Identifier { + return nil +} + +func (*zeroConstraint) anchor() bool { + return false +} + +func (*zeroConstraint) Subject() Identifier { + return "" } diff --git a/internal/solver/constraints_test.go b/internal/solver/constraints_test.go index 4bd0a2e..0a6b182 100644 --- a/internal/solver/constraints_test.go +++ b/internal/solver/constraints_test.go @@ -16,20 +16,20 @@ func TestOrder(t *testing.T) { for _, tt := range []tc{ { Name: "mandatory", - Constraint: Mandatory(), + Constraint: Mandatory("a"), }, { Name: "prohibited", - Constraint: Prohibited(), + Constraint: Prohibited("b"), }, { Name: "dependency", Constraint: Dependency("a", "b", "c"), - Expected: []Identifier{"a", "b", "c"}, + Expected: []Identifier{"b", "c"}, }, { Name: "conflict", - Constraint: Conflict("a"), + Constraint: Conflict("a", "b"), }, } { t.Run(tt.Name, func(t *testing.T) { diff --git a/internal/solver/lit_mapping.go b/internal/solver/lit_mapping.go index eb7a739..fdefb30 100644 --- a/internal/solver/lit_mapping.go +++ b/internal/solver/lit_mapping.go @@ -22,94 +22,76 @@ func (inconsistentLitMapping) Error() string { } // litMapping performs translation between the input and output types of -// Solve (Constraints, Variables, etc.) and the variables that +// Solve (Constraints, Constraints, etc.) and the variables that // appear in the SAT formula. type litMapping struct { - inorder []Variable - variables map[z.Lit]Variable - lits map[Identifier]z.Lit - constraints map[z.Lit]AppliedConstraint - c *logic.C - errs inconsistentLitMapping + inorder []Constraint + constraintsByLiteral map[z.Lit][]Constraint + lits map[Identifier]z.Lit + constraints map[z.Lit]Constraint + c *logic.C + errs inconsistentLitMapping } // newLitMapping returns a new litMapping with its state initialized based on -// the provided slice of Variables. This includes construction of -// the translation tables between Variables/Constraints and the +// the provided slice of Entities. This includes construction of +// the translation tables between Entities/Constraints and the // inputs to the underlying solver. -func newLitMapping(variables []Variable) (*litMapping, error) { +func newLitMapping(constraints []Constraint) (*litMapping, error) { d := litMapping{ - inorder: variables, - variables: make(map[z.Lit]Variable, len(variables)), - lits: make(map[Identifier]z.Lit, len(variables)), - constraints: make(map[z.Lit]AppliedConstraint), - c: logic.NewCCap(len(variables)), - } - - // First pass to assign lits: - for _, variable := range variables { - im := d.c.Lit() - if _, ok := d.lits[variable.Identifier()]; ok { - return nil, DuplicateIdentifier(variable.Identifier()) - } - d.lits[variable.Identifier()] = im - d.variables[im] = variable - } - - for _, variable := range variables { - for _, constraint := range variable.Constraints() { - m := constraint.apply(d.c, &d, variable.Identifier()) - if m == z.LitNull { - // This constraint doesn't have a - // useful representation in the SAT - // inputs. - continue - } - - d.constraints[m] = AppliedConstraint{ - Variable: variable, - Constraint: constraint, - } + inorder: make([]Constraint, len(constraints)), + constraintsByLiteral: make(map[z.Lit][]Constraint, 0), + lits: make(map[Identifier]z.Lit, 0), + constraints: make(map[z.Lit]Constraint), + c: logic.NewC(), + } + + for i, constraint := range constraints { + d.inorder[i] = constraints[i] + + m := constraint.apply(d.c, &d) + if m == z.LitNull { + // This constraint doesn't have a + // useful representation in the SAT + // inputs. + continue } + + d.constraints[m] = constraint + litForVar := d.lits[constraint.Subject()] + d.constraintsByLiteral[litForVar] = append(d.constraintsByLiteral[litForVar], constraint) } return &d, nil } -// LitOf returns the positive literal corresponding to the Variable +// LitOf returns the positive literal corresponding to the *DeppyEntity // with the given Identifier. func (d *litMapping) LitOf(id Identifier) z.Lit { - m, ok := d.lits[id] - if ok { - return m + _, ok := d.lits[id] + if !ok { + d.lits[id] = d.c.Lit() } - d.errs = append(d.errs, fmt.Errorf("variable %q referenced but not provided", id)) - return z.LitNull + return d.lits[id] } -// VariableOf returns the Variable corresponding to the provided -// literal, or a zeroVariable if no such Variable exists. -func (d *litMapping) VariableOf(m z.Lit) Variable { - i, ok := d.variables[m] +func (d *litMapping) ConstraintsFor(m z.Lit) []Constraint { + constrs, ok := d.constraintsByLiteral[m] if ok { - return i + return constrs } - d.errs = append(d.errs, fmt.Errorf("no variable corresponding to %s", m)) - return zeroVariable{} + return nil } // ConstraintOf returns the constraint application corresponding to // the provided literal, or a zeroConstraint if no such constraint // exists. -func (d *litMapping) ConstraintOf(m z.Lit) AppliedConstraint { +func (d *litMapping) ConstraintOf(m z.Lit) Constraint { if a, ok := d.constraints[m]; ok { return a } d.errs = append(d.errs, fmt.Errorf("no constraint corresponding to %s", m)) - return AppliedConstraint{ - Variable: zeroVariable{}, - Constraint: zeroConstraint{}, - } + return ZeroConstraint } // Error returns a single error value that is an aggregation of all @@ -134,8 +116,10 @@ func (d *litMapping) AddConstraints(g inter.S) { } func (d *litMapping) AssumeConstraints(s inter.S) { - for m := range d.constraints { - s.Assume(m) + for m, c := range d.constraints { + if !c.anchor() { + s.Assume(m) + } } } @@ -158,46 +142,33 @@ func (d *litMapping) CardinalityConstrainer(g inter.Adder, ms []z.Lit) *logic.Ca } // AnchorIdentifiers returns a slice containing the Identifiers of -// every Variable with at least one "anchor" constraint, in the +// every variable with at least one "anchor" constraint, in the // order they appear in the input. func (d *litMapping) AnchorIdentifiers() []Identifier { var ids []Identifier - for _, variable := range d.inorder { - for _, constraint := range variable.Constraints() { - if constraint.anchor() { - ids = append(ids, variable.Identifier()) - break - } + for _, c := range d.inorder { + if c.anchor() { + ids = append(ids, c.Subject()) } } - return ids -} -func (d *litMapping) Variables(g inter.S) []Variable { - var result []Variable - for _, i := range d.inorder { - if g.Value(d.LitOf(i.Identifier())) { - result = append(result, i) - } - } - return result + return ids } func (d *litMapping) Lits(dst []z.Lit) []z.Lit { - if cap(dst) < len(d.inorder) { - dst = make([]z.Lit, 0, len(d.inorder)) + if cap(dst) < len(d.lits) { + dst = make([]z.Lit, 0, len(d.lits)) } dst = dst[:0] - for _, i := range d.inorder { - m := d.LitOf(i.Identifier()) - dst = append(dst, m) + for _, lit := range d.lits { + dst = append(dst, lit) } return dst } -func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint { +func (d *litMapping) Conflicts(g inter.Assumable) []Constraint { whys := g.Why(nil) - as := make([]AppliedConstraint, 0, len(whys)) + as := make([]Constraint, 0, len(whys)) for _, why := range whys { if a, ok := d.constraints[why]; ok { as = append(as, a) @@ -205,3 +176,22 @@ func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint { } return as } + +func (d *litMapping) Selection(g inter.S) []Identifier { + selection := make([]Identifier, 0) + for id, lit := range d.lits { + if g.Value(lit) { + selection = append(selection, id) + } + } + return selection +} + +func (d *litMapping) IdentifierOf(lit z.Lit) Identifier { + for id, literal := range d.lits { + if literal == lit { + return id + } + } + return Identifier("nil") +} diff --git a/internal/solver/search.go b/internal/solver/search.go index 523b311..88609c2 100644 --- a/internal/solver/search.go +++ b/internal/solver/search.go @@ -56,10 +56,10 @@ func (h *search) PushGuess() { return } - variable := h.lits.VariableOf(g.m) - for _, constraint := range variable.Constraints() { + constrs := h.lits.ConstraintsFor(g.m) + for _, constr := range constrs { var ms []z.Lit - for _, dependency := range constraint.order() { + for _, dependency := range constr.order() { ms = append(ms, h.lits.LitOf(dependency)) } if len(ms) > 0 { @@ -202,16 +202,16 @@ func (h *search) Do(ctx context.Context, anchors []z.Lit) (int, []z.Lit, map[z.L return result, lits, set } -func (h *search) Variables() []Variable { - result := make([]Variable, 0, len(h.guesses)) +func (h *search) Identifiers() []Identifier { + result := make([]Identifier, 0, len(h.guesses)) for _, g := range h.guesses { if g.m != z.LitNull { - result = append(result, h.lits.VariableOf(g.candidates[g.index])) + result = append(result, h.lits.IdentifierOf(g.candidates[g.index])) } } return result } -func (h *search) Conflicts() []AppliedConstraint { +func (h *search) Conflicts() []Constraint { return h.lits.Conflicts(h.s) } diff --git a/internal/solver/search_test.go b/internal/solver/search_test.go index fd9221a..32d1461 100644 --- a/internal/solver/search_test.go +++ b/internal/solver/search_test.go @@ -31,7 +31,7 @@ func (c *TestScopeCounter) Untest() (result int) { func TestSearch(t *testing.T) { type tc struct { Name string - Variables []Variable + Constraints []Constraint TestReturns []int UntestReturns []int Result int @@ -41,10 +41,10 @@ func TestSearch(t *testing.T) { for _, tt := range []tc{ { Name: "children popped from back of deque when guess popped", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("c")), - variable("b", Mandatory()), - variable("c"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "c"), + Mandatory("b"), }, TestReturns: []int{0, -1}, UntestReturns: []int{-1, -1}, @@ -53,11 +53,11 @@ func TestSearch(t *testing.T) { }, { Name: "candidates exhausted", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("x")), - variable("b", Mandatory(), Dependency("y")), - variable("x"), - variable("y"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "x"), + Mandatory("b"), + Dependency("b", "y"), }, TestReturns: []int{0, 0, -1, 1}, UntestReturns: []int{0}, @@ -79,7 +79,7 @@ func TestSearch(t *testing.T) { var depth int counter := &TestScopeCounter{depth: &depth, S: &s} - lits, err := newLitMapping(tt.Variables) + lits, err := newLitMapping(tt.Constraints) assert.NoError(err) h := search{ s: counter, @@ -97,7 +97,7 @@ func TestSearch(t *testing.T) { assert.Equal(tt.Result, result) var ids []Identifier for _, m := range ms { - ids = append(ids, lits.VariableOf(m).Identifier()) + ids = append(ids, lits.IdentifierOf(m)) } assert.Equal(tt.Assumptions, ids) assert.Equal(0, depth) diff --git a/internal/solver/solve.go b/internal/solver/solve.go index 766fa60..acf79b1 100644 --- a/internal/solver/solve.go +++ b/internal/solver/solve.go @@ -4,6 +4,7 @@ import ( "context" "errors" "fmt" + "sort" "strings" "github.com/go-air/gini" @@ -15,7 +16,7 @@ var ErrIncomplete = errors.New("cancelled before a solution could be found") // NotSatisfiable is an error composed of a minimal set of applied // constraints that is sufficient to make a solution impossible. -type NotSatisfiable []AppliedConstraint +type NotSatisfiable []Constraint func (e NotSatisfiable) Error() string { const msg = "constraints not satisfiable" @@ -26,11 +27,12 @@ func (e NotSatisfiable) Error() string { for i, a := range e { s[i] = a.String() } + sort.Strings(s) return fmt.Sprintf("%s: %s", msg, strings.Join(s, ", ")) } type Solver interface { - Solve(context.Context) ([]Variable, error) + Solve(context.Context) ([]Identifier, error) } type solver struct { @@ -46,11 +48,11 @@ const ( unknown = 0 ) -// Solve takes a slice containing all Variables and returns a slice -// containing only those Variables that were selected for +// Solve takes a slice containing all Entities and returns a slice +// containing only those Entities that were selected for // installation. If no solution is possible, or if the provided // Context times out or is cancelled, an error is returned. -func (s *solver) Solve(ctx context.Context) (result []Variable, err error) { +func (s *solver) Solve(ctx context.Context) (result []Identifier, err error) { defer func() { // This likely indicates a bug, so discard whatever // return values were produced. @@ -64,7 +66,7 @@ func (s *solver) Solve(ctx context.Context) (result []Variable, err error) { s.litMap.AddConstraints(s.g) // collect literals of all mandatory variables to assume as a baseline - assumptions := []z.Lit{} + var assumptions []z.Lit for _, anchor := range s.litMap.AnchorIdentifiers() { assumptions = append(assumptions, s.litMap.LitOf(anchor)) } @@ -104,7 +106,7 @@ func (s *solver) Solve(ctx context.Context) (result []Variable, err error) { for w := 0; w <= cs.N(); w++ { s.g.Assume(cs.Leq(w)) if s.g.Solve() == satisfiable { - return s.litMap.Variables(s.g), nil + return s.litMap.Selection(s.g), nil } } // Something is wrong if we can't find a model anymore @@ -129,10 +131,10 @@ func New(options ...Option) (Solver, error) { type Option func(s *solver) error -func WithInput(input []Variable) Option { +func WithInput(constraints []Constraint) Option { return func(s *solver) error { var err error - s.litMap, err = newLitMapping(input) + s.litMap, err = newLitMapping(constraints) return err } } diff --git a/internal/solver/solve_test.go b/internal/solver/solve_test.go index d9ec36a..afb9d82 100644 --- a/internal/solver/solve_test.go +++ b/internal/solver/solve_test.go @@ -3,9 +3,7 @@ package solver import ( "bytes" "context" - "errors" "fmt" - "reflect" "sort" "testing" @@ -56,28 +54,19 @@ func TestNotSatisfiableError(t *testing.T) { { Name: "single failure", Error: NotSatisfiable{ - AppliedConstraint{ - Variable: variable("a", Mandatory()), - Constraint: Mandatory(), - }, + Mandatory("a"), }, String: fmt.Sprintf("constraints not satisfiable: %s", - Mandatory().String("a")), + Mandatory("a").String()), }, { Name: "multiple failures", Error: NotSatisfiable{ - AppliedConstraint{ - Variable: variable("a", Mandatory()), - Constraint: Mandatory(), - }, - AppliedConstraint{ - Variable: variable("b", Prohibited()), - Constraint: Prohibited(), - }, + Mandatory("a"), + Prohibited("b"), }, String: fmt.Sprintf("constraints not satisfiable: %s, %s", - Mandatory().String("a"), Prohibited().String("b")), + Mandatory("a").String(), Prohibited("b").String()), }, } { t.Run(tt.Name, func(t *testing.T) { @@ -88,210 +77,184 @@ func TestNotSatisfiableError(t *testing.T) { func TestSolve(t *testing.T) { type tc struct { - Name string - Variables []Variable - Installed []Identifier - Error error + Name string + Constraints []Constraint + Installed []Identifier + Error error } for _, tt := range []tc{ { - Name: "no variables", + Name: "no variables", + Installed: []Identifier{}, }, { - Name: "unnecessary variable is not installed", - Variables: []Variable{variable("a")}, + Name: "single mandatory variable is installed", + Constraints: []Constraint{Mandatory("a")}, + Installed: []Identifier{"a"}, }, { - Name: "single mandatory variable is installed", - Variables: []Variable{variable("a", Mandatory())}, - Installed: []Identifier{"a"}, - }, - { - Name: "both mandatory and prohibited produce error", - Variables: []Variable{variable("a", Mandatory(), Prohibited())}, + Name: "both mandatory and prohibited produce error", + Constraints: []Constraint{Mandatory("a"), Prohibited("a")}, Error: NotSatisfiable{ - { - Variable: variable("a", Mandatory(), Prohibited()), - Constraint: Mandatory(), - }, - { - Variable: variable("a", Mandatory(), Prohibited()), - Constraint: Prohibited(), - }, + Mandatory("a"), + Prohibited("a"), }, }, { Name: "dependency is installed", - Variables: []Variable{ - variable("a"), - variable("b", Mandatory(), Dependency("a")), + Constraints: []Constraint{ + Mandatory("b"), + Dependency("b", "a"), }, Installed: []Identifier{"a", "b"}, }, { Name: "transitive dependency is installed", - Variables: []Variable{ - variable("a"), - variable("b", Dependency("a")), - variable("c", Mandatory(), Dependency("b")), + Constraints: []Constraint{ + Dependency("b", "a"), + Mandatory("c"), + Dependency("c", "b"), }, Installed: []Identifier{"a", "b", "c"}, }, { Name: "both dependencies are installed", - Variables: []Variable{ - variable("a"), - variable("b"), - variable("c", Mandatory(), Dependency("a"), Dependency("b")), + Constraints: []Constraint{ + Mandatory("c"), + Dependency("c", "a"), + Dependency("c", "b"), }, Installed: []Identifier{"a", "b", "c"}, }, { Name: "solution with first dependency is selected", - Variables: []Variable{ - variable("a"), - variable("b", Conflict("a")), - variable("c", Mandatory(), Dependency("a", "b")), + Constraints: []Constraint{ + Conflict("b", "a"), + Mandatory("c"), + Dependency("c", "a", "b"), }, Installed: []Identifier{"a", "c"}, }, { Name: "solution with only first dependency is selected", - Variables: []Variable{ - variable("a"), - variable("b"), - variable("c", Mandatory(), Dependency("a", "b")), + Constraints: []Constraint{ + Mandatory("c"), + Dependency("c", "a", "b"), }, Installed: []Identifier{"a", "c"}, }, { Name: "solution with first dependency is selected (reverse)", - Variables: []Variable{ - variable("a"), - variable("b", Conflict("a")), - variable("c", Mandatory(), Dependency("b", "a")), + Constraints: []Constraint{ + Conflict("b", "a"), + Mandatory("c"), + Dependency("c", "b", "a"), }, Installed: []Identifier{"b", "c"}, }, { Name: "two mandatory but conflicting packages", - Variables: []Variable{ - variable("a", Mandatory()), - variable("b", Mandatory(), Conflict("a")), + Constraints: []Constraint{ + Mandatory("b"), + Mandatory("a"), + Conflict("b", "a"), }, Error: NotSatisfiable{ - { - Variable: variable("a", Mandatory()), - Constraint: Mandatory(), - }, - { - Variable: variable("b", Mandatory(), Conflict("a")), - Constraint: Mandatory(), - }, - { - Variable: variable("b", Mandatory(), Conflict("a")), - Constraint: Conflict("a"), - }, + Mandatory("a"), + Mandatory("b"), + Conflict("b", "a"), }, }, { Name: "irrelevant dependencies don't influence search order", - Variables: []Variable{ - variable("a", Dependency("x", "y")), - variable("b", Mandatory(), Dependency("y", "x")), - variable("x"), - variable("y"), + Constraints: []Constraint{ + Dependency("a", "x", "y"), + Mandatory("b"), + Dependency("b", "y", "x"), }, Installed: []Identifier{"b", "y"}, }, { Name: "cardinality constraint prevents resolution", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")), - variable("x", Mandatory()), - variable("y", Mandatory()), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "x", "y"), + Mandatory("x"), + Mandatory("y"), + AtMost("a", 1, "x", "y"), }, Error: NotSatisfiable{ - { - Variable: variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")), - Constraint: AtMost(1, "x", "y"), - }, - { - Variable: variable("x", Mandatory()), - Constraint: Mandatory(), - }, - { - Variable: variable("y", Mandatory()), - Constraint: Mandatory(), - }, + Mandatory("y"), + Mandatory("x"), + AtMost("a", 1, "x", "y"), }, }, { Name: "cardinality constraint forces alternative", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")), - variable("b", Mandatory(), Dependency("y")), - variable("x"), - variable("y"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "x", "y"), + AtMost("a", 1, "x", "y"), + Mandatory("b"), + Dependency("b", "y"), }, Installed: []Identifier{"a", "b", "y"}, }, { Name: "two dependencies satisfied by one variable", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("y")), - variable("b", Mandatory(), Dependency("x", "y")), - variable("x"), - variable("y"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "y"), + Mandatory("b"), + Dependency("b", "x", "y"), }, Installed: []Identifier{"a", "b", "y"}, }, { Name: "foo two dependencies satisfied by one variable", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("y", "z", "m")), - variable("b", Mandatory(), Dependency("x", "y")), - variable("x"), - variable("y"), - variable("z"), - variable("m"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "y", "z", "m"), + Mandatory("b"), + Dependency("b", "x", "y"), }, Installed: []Identifier{"a", "b", "y"}, }, { Name: "result size larger than minimum due to preference", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("x", "y")), - variable("b", Mandatory(), Dependency("y")), - variable("x"), - variable("y"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "x", "y"), + Mandatory("b"), + Dependency("b", "y"), }, Installed: []Identifier{"a", "b", "x", "y"}, }, { Name: "only the least preferable choice is acceptable", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("a1", "a2")), - variable("a1", Conflict("c1"), Conflict("c2")), - variable("a2", Conflict("c1")), - variable("b", Mandatory(), Dependency("b1", "b2")), - variable("b1", Conflict("c1"), Conflict("c2")), - variable("b2", Conflict("c1")), - variable("c", Mandatory(), Dependency("c1", "c2")), - variable("c1"), - variable("c2"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "a1", "a2"), + Conflict("a1", "c1"), + Conflict("a1", "c2"), + Conflict("a2", "c1"), + Mandatory("b"), + Dependency("b", "b1", "b2"), + Conflict("b1", "c1"), + Conflict("b1", "c2"), + Conflict("b2", "c1"), + Mandatory("c"), + Dependency("c", "c1", "c2"), }, Installed: []Identifier{"a", "a2", "b", "b2", "c", "c2"}, }, { Name: "preferences respected with multiple dependencies per variable", - Variables: []Variable{ - variable("a", Mandatory(), Dependency("x1", "x2"), Dependency("y1", "y2")), - variable("x1"), - variable("x2"), - variable("y1"), - variable("y2"), + Constraints: []Constraint{ + Mandatory("a"), + Dependency("a", "x1", "x2"), + Dependency("a", "y1", "y2"), }, Installed: []Identifier{"a", "x1", "y1"}, }, @@ -300,7 +263,7 @@ func TestSolve(t *testing.T) { assert := assert.New(t) var traces bytes.Buffer - s, err := New(WithInput(tt.Variables), WithTracer(LoggingTracer{Writer: &traces})) + s, err := New(WithInput(tt.Constraints), WithTracer(LoggingTracer{Writer: &traces})) if err != nil { t.Fatalf("failed to initialize solver: %s", err) } @@ -309,44 +272,11 @@ func TestSolve(t *testing.T) { if installed != nil { sort.SliceStable(installed, func(i, j int) bool { - return installed[i].Identifier() < installed[j].Identifier() - }) - } - - // Failed constraints are sorted in lexically - // increasing order of the identifier of the - // constraint's variable, with ties broken - // in favor of the constraint that appears - // earliest in the variable's list of - // constraints. - var ns NotSatisfiable - if errors.As(err, &ns) { - sort.SliceStable(ns, func(i, j int) bool { - if ns[i].Variable.Identifier() != ns[j].Variable.Identifier() { - return ns[i].Variable.Identifier() < ns[j].Variable.Identifier() - } - var x, y int - for ii, c := range ns[i].Variable.Constraints() { - if reflect.DeepEqual(c, ns[i].Constraint) { - x = ii - break - } - } - for ij, c := range ns[j].Variable.Constraints() { - if reflect.DeepEqual(c, ns[j].Constraint) { - y = ij - break - } - } - return x < y + return installed[i] < installed[j] }) } - var ids []Identifier - for _, variable := range installed { - ids = append(ids, variable.Identifier()) - } - assert.Equal(tt.Installed, ids) + assert.Equal(tt.Installed, installed) assert.Equal(tt.Error, err) if t.Failed() { @@ -355,11 +285,3 @@ func TestSolve(t *testing.T) { }) } } - -func TestDuplicateIdentifier(t *testing.T) { - _, err := New(WithInput([]Variable{ - variable("a"), - variable("a"), - })) - assert.Equal(t, DuplicateIdentifier("a"), err) -} diff --git a/internal/solver/tracer.go b/internal/solver/tracer.go index b103536..c876df2 100644 --- a/internal/solver/tracer.go +++ b/internal/solver/tracer.go @@ -6,8 +6,8 @@ import ( ) type SearchPosition interface { - Variables() []Variable - Conflicts() []AppliedConstraint + Identifiers() []Identifier + Conflicts() []Constraint } type Tracer interface { @@ -25,10 +25,10 @@ type LoggingTracer struct { func (t LoggingTracer) Trace(p SearchPosition) { fmt.Fprintf(t.Writer, "---\nAssumptions:\n") - for _, i := range p.Variables() { - fmt.Fprintf(t.Writer, "- %s\n", i.Identifier()) + for _, i := range p.Identifiers() { + fmt.Fprintf(t.Writer, "- %s\n", i) } - fmt.Fprintf(t.Writer, "Conflicts:\n") + fmt.Fprintf(t.Writer, "Conflict:\n") for _, a := range p.Conflicts() { fmt.Fprintf(t.Writer, "- %s\n", a) } diff --git a/internal/solver/variable.go b/internal/solver/variable.go index 32afab7..c98f0e1 100644 --- a/internal/solver/variable.go +++ b/internal/solver/variable.go @@ -1,6 +1,6 @@ package solver -// Identifier values uniquely identify particular Variables within +// Identifier values uniquely identify particular Identifiers within // the input to a single call to Solve. type Identifier string @@ -18,7 +18,7 @@ func IdentifierFromString(s string) Identifier { // understood by this package. type Variable interface { // Identifier returns the Identifier that uniquely identifies - // this Variable among all other Variables in a given + // this Variable among all other Identifiers in a given // problem. Identifier() Identifier // Constraints returns the set of constraints that apply to