solver

package module
v0.0.0-...-9c33ad3 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Jul 13, 2022 License: Apache-2.0 Imports: 10 Imported by: 1

README

Solver

Go Reference

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

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.

Documentation

Overview

Package solver is a Go wrapper library for the CP-SAT Solver included as part Google's Operations Research tools.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

This section is empty.

Types

type Constraint 

type Constraint interface {
	// OnlyEnforceIf enforces the constraint iff all literals listed are true. If
	// not explicitly called, of if the list is empty, then the constraint will
	// always be enforced.
	//
	// NB: Only a few constraints support enforcement:
	// - NewBooleanOrConstraint
	// - NewBooleanAndConstraint
	// - NewLinearConstraint
	//
	// Intervals support enforcement too, but only with a single literal.
	OnlyEnforceIf(literals ...Literal) Constraint

	// Stringer provides a printable format representation for the constraint.
	fmt.Stringer

	// WithName sets a name for the constraint; used for debugging/logging
	// purposes.
	//
	// TODO(irfansharif): We don't use it in our pretty printing, yet. That
	// aside it would be nice to have a unified way to name things. For intvars,
	// literal, intervals -- it's provided as part of initializer. We use
	// separate things for models and constraints.
	WithName(name string) Constraint
	// contains filtered or unexported methods
}

Constraint is what a model attempts to satisfy when deciding on a solution.

func NewAllDifferentConstraint 

func NewAllDifferentConstraint(vars ...IntVar) Constraint

NewAllDifferentConstraint forces all variables to take different values.

func NewAllSameConstraint 

func NewAllSameConstraint(vars ...IntVar) Constraint

NewAllSameConstraint forces all variables to take the same values.

func NewAllowedAssignmentsConstraint 

func NewAllowedAssignmentsConstraint(vars []IntVar, assignments [][]int64) Constraint

NewAllowedAssignmentsConstraint ensures that the values of the n-tuple formed by the given variables is one of the listed n-tuple assignments.

func NewAllowedLiteralAssignmentsConstraint 

func NewAllowedLiteralAssignmentsConstraint(literals []Literal, assignments [][]bool) Constraint

NewAllowedLiteralAssignmentsConstraint ensures that the values of the n-tuple formed by the given literals is one of the listed n-tuple assignments.

func NewAtLeastKConstraint 

func NewAtLeastKConstraint(k int, literals ...Literal) Constraint

NewAtLeastKConstraint ensures that at least k literals are true.

func NewAtMostKConstraint 

func NewAtMostKConstraint(k int, literals ...Literal) Constraint

NewAtMostKConstraint ensures that no more than k literals are true.

func NewBooleanAndConstraint 

func NewBooleanAndConstraint(literals ...Literal) Constraint

NewBooleanAndConstraint ensures that all literals are true.

func NewBooleanOrConstraint 

func NewBooleanOrConstraint(literals ...Literal) Constraint

NewBooleanOrConstraint ensures that at least one literal is true. It can be thought of as a special case of NewAtLeastKConstraint, but one that uses a more efficient internal encoding.

func NewBooleanXorConstraint 

func NewBooleanXorConstraint(literals ...Literal) Constraint

NewBooleanXorConstraint ensures that an odd number of the literals are true.

func NewCumulativeConstraint 

func NewCumulativeConstraint(capacity IntVar, intervals []Interval, demands []IntVar) Constraint

NewCumulativeConstraint ensures that the sum of the demands of the intervals (intervals[i]'s demand is specified in demands[i]) at each interval point cannot exceed a max capacity. The intervals are interpreted as [start, end). Intervals of size zero are ignored.

func NewDivisionConstraint 

func NewDivisionConstraint(target, numerator, denominator IntVar) Constraint

NewDivisionConstraint ensures that the target is to equal to numerator/denominator. It also ensures that the denominator is non-zero.

func NewElementConstraint 

func NewElementConstraint(target, index IntVar, vars ...IntVar) Constraint

NewElementConstraint ensures that the target is equal to vars[index]. Implicitly index takes on one of the values in [0, len(vars)).

func NewExactlyKConstraint 

func NewExactlyKConstraint(k int, literals ...Literal) Constraint

NewExactlyKConstraint ensures that exactly k literals are true.

func NewForbiddenAssignmentsConstraint 

func NewForbiddenAssignmentsConstraint(vars []IntVar, assignments [][]int64) Constraint

NewForbiddenAssignmentsConstraint ensures that the values of the n-tuple formed by the given variables is not one of the listed n-tuple assignments.

func NewForbiddenLiteralAssignmentsConstraint 

func NewForbiddenLiteralAssignmentsConstraint(literals []Literal, assignments [][]bool) Constraint

NewForbiddenLiteralAssignmentsConstraint ensures that the values of the n-tuple formed by the given literals is not one of the listed n-tuple assignments.

func NewImplicationConstraint 

func NewImplicationConstraint(a, b Literal) Constraint

NewImplicationConstraint ensures that the first literal implies the second.

func NewLinearConstraint 

func NewLinearConstraint(e LinearExpr, d Domain) Constraint

NewLinearConstraint ensures that the linear expression lies in the given domain. It can be used to express linear equalities of the form: 

0 <= x + 2y <= 10

func NewLinearMaximumConstraint 

func NewLinearMaximumConstraint(target LinearExpr, exprs ...LinearExpr) Constraint

NewLinearMaximumConstraint ensures that the target is equal to the maximum of all linear expressions.

func NewLinearMinimumConstraint 

func NewLinearMinimumConstraint(target LinearExpr, exprs ...LinearExpr) Constraint

NewLinearMinimumConstraint ensures that the target is equal to the minimum of all linear expressions.

func NewMaximumConstraint 

func NewMaximumConstraint(target IntVar, vars ...IntVar) Constraint

NewMaximumConstraint ensures that the target is equal to the maximum of all variables.

func NewMinimumConstraint 

func NewMinimumConstraint(target IntVar, vars ...IntVar) Constraint

NewMinimumConstraint ensures that the target is equal to the minimum of all variables.

func NewModuloConstraint 

func NewModuloConstraint(target, dividend, divisor IntVar) Constraint

NewModuloConstraint ensures that the target to equal to dividend%divisor. The domain of the divisor must be strictly positive.

func NewNonOverlapping2DConstraint 

func NewNonOverlapping2DConstraint(
	xintervals []Interval,
	yintervals []Interval,
	boxesWithNoAreaCanOverlap bool,
) Constraint

NewNonOverlapping2DConstraint ensures that the boxes defined by the following don't overlap: 

[xintervals[i].start, xintervals[i].end)
[yintervals[i].start, yintervals[i].end)

Intervals/boxes of size zero are considered for overlap if the last argument is true.

func NewNonOverlappingConstraint 

func NewNonOverlappingConstraint(intervals ...Interval) Constraint

NewNonOverlappingConstraint ensures that all the intervals are disjoint. More formally, there must exist a sequence such that for every pair of consecutive intervals, we have intervals[i].end <= intervals[i+1].start. Intervals of size zero matter for this constraint. This is also known as a disjunctive constraint in scheduling.

func NewProductConstraint 

func NewProductConstraint(target IntVar, multiplicands ...IntVar) Constraint

NewProductConstraint ensures that the target to equal to the product of all multiplicands. An empty multiplicands list forces the target to be equal to one.

type Domain 

type Domain interface {
	fmt.Stringer
	// contains filtered or unexported methods
}

Domain represents n disjoint intervals, each of the form [min, max]: 

[min_0, max_0,  ..., min_{n-1}, max_{n-1}].

The following constraints hold:

  • For all i < n : min_i <= max_i
  • For all i < n-1 : max_i + 1 < min_{i+1}.

The most common example being just [min, max]. If min == max, then this is a constant variable.

NB: We check at validation that a variable domain is small enough so that we don't run into integer overflow in our algorithms. Avoid having "unbounded" variables like [0, math.MaxInt64], opting instead for tighter domains.

func NewDomain 

func NewDomain(lb, ub int64, ds ...int64) Domain

NewDomain instantiates a new domain using the given intervals.

type IntVar 

type IntVar interface {
	// Stringer provides a printable format representation for the int var.
	fmt.Stringer
	// contains filtered or unexported methods
}

IntVar is an integer variable. It's typically constructed using a domain and is used as part of a model's constraints/objectives. When solving a model, the variable's integer value is decided on.

func AsIntVars 

func AsIntVars(literals []Literal) []IntVar

AsIntVars is a convenience function to convert a slice of Literals to IntVars.

type Interval 

type Interval interface {
	Constraint

	// Parameters returns the variables the interval is comprised of.
	Parameters() (start, end, size IntVar)

	// Stringer provides a printable format representation for the interval.
	fmt.Stringer
	// contains filtered or unexported methods
}

Interval represents an interval parameterized by a start, end, and size. When added to a model, it automatically enforces the following properties: 

start + size == end
size >= 0

It can be used to define interval-based constraints. Constraints differ in how they interpret zero-sized intervals and whether the end is considered exclusive.

type LinearExpr 

type LinearExpr interface {
	// Parameters returns the variables, coefficients, and offset the linear
	// expression is comprised of.
	Parameters() (vars []IntVar, coeffs []int64, offset int64)

	fmt.Stringer
	// contains filtered or unexported methods
}

LinearExpr represents a linear expression of the form: 

5x - 7y + 21z - 42

In the expression above {x, y, z} are variables (IntVars) to be decided on by the model, {5, -7, 21} are coefficients for said variables, and -42 is the offset.

func NewLinearExpr 

func NewLinearExpr(vars []IntVar, coeffs []int64, offset int64) LinearExpr

NewLinearExpr instantiates a new linear expression, representing: 

sum(coefficients[i] * vars[i]) + offset

func Sum 

func Sum(vars ...IntVar) LinearExpr

Sum instantiates a new linear expression representing the sum of the given variables. It's a shorthand for NewLinearExpr with no offset and coefficients equal to one.

type Literal 

type Literal interface {
	IntVar

	// Not returns the negated form of literal. It uses a more efficient encoding
	// than two literals with a model constraint xor-ing them together.
	Not() Literal
	// contains filtered or unexported methods
}

Literal is a boolean variable. It's represented using an IntVar with a fixed domain [0, 1].

type Model 

type Model struct {
	// contains filtered or unexported fields
}

Model is a constraint programming problem. It's not safe for concurrent use.

func NewModel 

func NewModel(name string) *Model

NewModel instantiates a new model.

func (*Model) AddConstraints 

func (m *Model) AddConstraints(cs ...Constraint)

AddConstraints adds constraints to the model. When deciding on a solution, these constraints will need to be satisfied.

func (*Model) Maximize 

func (m *Model) Maximize(e LinearExpr)

Maximize sets a maximization objective for the model.

func (*Model) Minimize 

func (m *Model) Minimize(e LinearExpr)

Minimize sets a minimization objective for the model.

func (*Model) NewConstant 

func (m *Model) NewConstant(c int64, name string) IntVar

NewConstant adds a new constant to the model.

func (*Model) NewIntVar 

func (m *Model) NewIntVar(lb int64, ub int64, name string) IntVar

NewIntVar adds a new integer variable to the model, one that's constrained to the given inclusive upper/lower bound.

func (*Model) NewIntVarFromDomain 

func (m *Model) NewIntVarFromDomain(d Domain, name string) IntVar

NewIntVarFromDomain adds a new integer variable to the model, one that's constrained to the given domain.

func (*Model) NewInterval 

func (m *Model) NewInterval(start, end, size IntVar, name string) Interval

NewInterval adds a new interval to the model, one that's defined using the given start, end and size.

func (*Model) NewLiteral 

func (m *Model) NewLiteral(name string) Literal

NewLiteral adds a new literal to the model.

func (*Model) Solve 

func (m *Model) Solve(os ...Option) Result

Solve attempts to satisfy the model's constraints, if any, by deciding values for all the variables/literals that were instantiated into it. It returns the optimal result if an objective function is declared. If not, it returns the first found result that satisfies the model.

The solve process itself can be configured with various options.

func (*Model) String 

func (m *Model) String() string

String provides a string representation of the model.

func (*Model) Validate 

func (m *Model) Validate() (ok bool, _ error)

Validate checks whether the model is valid. If not, a descriptive error message is returned.

TODO(irfansharif): This validation message refers to things using indexes, which is not really usable.

type Option 

type Option func(o *options, s internal.SolveWrapper)

func WithEnumeration 

func WithEnumeration(f func(Result)) Option

WithEnumeration configures the solver to enumerate over all solutions without objective. This option is incompatible with a parallelism greater than 1.

func WithLogger 

func WithLogger(w io.Writer, prefix string) Option

WithLogger configures the solver to route its internal logging to the given io.Writer, using the given prefix.

func WithParallelism 

func WithParallelism(parallelism int) Option

WithParallelism configures the solver to use the given number of parallel workers during search. If the number provided is <= 1, there will be no parallelism.

func WithTimeout 

func WithTimeout(d time.Duration) Option

WithTimeout configures the solver with a hard time limit.

type Result 

type Result struct {
	// contains filtered or unexported fields
}

Result is what's returned after attempting to solve a model.

func (Result) BooleanValue 

func (r Result) BooleanValue(l Literal) bool

BooleanValue returns the decided value of the given Literal. This is only valid to use if the result is optimal or feasible.

func (Result) Feasible 

func (r Result) Feasible() bool

Feasible is true if a feasible solution has been found, and if we're enumerating through all solutions (if asked). See comment for Optimal for more details.

func (Result) Infeasible 

func (r Result) Infeasible() bool

Infeasible is true iff the problem has been proven infeasible.

func (Result) Invalid 

func (r Result) Invalid() bool

Invalid is true if the model being solved was invalid.

func (Result) ObjectiveValue 

func (r Result) ObjectiveValue() float64

ObjectiveValue is the result of evaluating a model's objective function if the solution found is optimal or feasible. If no solution is found, then for a minimization problem, this will be an upper-bound of the objective of any feasible solution. For a maximization problem, it will be the lower-bound.

func (Result) Optimal 

func (r Result) Optimal() bool

Optimal is true iff a feasible solution has been found.

More generally, this status represents a successful attempt at solving a model (if we've found a solution for a pure feasability problem, or if a gap limit has been specified and we've found solutions within the limit). In the case where we're iterating through all feasible solutions, this status will only be Feasible().

func (Result) String 

func (r Result) String() string

func (Result) Value 

func (r Result) Value(iv IntVar) int64

Value returns the decided value of the given IntVar. This is only valid to use if the result is optimal or feasible.

Source Files

View all Source files

Directories

Path Synopsis
Package internal is where the raw SWIG bindings to the OR-Tools CP-SAT solver live.
 Package internal is where the raw SWIG bindings to the OR-Tools CP-SAT solver live.
pb
testutils
testutils/bazel
testutils/parser
Package parser contains the parsing primitives needed to process the datadriven tests.
 Package parser contains the parsing primitives needed to process the datadriven tests.
testutils/parser/ast
testutils/parser/lexer
testutils/parser/token

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.