Skip to content

Commit a86ee09

Browse files
authored
Merge pull request #1440 from benluddy/sat
Add initial SAT solver package.
2 parents 22aff73 + 01de370 commit a86ee09

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

58 files changed

+7369
-0
lines changed

go.mod

+1
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ require (
1111
github.com/go-bindata/go-bindata/v3 v3.1.3
1212
github.com/go-openapi/spec v0.19.4
1313
github.com/golang/mock v1.3.1
14+
github.com/irifrance/gini v1.0.1
1415
github.com/maxbrunsfeld/counterfeiter/v6 v6.2.2
1516
github.com/mikefarah/yq/v2 v2.4.1
1617
github.com/mitchellh/hashstructure v1.0.0

go.sum

+2
Original file line numberDiff line numberDiff line change
@@ -372,6 +372,8 @@ github.com/imdario/mergo v0.3.7 h1:Y+UAYTZ7gDEuOfhxKWy+dvb5dRQ6rJjFSdX2HZY1/gI=
372372
github.com/imdario/mergo v0.3.7/go.mod h1:2EnlNZ0deacrJVfApfmtdGgDfMuh/nq6Ok1EcJh5FfA=
373373
github.com/inconshreveable/mousetrap v1.0.0 h1:Z8tu5sraLXCXIcARxBp/8cbvlwVa7Z1NHg9XEKhtSvM=
374374
github.com/inconshreveable/mousetrap v1.0.0/go.mod h1:PxqpIevigyE2G7u3NXJIT2ANytuPF1OarO4DADm73n8=
375+
github.com/irifrance/gini v1.0.1 h1:oTABiARLoRsnTmda0uY2u2e5kfm8e6meBZB19lf5xhE=
376+
github.com/irifrance/gini v1.0.1/go.mod h1:swH5OTtiG/X/YrU06r288qZwq6I1agpbuXQOB55xqGU=
375377
github.com/jackc/fake v0.0.0-20150926172116-812a484cc733/go.mod h1:WrMFNQdiFJ80sQsxDoMokWK1W5TQtxBFNpzWTD84ibQ=
376378
github.com/jackc/pgx v3.2.0+incompatible/go.mod h1:0ZGrqGqkRlliWnWB4zKnWtjbSWbGkVEFm4TeybAXq+I=
377379
github.com/jmespath/go-jmespath v0.0.0-20160202185014-0b12d6b521d8/go.mod h1:Nht3zPeWKUH0NzdCt2Blrr5ys8VGpn0CEB0cQHVjt7k=
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
package sat
2+
3+
import (
4+
"context"
5+
"math/rand"
6+
"strconv"
7+
"testing"
8+
9+
"github.com/irifrance/gini"
10+
)
11+
12+
func generateInput() []Installable {
13+
const (
14+
length = 256
15+
seed = 9
16+
pMandatory = .1
17+
pDependency = .15
18+
nDependency = 6
19+
pConflict = .05
20+
nConflict = 3
21+
pWeight = 0
22+
nWeight = 4
23+
)
24+
25+
id := func(i int) Identifier {
26+
return Identifier(strconv.Itoa(i))
27+
}
28+
29+
installable := func(i int) TestInstallable {
30+
var c []Constraint
31+
if rand.Float64() < pMandatory {
32+
c = append(c, Mandatory())
33+
}
34+
if rand.Float64() < pDependency {
35+
n := rand.Intn(nDependency-1) + 1
36+
var d []Identifier
37+
for x := 0; x < n; x++ {
38+
y := i
39+
for y == i {
40+
y = rand.Intn(length)
41+
}
42+
d = append(d, id(y))
43+
}
44+
c = append(c, Dependency(d...))
45+
}
46+
if rand.Float64() < pConflict {
47+
n := rand.Intn(nConflict-1) + 1
48+
for x := 0; x < n; x++ {
49+
y := i
50+
for y == i {
51+
y = rand.Intn(length)
52+
}
53+
c = append(c, Conflict(id(y)))
54+
}
55+
}
56+
if rand.Float64() < pWeight {
57+
n := rand.Intn(nWeight-1) + 1
58+
c = append(c, Weight(n))
59+
}
60+
return TestInstallable{
61+
identifier: id(i),
62+
constraints: c,
63+
}
64+
}
65+
66+
rand.Seed(seed)
67+
result := make([]Installable, length)
68+
for i := range result {
69+
result[i] = installable(i)
70+
}
71+
return result
72+
}
73+
74+
func BenchmarkCompileDict(b *testing.B) {
75+
input := generateInput()
76+
77+
b.ResetTimer()
78+
for i := 0; i < b.N; i++ {
79+
compileDict(input)
80+
}
81+
}
82+
83+
func BenchmarkDictSolve(b *testing.B) {
84+
d := compileDict(generateInput())
85+
86+
b.ResetTimer()
87+
for i := 0; i < b.N; i++ {
88+
g := gini.New()
89+
d.Solve(context.Background(), g)
90+
}
91+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
package sat
2+
3+
import (
4+
"fmt"
5+
"strings"
6+
)
7+
8+
// Constraint implementations limit the circumstances under which a
9+
// particular Installable can appear in a solution.
10+
type Constraint interface {
11+
String(subject Identifier) string
12+
apply(x constrainer, subject Identifier)
13+
}
14+
15+
// AppliedConstraint values compose a single Constraint with the
16+
// Installable it applies to.
17+
type AppliedConstraint struct {
18+
Installable Installable
19+
Constraint Constraint
20+
}
21+
22+
// String implements fmt.Stringer and returns a human-readable message
23+
// representing the receiver.
24+
func (a AppliedConstraint) String() string {
25+
return a.Constraint.String(a.Installable.Identifier())
26+
}
27+
28+
// constrainer is the set of operations available to Constraint
29+
// implementations.
30+
type constrainer interface {
31+
// Add appends the Installable identified by the given
32+
// Identifier to the clause representing a Constraint.
33+
Add(Identifier)
34+
// Add appends the negation of the Installable identified by
35+
// the given Identifier to the clause representing a
36+
// Constraint.
37+
AddNot(Identifier)
38+
// Weight sets an additional weight to add to the constrained
39+
// Installable. Calls with negative arguments are ignored.
40+
Weight(int)
41+
}
42+
43+
type mandatory struct{}
44+
45+
func (c mandatory) String(subject Identifier) string {
46+
return fmt.Sprintf("%s is mandatory", subject)
47+
}
48+
49+
func (c mandatory) apply(x constrainer, subject Identifier) {
50+
x.Add(subject)
51+
}
52+
53+
// Mandatory returns a Constraint that will permit only solutions that
54+
// contain a particular Installable.
55+
func Mandatory() Constraint {
56+
return mandatory{}
57+
}
58+
59+
type prohibited struct{}
60+
61+
func (c prohibited) String(subject Identifier) string {
62+
return fmt.Sprintf("%s is prohibited", subject)
63+
}
64+
65+
func (c prohibited) apply(x constrainer, subject Identifier) {
66+
x.AddNot(subject)
67+
}
68+
69+
// Prohibited returns a Constraint that will reject any solution that
70+
// contains a particular Installable. Callers may also decide to omit
71+
// an Installable from input to Solve rather than apply such a
72+
// Constraint.
73+
func Prohibited() Constraint {
74+
return prohibited{}
75+
}
76+
77+
type dependency []Identifier
78+
79+
func (c dependency) String(subject Identifier) string {
80+
s := make([]string, len(c))
81+
for i, each := range c {
82+
s[i] = string(each)
83+
}
84+
return fmt.Sprintf("%s requires at least one of %s", subject, strings.Join(s, ", "))
85+
}
86+
87+
func (c dependency) apply(x constrainer, subject Identifier) {
88+
if len(c) == 0 {
89+
return
90+
}
91+
x.AddNot(subject)
92+
for _, each := range c {
93+
x.Add(each)
94+
}
95+
}
96+
97+
// Dependency returns a Constraint that will only permit solutions
98+
// containing a given Installable on the condition that at least one
99+
// of the Installables identified by the given Identifiers also
100+
// appears in the solution.
101+
func Dependency(ids ...Identifier) Constraint {
102+
return dependency(ids)
103+
}
104+
105+
type conflict Identifier
106+
107+
func (c conflict) String(subject Identifier) string {
108+
return fmt.Sprintf("%s conflicts with %s", subject, c)
109+
}
110+
111+
func (c conflict) apply(x constrainer, subject Identifier) {
112+
x.AddNot(subject)
113+
x.AddNot(Identifier(c))
114+
}
115+
116+
// Conflict returns a Constraint that will permit solutions containing
117+
// either the constrained Installable, the Installable identified by
118+
// the given Identifier, or neither, but not both.
119+
func Conflict(id Identifier) Constraint {
120+
return conflict(id)
121+
}
122+
123+
type weight int
124+
125+
func (c weight) String(subject Identifier) string {
126+
return fmt.Sprintf("%s has weight %d", subject, c)
127+
}
128+
129+
func (c weight) apply(x constrainer, subject Identifier) {
130+
x.Weight(int(c))
131+
}
132+
133+
// Weight returns a Constraint that increases the weight of the
134+
// constrainted Installable by the given (non-negative) amount.
135+
func Weight(w int) Constraint {
136+
return weight(w)
137+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
package sat
2+
3+
import (
4+
"sort"
5+
"testing"
6+
7+
"github.com/stretchr/testify/assert"
8+
)
9+
10+
func TestConstraints(t *testing.T) {
11+
type tc struct {
12+
Name string
13+
Constraint Constraint
14+
Subject Identifier
15+
Expected cstate
16+
}
17+
18+
for _, tt := range []tc{
19+
{
20+
Name: "mandatory",
21+
Constraint: Mandatory(),
22+
Subject: "a",
23+
Expected: cstate{
24+
pos: []Identifier{"a"},
25+
},
26+
},
27+
{
28+
Name: "prohibited",
29+
Constraint: Prohibited(),
30+
Subject: "a",
31+
Expected: cstate{
32+
neg: []Identifier{"a"},
33+
},
34+
},
35+
{
36+
Name: "empty dependency",
37+
Constraint: Dependency(),
38+
Subject: "a",
39+
Expected: cstate{},
40+
},
41+
{
42+
Name: "single dependency",
43+
Constraint: Dependency("b"),
44+
Subject: "a",
45+
Expected: cstate{
46+
pos: []Identifier{"b"},
47+
neg: []Identifier{"a"},
48+
},
49+
},
50+
{
51+
Name: "multiple dependency",
52+
Constraint: Dependency("x", "y", "z"),
53+
Subject: "a",
54+
Expected: cstate{
55+
pos: []Identifier{"x", "y", "z"},
56+
neg: []Identifier{"a"},
57+
},
58+
},
59+
{
60+
Name: "conflict",
61+
Constraint: Conflict("b"),
62+
Subject: "a",
63+
Expected: cstate{
64+
neg: []Identifier{"a", "b"},
65+
},
66+
},
67+
{
68+
Name: "negative weight",
69+
Constraint: Weight(-1),
70+
Subject: "a",
71+
Expected: cstate{},
72+
},
73+
{
74+
Name: "weight",
75+
Constraint: Weight(5),
76+
Subject: "a",
77+
Expected: cstate{
78+
weight: 5,
79+
},
80+
},
81+
} {
82+
t.Run(tt.Name, func(t *testing.T) {
83+
var x cstate
84+
tt.Constraint.apply(&x, tt.Subject)
85+
86+
// Literals in lexically increasing order:
87+
sort.Slice(x.pos, func(i, j int) bool {
88+
return x.pos[i] < x.pos[j]
89+
})
90+
sort.Slice(x.neg, func(i, j int) bool {
91+
return x.neg[i] < x.neg[j]
92+
})
93+
94+
assert.Equal(t, tt.Expected, x)
95+
})
96+
}
97+
}

0 commit comments

Comments
 (0)