This is a SAT solver library; underneath the hood it's using cgo and links against Google's Operations Research Tools. It exposes a high-level package for the CP-SAT Solver, targeting the v9.1 release.
Here's a simple example solving for free integer variables, ensuring that they're all different.
model := NewModel() var numVals int64 = 3 x := model.NewIntVar(0, numVals-1, "x") y := model.NewIntVar(0, numVals-1, "y") z := model.NewIntVar(0, numVals-1, "z") ct := NewAllDifferentConstraint(x, y, z) model.AddConstraints(ct) result := model.Solve() require.True(t, result.Optimal(), "expected solver to find solution") { x := result.Value(x) y := result.Value(y) z := result.Value(z) for _, value := range []int64{x, y, z} { require.Truef(t, value >= 0 && value <= numVals-1, "expected %d to be in domain [%d, %d]", value, 0, numVals-1) } require.Falsef(t, x == y || x == z || y == z, "all different constraint violated, both x=%d y=%d z=%d", x, y, z) }
Here's another solving with a few linear constraints and a maximization objective.
model := NewModel() x := model.NewIntVar(0, 100, "x") y := model.NewIntVar(0, 100, "y") // Constraint 1: x + 2y <= 14. ct1 := NewLinearConstraint( NewLinearExpr([]IntVar{x, y}, []int64{1, 2}, 0), NewDomain(math.MinInt64, 14), ) // Constraint 2: 3x - y >= 0. ct2 := NewLinearConstraint( NewLinearExpr([]IntVar{x, y}, []int64{3, -1}, 0), NewDomain(0, math.MaxInt64), ) // Constraint 3: x - y <= 2. ct3 := NewLinearConstraint( NewLinearExpr([]IntVar{x, y}, []int64{1, -1}, 0), NewDomain(0, 2), ) model.AddConstraints(ct1, ct2, ct3) // Objective function: 3x + 4y. model.Maximize(NewLinearExpr([]IntVar{x, y}, []int64{3, 4}, 0)) result := model.Solve() require.True(t, result.Optimal(), "expected solver to find solution") { x := result.Value(x) y := result.Value(y) require.Equal(t, int64(6), x) require.Equal(t, int64(4), y) require.Equal(t, float64(34), result.ObjectiveValue()) }
Finally, an example solving for arbitrary boolean constraints.
model := NewModel() a := model.NewLiteral("a") b := model.NewLiteral("b") c := model.NewLiteral("c") d := model.NewLiteral("d") e := model.NewLiteral("e") f := model.NewLiteral("f") model.AddConstraints( NewBooleanAndConstraint(a, b), // a && b NewBooleanOrConstraint(c, d), // c || d NewBooleanXorConstraint(e, f), // e != f ) result := model.Solve() require.True(t, result.Optimal(), "expected solver to find solution") { a := result.BooleanValue(a) b := result.BooleanValue(b) c := result.BooleanValue(c) d := result.BooleanValue(d) e := result.BooleanValue(e) f := result.BooleanValue(f) require.True(t, a && b) require.True(t, c || d) require.True(t, e != f) }
For more, look through the package tests and the docs.
The Go/C++ binding code is generated using SWIG and can
be found under internal/. SWIG generated code is ugly and difficult to work
with; a sanitized API is exposed via the top-level package.
Because of the C++ dependencies, the library is compiled/tested using Bazel. The top-level Makefile packages most things you'd need.
# ensure that the submodules are initialized: # git submodule update --init --recursive # # supported bazel version >= 4.0.0 # supported swig version == 4.0.2 # supported protoc version == 3.14.0 # supported protoc-gen-go version == 1.27.1 $ make help Supported commands: build, test, generate, rewrite $ make generate --- generating go:generate files --- generating swig files --- generating proto files --- generating bazel files ok $ make build ok $ make test ... INFO: Build completed successfully, 4 total actions
This library is tested using the (awesome)
datadriven library + a tiny
testing grammar. See testdata/ for what that looks like.
sat
model.name(ex)
model.literals(x, y, z)
constrain.at-most-k(x to z | 2)
model.print()
----
model=ex
literals (num = 3)
x, y, z
constraints (num = 1)
at-most-k: x, y, z | 2
sat
model.solve()
----
optimal
sat
result.bools(x to z)
----
x = false
y = false
z = false
# to update the testdata files $ make rewrite # to run specific tests $ bazel test ... --test_output=all \ --cache_test_results=no \ --test_arg='-test.v' \ --test_filter='Test.*'
The SWIG interface files to work with protobufs was cribbed from AirspaceTechnologies/or-tools. To figure out how to structure this package as a stand-alone bazel target, I looked towards from gonzojive/or-tools-go. The CP-SAT stuff was then mostly pattern matching.