/ solver Public

SAT solver library in Go; wraps around Google's Operational Research Tools

# irfansharif/solver

Switch branches/tags
Nothing to show

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

## Latest commit

`9c33ad3`

## Files

Failed to load latest commit information.

## Solver

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.

### Examples

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)

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),
)

// 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")

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.

### Contributing

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```

#### Testing

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.*'```

### Acknowledgements

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.

SAT solver library in Go; wraps around Google's Operational Research Tools

## Releases

No releases published

## Packages 0

No packages published