[CP-SAT] optimize linear constraint memory; add go code and samples (without any build instructions)

ortools/sat/BUILD.bazel

@@ -1470,6 +1470,7 @@ cc_library(
         "//ortools/util:saturated_arithmetic",
         "//ortools/util:sorted_interval_list",
         "//ortools/util:strong_integers",
+        "@com_google_absl//absl/base:core_headers",
         "@com_google_absl//absl/container:btree",
         "@com_google_absl//absl/container:flat_hash_map",
         "@com_google_absl//absl/container:flat_hash_set",
@@ -1580,6 +1581,7 @@ cc_library(
         "//ortools/lp_data:base",
         "//ortools/util:strong_integers",
         "@com_google_absl//absl/log:check",
+        "@com_google_absl//absl/types:span",
     ],
 )
 

ortools/sat/cuts.cc

@@ -23,6 +23,7 @@
 #include <utility>
 #include <vector>
 
+#include "absl/base/attributes.h"
 #include "absl/container/btree_map.h"
 #include "absl/container/btree_set.h"
 #include "absl/container/flat_hash_map.h"
@@ -279,6 +280,7 @@ void CutDataBuilder::AddOrMergeTerm(const CutTerm& term, IntegerValue t,
 
 // TODO(user): Divide by gcd first to avoid possible overflow in the
 // conversion? it is however unlikely given that our coeffs should be small.
+ABSL_DEPRECATED("Only used in tests, this will be removed.")
 bool CutDataBuilder::ConvertToLinearConstraint(const CutData& cut,
                                                LinearConstraint* output) {
   tmp_map_.clear();
@@ -300,9 +302,10 @@ bool CutDataBuilder::ConvertToLinearConstraint(const CutData& cut,
     }
   }
 
-  output->ClearTerms();
   output->lb = kMinIntegerValue;
   output->ub = new_rhs;
+  output->vars.clear();
+  output->coeffs.clear();
   for (const auto [var, coeff] : tmp_map_) {
     if (coeff == 0) continue;
     output->vars.push_back(var);

ortools/sat/docs/README.md

@@ -8,7 +8,7 @@ https://developers.google.com/optimization/cp/cp_solver
 
 This document presents modeling recipes for the CP-SAT solver.
 
-Code samples are given in C++, Python, Java and C#. Each language has
+Code samples are given in C++, Python, Java, C#, and Go. Each language has
 different requirements for the code samples.
 
 ## Searching for one (optimal) solution of a CP-SAT model
@@ -207,3 +207,64 @@ public class SimpleSatProgram
     }
 }
 ```
+
+### Go code samples
+
+The interface to the CP-SAT solver is implemented through the **CpModelBuilder**
+described in the package **cpmodel** in
+*ortools/sat/go/cp_model.go*. This class is a helper to fill in
+the cp_model protobuf.
+
+Also within the **cpmodel** package is
+*ortools/sat/go/cp_model.go* which provides functions to solve
+the model along with helpers to access the solution found by the solver.
+
+```cs
+// The simple_sat_program command is an example of a simple sat program.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+func simpleSatProgram() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	switch response.GetStatus() {
+	case cmpb.CpSolverStatus_OPTIMAL, cmpb.CpSolverStatus_FEASIBLE:
+		fmt.Printf("x = %d\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf("y = %d\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf("z = %d\n", cpmodel.SolutionIntegerValue(response, z))
+	default:
+		fmt.Println("No solution found.")
+	}
+
+	return nil
+}
+
+func main() {
+	if err := simpleSatProgram(); err != nil {
+		log.Exitf("simpleSatProgram returned with error: %v", err)
+	}
+}
+```

ortools/sat/docs/boolean_logic.md

@@ -106,6 +106,31 @@ public class LiteralSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The literal_sample_sat command is a simple example of literals.
+package main
+
+import (
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+func literalSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar().WithName("x")
+	notX := x.Not()
+
+	log.Infof("x = %d, x.Not() = %d", x.Index(), notX.Index())
+}
+
+func main() {
+	literalSampleSat()
+}
+```
+
 ## Boolean constraints
 
 For Boolean variables x and y, the following are elementary Boolean constraints:
@@ -216,6 +241,30 @@ public class BoolOrSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The bool_or_sample_sat command is simple example of the BoolOr constraint.
+package main
+
+import (
+	"ortools/sat/go/cpmodel"
+)
+
+func boolOrSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar()
+	y := model.NewBoolVar()
+
+	model.AddBoolOr(x, y.Not())
+}
+
+func main() {
+	boolOrSampleSat()
+}
+```
+
 ## Reified constraints
 
 The CP-SAT solver supports *half-reified* constraints, also called
@@ -378,6 +427,40 @@ public class ReifiedSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The reified_sample_sat command is a simple example of implication constraints.
+package main
+
+import (
+	"ortools/sat/go/cpmodel"
+)
+
+func reifiedSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar()
+	y := model.NewBoolVar()
+	b := model.NewBoolVar()
+
+	// First version using a half-reified bool and.
+	model.AddBoolAnd(x, y.Not()).OnlyEnforceIf(b)
+
+	// Second version using implications.
+	model.AddImplication(b, x)
+	model.AddImplication(b, y.Not())
+
+	// Third version using bool or.
+	model.AddBoolOr(b.Not(), x)
+	model.AddBoolOr(b.Not(), y.Not())
+}
+
+func main() {
+	reifiedSampleSat()
+}
+```
+
 ## Product of two Boolean Variables
 
 A useful construct is the product `p` of two Boolean variables `x` and `y`.
@@ -432,3 +515,68 @@ def boolean_product_sample_sat():
 
 boolean_product_sample_sat()
 ```
+
+### Go code
+
+```cs
+// The boolean_product_sample_sat command is a simple example of the product of two literals.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func booleanProductSample() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar().WithName("x")
+	y := model.NewBoolVar().WithName("y")
+	p := model.NewBoolVar().WithName("p")
+
+	// x and y implies p, rewrite as not(x and y) or p.
+	model.AddBoolOr(x.Not(), y.Not(), p)
+
+	// p implies x and y, expanded into two implications.
+	model.AddImplication(p, x)
+	model.AddImplication(p, y)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	// Set `fill_additional_solutions_in_response` and `enumerate_all_solutions` to true so
+	// the solver returns all solutions found.
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(4),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		fmt.Printf("x: %v", additionalSolution.GetValues()[x.Index()])
+		fmt.Printf(" y: %v", additionalSolution.GetValues()[y.Index()])
+		fmt.Printf(" p: %v\n", additionalSolution.GetValues()[p.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	err := booleanProductSample()
+	if err != nil {
+		log.Exitf("booleanProductSample returned with error: %v", err)
+	}
+}
+```

ortools/sat/docs/channeling.md

@@ -296,6 +296,79 @@ public class ChannelingSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The channeling_sample_sat command is a simple example of a channeling constraint.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func channelingSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our two primary variables.
+	x := model.NewIntVar(0, 10)
+	y := model.NewIntVar(0, 10)
+
+	// Declare our intermediate Boolean variable.
+	b := model.NewBoolVar()
+
+	// Implement b == (x > 5).
+	model.AddGreaterOrEqual(x, cpmodel.NewConstant(5)).OnlyEnforceIf(b)
+	model.AddLessThan(x, model.NewConstant(5)).OnlyEnforceIf(b.Not())
+
+	// Create our two half-reified constraints.
+	// First, b implies (y == 10 - x).
+	model.AddEquality(cpmodel.NewLinearExpr().Add(x).Add(y), cpmodel.NewConstant(10)).OnlyEnforceIf(b)
+	// Second, b.Not() implies (y == 0).
+	model.AddEquality(y, cpmodel.NewConstant(0)).OnlyEnforceIf(b.Not())
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(11),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x: %v y: %v b: %v\n", vs[x.Index()], vs[y.Index()], vs[b.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := channelingSampleSat(); err != nil {
+		log.Exitf("channelingSampleSat returned with error: %v", err)
+	}
+}
+```
+
 This displays the following:
 
 ```
@@ -701,3 +774,116 @@ public class BinPackingProblemSat
     }
 }
 ```
+
+### Go code
+
+```cs
+// The binpacking_problem_sat command is an example of a bin packing problem that uses channeling
+// constraints.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const (
+	binCapacity   = 100
+	slackCapacity = 20
+	safeCapacity  = binCapacity - slackCapacity
+	numBins       = 5
+)
+
+type item struct {
+	Cost, Copies int64_t
+}
+
+func binpackingProblemSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	items := []item{{20, 6}, {15, 6}, {30, 4}, {45, 3}}
+	numItems := len(items)
+
+	// Main variables.
+	x := make([][]cpmodel.IntVar, numItems)
+	for i, item := range items {
+		x[i] = make([]cpmodel.IntVar, numBins)
+		for b := 0; b < numBins; b++ {
+			x[i][b] = model.NewIntVar(0, item.Copies)
+		}
+	}
+
+	// Load variables.
+	load := make([]cpmodel.IntVar, numBins)
+	for b := 0; b < numBins; b++ {
+		load[b] = model.NewIntVar(0, binCapacity)
+	}
+
+	// Slack variables.
+	slacks := make([]cpmodel.BoolVar, numBins)
+	for b := 0; b < numBins; b++ {
+		slacks[b] = model.NewBoolVar()
+	}
+
+	// Links load and x.
+	for b := 0; b < numBins; b++ {
+		expr := cpmodel.NewLinearExpr()
+		for i := 0; i < numItems; i++ {
+			expr.AddTerm(x[i][b], items[i].Cost)
+		}
+		model.AddEquality(expr, load[b])
+	}
+
+	// Place all items.
+	for i := 0; i < numItems; i++ {
+		copies := cpmodel.NewLinearExpr()
+		for _, b := range x[i] {
+			copies.Add(b)
+		}
+		model.AddEquality(copies, cpmodel.NewConstant(items[i].Copies))
+	}
+
+	// Links load and slack through an equivalence relation.
+	for b := 0; b < numBins; b++ {
+		// slacks[b] => load[b] <= safeCapacity.
+		model.AddLessOrEqual(load[b], cpmodel.NewConstant(safeCapacity)).OnlyEnforceIf(slacks[b])
+		// slacks[b].Not() => load[b] > safeCapacity.
+		model.AddGreaterThan(load[b], cpmodel.NewConstant(safeCapacity)).OnlyEnforceIf(slacks[b].Not())
+	}
+
+	// Maximize sum of slacks.
+	obj := cpmodel.NewLinearExpr()
+	for _, s := range slacks {
+		obj.Add(s)
+	}
+	model.Maximize(obj)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Println("Status: ", response.GetStatus())
+	fmt.Println("Objective: ", response.GetObjectiveValue())
+	fmt.Println("Statistics: ")
+	fmt.Println("  - conflicts : ", response.GetNumConflicts())
+	fmt.Println("  - branches  : ", response.GetNumBranches())
+	fmt.Println("  - wall time : ", response.GetWallTime())
+
+	return nil
+}
+
+func main() {
+	if err := binpackingProblemSat(); err != nil {
+		log.Exitf("binpackingProblemSat returned with error: %v", err)
+	}
+}
+```

ortools/sat/docs/integer_arithmetic.md

@@ -37,6 +37,7 @@ non-contiguous domains. Here, the variable can be any of 1, 3, 4, or 6:
     6}), "x");`
 -   **C#**: `model.NewIntVarFromDomain(Domain.FromValues(new long[] {1, 3, 4,
     6}), "x");`
+-   **Go**: `model.NewIntVarFromDomain(cpmodel.FromValues([]int64_t{1, 3, 4, 6})`
 
 Variables can also be created using a list of intervals. Below, the variable
 created is constrained to be 1, 2, 4, 5, or 6:
@@ -48,6 +49,8 @@ created is constrained to be 1, 2, 4, 5, or 6:
     2}, {4, 6}}), "x");`
 -   **C#**: `model.NewIntVarFromDomain(Domain.FromIntervals(new long[][] { new
     long[] {1, 2}, new long[] {4, 6} }), "x");`
+-   **Go**: `model.NewIntVarFromDomain(cpmodel.FromIntervals(
+    []cpmodel.ClosedInterval{{1, 2}, {4, 6}}))`
 
 ### Boolean variables
 
@@ -59,6 +62,7 @@ type is not uniform across languages.
 -   **Python**: `x = model.NewBoolVar('x')`
 -   **Java**: `Literal x = model.newBoolVar("x");`
 -   **C#**: `ILiteral x = model.NewBoolVar("x");`
+-   **Go**: `x := model.NewBoolVar().WithName("x")`
 
 ### Other methods
 
@@ -71,16 +75,17 @@ To create a variable with a single value domain, use the `NewConstant()` API (or
 
 ## Linear constraints
 
-### C++ and Java linear constraints and linear expressions
+### C++, Java, and Go linear constraints and linear expressions
 
-**C++** and **Java** APIs do not use arithmetic operators (+, \*, -, <=...).
-Linear constraints are created using a method of the model factory, such as
-`cp_model.AddEquality(x, 3)` in C++, or `cp_model.addGreaterOrEqual(x, 10)` in
-Java.
+**C++**, **Java**, and **Go** APIs do not use arithmetic operators (+, \*, -,
+<=...). Linear constraints are created using a method of the model factory, such
+as `cp_model.AddEquality(x, 3)` in C++, `cp_model.addGreaterOrEqual(x, 10)` in
+Java, or `model.AddLessThan(x, cpmodel.NewConstant(5))` in Go.
 
 Furthermore, helper methods can be used to create sums and scalar products like
-`LinearExpr::Sum({x, y, z})` in C++, and `LinearExpr.weightedSum(new IntVar[]
-{x, y, z}, new long[] {1, 2, 3})` in Java.
+`LinearExpr::Sum({x, y, z})` in C++, `LinearExpr.weightedSum(new IntVar[] {x, y,
+z}, new long[] {1, 2, 3})` in Java, and `cpmodel.NewLinearExpr().AddSum(x, y,
+z)` in Go.
 
 ### Python and C\# linear constraints and linear expressions
 
@@ -260,6 +265,61 @@ public class RabbitsAndPheasantsSat
 }
 ```
 
+### Go code
+
+```cs
+// The rabbits_and_pheasants_sat command is an example of a simple sat program that
+// solves the rabbits and pheasants problem.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const numAnimals = 20
+
+func rabbitsAndPheasants() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	allAnimals := cpmodel.NewDomain(0, numAnimals)
+	rabbits := model.NewIntVarFromDomain(allAnimals).WithName("rabbits")
+	pheasants := model.NewIntVarFromDomain(allAnimals).WithName("pheasants")
+
+	model.AddEquality(cpmodel.NewLinearExpr().AddSum(rabbits, pheasants), cpmodel.NewConstant(numAnimals))
+	model.AddEquality(cpmodel.NewLinearExpr().AddTerm(rabbits, 4).AddTerm(pheasants, 2), cpmodel.NewConstant(56))
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	switch response.GetStatus() {
+	case cmpb.CpSolverStatus_OPTIMAL, cmpb.CpSolverStatus_FEASIBLE:
+		fmt.Printf("There are %d rabbits and %d pheasants.\n",
+			cpmodel.SolutionIntegerValue(response, rabbits),
+			cpmodel.SolutionIntegerValue(response, pheasants))
+	default:
+		fmt.Println("No solution found.")
+	}
+
+	return nil
+}
+
+func main() {
+	if err := rabbitsAndPheasants(); err != nil {
+		log.Exitf("rabbitsAndPheasants returned with error: %v", err)
+	}
+}
+```
+
 ## Earliness-Tardiness cost function.
 
 Let's encode a useful convex piecewise linear function that often appears in
@@ -604,6 +664,88 @@ public class EarlinessTardinessCostSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The earliness_tardiness_cost_sample_sat command is an example of an implementation of a convex
+// piecewise linear function.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+const (
+	earlinessDate = 5
+	earlinessCost = 8
+	latenessDate  = 15
+	latenessCost  = 12
+	largeConstant = 1000
+)
+
+func earlinessTardinessCostSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our primary variable.
+	x := model.NewIntVar(0, 20)
+
+	// Create the expression variable and implement the piecewise linear function.
+	//
+	//  \        /
+	//   \______/
+	//   ed    ld
+	//
+	expr := model.NewIntVar(0, largeConstant)
+
+	// Link together expr and x through the 3 segments.
+	firstSegment := cpmodel.NewConstant(earlinessDate*earlinessCost).AddTerm(x, -earlinessCost)
+	secondSegment := cpmodel.NewConstant(0)
+	thirdSegment := cpmodel.NewConstant(-latenessDate*latenessCost).AddTerm(x, latenessCost)
+	model.AddMaxEquality(expr, firstSegment, secondSegment, thirdSegment)
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(21),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x= %v expr= %v\n", vs[x.Index()], vs[expr.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := earlinessTardinessCostSampleSat(); err != nil {
+		log.Exitf("earlinessTardinessCostSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Step function.
 
 Let's encode a step function. We will use one Boolean variable per step value,
@@ -977,3 +1119,94 @@ public class StepFunctionSampleSat
     }
 }
 ```
+
+### Go code
+
+```cs
+// The step_function_sample_sat command is an example of an implementation of a step function.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func stepFunctionSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our primary variable.
+	x := model.NewIntVar(0, 20)
+
+	// Create the expression variable and implement the step function
+	// Note it is not defined for var == 2.
+	//
+	//        -               3
+	// -- --      ---------   2
+	//                        1
+	//      -- ---            0
+	//           1         2
+	// 012345678901234567890
+	//
+	expr := model.NewIntVar(0, 3)
+
+	// expr == 0 on [5, 6] U [8, 10]
+	b0 := model.NewBoolVar()
+	d0 := cpmodel.FromValues([]int64_t{5, 6, 8, 9, 10})
+	model.AddLinearConstraintForDomain(x, d0).OnlyEnforceIf(b0)
+	model.AddEquality(expr, cpmodel.NewConstant(0)).OnlyEnforceIf(b0)
+
+	// expr == 2 on [0, 1] U [3, 4] U [11, 20]
+	b2 := model.NewBoolVar()
+	d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{0, 1}, {3, 4}, {11, 20}})
+	model.AddLinearConstraintForDomain(x, d2).OnlyEnforceIf(b2)
+	model.AddEquality(expr, cpmodel.NewConstant(2)).OnlyEnforceIf(b2)
+
+	// expr = 3 when x = 7
+	b3 := model.NewBoolVar()
+	model.AddEquality(x, cpmodel.NewConstant(7)).OnlyEnforceIf(b3)
+	model.AddEquality(expr, cpmodel.NewConstant(3)).OnlyEnforceIf(b3)
+
+	// At least one Boolean variable is true.
+	model.AddBoolOr(b0, b2, b3)
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(21),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x= %v expr= %v\n", vs[x.Index()], vs[expr.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := stepFunctionSampleSat(); err != nil {
+		log.Exitf("stepFunctionSampleSat returned with error: %v", err)
+	}
+}
+```

ortools/sat/docs/model.md

@@ -25,6 +25,7 @@ model list of variables:
 -   **Python**: `var.Index()`
 -   **Java**: `var.getIndex()`
 -   **C#**: `var.Index` or `var.GetIndex()`
+-   **Go**: `var.Index()`
 
 The implementation of Boolean literals differs across languages.
 
@@ -44,6 +45,10 @@ The implementation of Boolean literals differs across languages.
 -   **C#**: Boolean variables are defined as an `IntVar` with a Boolean domain
     (0 or 1). Boolean variables and their negations implement the `ILiteral`
     interface. This interface defines `GetIndex()` and `Not()` methods.
+-   **Go**: The `BoolVar` class is a separate class from the `IntVar` class. A
+    `BoolVar` object has two important methods: `Not()` and `Index()`. `Not()`
+    returned another `BoolVar` with a different index: `b.Not.Index() =
+    -b.Index() - 1`
 
 ## Solution hinting
 
@@ -295,6 +300,63 @@ public class SolutionHintingSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The solution_hinting_sample_sat command is an example of setting solution hints on the model.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+func solutionHintingSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64_t{1, 2, 3}))
+
+	// Solution hinting: x <- 1, y <- 2
+	hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64_t{x: 7}}
+	model.SetHint(hint)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Printf(" x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf(" y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf(" z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := solutionHintingSampleSat(); err != nil {
+		log.Exitf("solutionHintingSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Model copy
 
 The CpModel classes supports deep copy from a previous model. This is useful to

ortools/sat/docs/scheduling.md

@@ -186,6 +186,56 @@ public class IntervalSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The interval_sample_sat_go command is a simple example of the Interval variable.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 100
+
+func intervalSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVar(2, 4).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	// An interval can be created from three affine expressions.
+	intervalVar := model.NewIntervalVar(x, y, cpmodel.NewConstant(2).Add(z)).WithName("interval")
+
+	// If the size is fixed, a simpler version uses the start expression and the size.
+	fixedSizeIntervalVar := model.NewFixedSizeIntervalVar(x, 10).WithName("fixedSizeInterval")
+
+	// A fixed interval can be created using the same API.
+	fixedIntervalVar := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(5), 10).WithName("fixedInterval")
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	fmt.Printf("%v\n", m.GetConstraints()[intervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedSizeIntervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedIntervalVar.Index()])
+
+	return nil
+}
+
+func main() {
+	if err := intervalSampleSat(); err != nil {
+		log.Exitf("intervalSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Optional intervals
 
 An interval can be marked as optional. The presence of this interval is
@@ -361,6 +411,54 @@ public class OptionalIntervalSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The optional_interval_sample_sat command is an example of an Interval variable that is
+// marked as optional.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 100
+
+func optionalIntervalSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVar(2, 4).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+	presenceVar := model.NewBoolVar().WithName("presence")
+
+	// An optional interval can be created from three affine expressions and a BoolVar.
+	intervalVar := model.NewOptionalIntervalVar(x, y, cpmodel.NewConstant(2).Add(z), presenceVar).WithName("interval")
+
+	// If the size is fixed, a simpler version uses the start expression and the size.
+	fixedSizeIntervalVar := model.NewOptionalFixedSizeIntervalVar(x, 10, presenceVar).WithName("fixedSizeInterval")
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	fmt.Printf("%v\n", m.GetConstraints()[intervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedSizeIntervalVar.Index()])
+
+	return nil
+}
+
+func main() {
+	if err := optionalIntervalSampleSat(); err != nil {
+		log.Exitf("optionalIntervalSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## NoOverlap constraint
 
 A no_overlap constraint simply states that all intervals are disjoint. It is
@@ -646,6 +744,88 @@ public class NoOverlapSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The no_overlap_sample_sat command is an example of the NoOverlap constraints.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 21 // 3 weeks
+
+func noOverlapSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	// Task 0, duration 2.
+	start0 := model.NewIntVarFromDomain(domain)
+	duration0 := cpmodel.NewConstant(2)
+	end0 := model.NewIntVarFromDomain(domain)
+	task0 := model.NewIntervalVar(start0, duration0, end0)
+
+	// Task 1, duration 4.
+	start1 := model.NewIntVarFromDomain(domain)
+	duration1 := cpmodel.NewConstant(4)
+	end1 := model.NewIntVarFromDomain(domain)
+	task1 := model.NewIntervalVar(start1, duration1, end1)
+
+	// Task 2, duration 3
+	start2 := model.NewIntVarFromDomain(domain)
+	duration2 := cpmodel.NewConstant(2)
+	end2 := model.NewIntVarFromDomain(domain)
+	task2 := model.NewIntervalVar(start2, duration2, end2)
+
+	// Weekends.
+	weekend0 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(5), 2)
+	weekend1 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(12), 2)
+	weekend2 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(19), 2)
+
+	// No Overlap constraint.
+	model.AddNoOverlap(task0, task1, task2, weekend0, weekend1, weekend2)
+
+	// Makespan.
+	makespan := model.NewIntVarFromDomain(domain)
+	model.AddLessOrEqual(end0, makespan)
+	model.AddLessOrEqual(end1, makespan)
+	model.AddLessOrEqual(end2, makespan)
+
+	model.Minimize(makespan)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Println(response.GetStatus())
+		fmt.Println("Optimal Schedule Length: ", response.GetObjectiveValue())
+		fmt.Println("Task 0 starts at ", cpmodel.SolutionIntegerValue(response, start0))
+		fmt.Println("Task 1 starts at ", cpmodel.SolutionIntegerValue(response, start1))
+		fmt.Println("Task 2 starts at ", cpmodel.SolutionIntegerValue(response, start2))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := noOverlapSampleSat(); err != nil {
+		log.Exitf("noOverlapSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Cumulative constraint with varying capacity profile.
 
 A cumulative constraint takes a list of intervals, and a list of demands, and a
@@ -1458,6 +1638,163 @@ public class RankingSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The ranking_sample_sat command is an example of ranking intervals in a NoOverlap constraint.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const (
+	horizonLength = 100
+	numTasks      = 4
+)
+
+// rankTasks adds constraints and variables to link tasks and ranks. This method
+// assumes that all starts are disjoint, meaning that all tasks have a strictly
+// positive duration, and they appear in the same NoOverlap constraint.
+func rankTasks(starts []cpmodel.IntVar, presences []cpmodel.BoolVar, ranks []cpmodel.IntVar, model *cpmodel.Builder) {
+	// Creates precedence variables between pairs of intervals.
+	precedences := make([][]cpmodel.BoolVar, numTasks)
+	for i := 0; i < numTasks; i++ {
+		precedences[i] = make([]cpmodel.BoolVar, numTasks)
+		for j := 0; j < numTasks; j++ {
+			if i == j {
+				precedences[i][i] = presences[i]
+			} else {
+				prec := model.NewBoolVar()
+				precedences[i][j] = prec
+				model.AddLessOrEqual(starts[i], starts[j]).OnlyEnforceIf(prec)
+			}
+		}
+	}
+
+	// Treats optional intervals.
+	for i := 0; i+1 < numTasks; i++ {
+		for j := i + 1; j < numTasks; j++ {
+			// Make sure that if task i is not performed, all precedences are false.
+			model.AddImplication(presences[i].Not(), precedences[i][j].Not())
+			model.AddImplication(presences[i].Not(), precedences[j][i].Not())
+			// Make sure that if task j is not performed, all precedences are false.
+			model.AddImplication(presences[j].Not(), precedences[i][j].Not())
+			model.AddImplication(presences[j].Not(), precedences[j][i].Not())
+			// The following BoolOr will enforce that for any two intervals:
+			// 		i precedes j or j precedes i or at least one interval is not performed.
+			model.AddBoolOr(precedences[i][j], precedences[j][i], presences[i].Not(), presences[j].Not())
+			// Redundant constraint: it propagates early that at most one precedence
+			// is true.
+			model.AddImplication(precedences[i][j], precedences[j][i].Not())
+			model.AddImplication(precedences[j][i], precedences[i][j].Not())
+		}
+	}
+
+	// Links precedences and ranks.
+	for i := 0; i < numTasks; i++ {
+		sumOfPredecessors := cpmodel.NewConstant(-1)
+		for j := 0; j < numTasks; j++ {
+			sumOfPredecessors.Add(precedences[j][i])
+		}
+		model.AddEquality(ranks[i], sumOfPredecessors)
+	}
+}
+
+func rankingSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	starts := make([]cpmodel.IntVar, numTasks)
+	ends := make([]cpmodel.IntVar, numTasks)
+	intervals := make([]cpmodel.IntervalVar, numTasks)
+	presences := make([]cpmodel.BoolVar, numTasks)
+	ranks := make([]cpmodel.IntVar, numTasks)
+
+	horizon := cpmodel.NewDomain(0, horizonLength)
+	possibleRanks := cpmodel.NewDomain(-1, numTasks-1)
+
+	for t := 0; t < numTasks; t++ {
+		start := model.NewIntVarFromDomain(horizon)
+		duration := cpmodel.NewConstant(int64_t(t + 1))
+		end := model.NewIntVarFromDomain(horizon)
+		var presence cpmodel.BoolVar
+		if t < numTasks/2 {
+			presence = model.TrueVar()
+		} else {
+			presence = model.NewBoolVar()
+		}
+		interval := model.NewOptionalIntervalVar(start, duration, end, presence)
+		rank := model.NewIntVarFromDomain(possibleRanks)
+
+		starts[t] = start
+		ends[t] = end
+		intervals[t] = interval
+		presences[t] = presence
+		ranks[t] = rank
+	}
+
+	// Adds NoOverlap constraint.
+	model.AddNoOverlap(intervals...)
+
+	// Ranks tasks.
+	rankTasks(starts, presences, ranks, model)
+
+	// Adds a constraint on ranks.
+	model.AddLessThan(ranks[0], ranks[1])
+
+	// Creates makespan variables.
+	makespan := model.NewIntVarFromDomain(horizon)
+	for t := 0; t < numTasks; t++ {
+		model.AddLessOrEqual(ends[t], makespan).OnlyEnforceIf(presences[t])
+	}
+
+	// Create objective: minimize 2 * makespan - 7 * sum of presences.
+	// This is you gain 7 by interval performed, but you pay 2 by day of delays.
+	objective := cpmodel.NewLinearExpr().AddTerm(makespan, 2)
+	for t := 0; t < numTasks; t++ {
+		objective.AddTerm(presences[t], -7)
+	}
+	model.Minimize(objective)
+
+	// Solving part.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Println(response.GetStatus())
+		fmt.Println("Optimal cost: ", response.GetObjectiveValue())
+		fmt.Println("Makespan: ", cpmodel.SolutionIntegerValue(response, makespan))
+		for t := 0; t < numTasks; t++ {
+			rank := cpmodel.SolutionIntegerValue(response, ranks[t])
+			if cpmodel.SolutionBooleanValue(response, presences[t]) {
+				start := cpmodel.SolutionIntegerValue(response, starts[t])
+				fmt.Printf("Task %v starts at %v with rank %v\n", t, start, rank)
+			} else {
+				fmt.Printf("Task %v is not performed and ranked at %v\n", t, rank)
+			}
+		}
+	}
+
+	return nil
+}
+
+func main() {
+	if err := rankingSampleSat(); err != nil {
+		log.Exitf("rankingSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Ranking tasks in a disjunctive resource with a circuit constraint.
 
 To rank intervals in a no_overlap constraint, we will use a circuit constraint

ortools/sat/docs/solver.md

@@ -185,6 +185,66 @@ public class SolveWithTimeLimitSampleSat
 }
 ```
 
+### Specifying the time limit in Go
+
+```cs
+// The solve_with_time_limit_sample_sat command is an example of setting a time limit on the model.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func solveWithTimeLimitSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+
+	// Sets a time limit of 10 seconds.
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(10.0),
+	}.Build()
+
+	// Solve.
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Printf(" x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf(" y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf(" z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := solveWithTimeLimitSampleSat(); err != nil {
+		log.Exitf("solveWithTimeLimitSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Printing intermediate solutions
 
 In an optimization model, you can print intermediate solutions. For all
@@ -435,6 +495,68 @@ public class SolveAndPrintIntermediateSolutionsSampleSat
 }
 ```
 
+### Go code
+
+```cs
+// The solve_and_print_intermediate_solutions_sample_sat command
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func solveAndPrintIntermediateSolutionsSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	model.Maximize(cpmodel.NewLinearExpr().Add(x).AddTerm(y, 2).AddTerm(z, 3))
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+
+	// Currently, the CpModelBuilder does not allow for callbacks, so intermediate solutions
+	// cannot be printed while solving. However, the CP-SAT solver does allow for returning
+	// the intermediate solutions found while solving in the response.
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(10),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Println("Number of intermediate solutions found: ", len(response.GetAdditionalSolutions()))
+
+	fmt.Println("Optimal solution:")
+	fmt.Printf("  x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+	fmt.Printf("  y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+	fmt.Printf("  z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+
+	return nil
+}
+
+func main() {
+	if err := solveAndPrintIntermediateSolutionsSampleSat(); err != nil {
+		log.Exitf("solveAndPrintIntermediateSolutionsSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Searching for all solutions in a satisfiability model
 
 In an non-optimization model, you can search for all solutions. For all
@@ -706,6 +828,68 @@ public class SearchForAllSolutionsSampleSat
 }
 ```
 
+### Go code
+
+To search for all solutions, a parameter of the SAT solver must be changed.
+
+```cs
+// The search_for_all_solutions_sample_sat command is an example for how to search for
+// all solutions.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func searchForAllSolutionsSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	// Currently, the CpModelBuilder does not allow for callbacks, so each feasible solution cannot
+	// be printed while solving. However, the CP Solver can return all of the enumerated solutions
+	// in the response by setting the following parameters.
+	params := sppb.SatParameters_builder{
+		EnumerateAllSolutions:             proto.Bool(true),
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(27),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	for i, solution := range response.GetAdditionalSolutions() {
+		vs := solution.GetValues()
+		fmt.Printf("Solution %v: x = %v, y = %v, z = %v\n", i, vs[x.Index()], vs[y.Index()], vs[z.Index()])
+	}
+
+	fmt.Println("Number of solutions found: ", len(response.GetAdditionalSolutions()))
+
+	return nil
+}
+
+func main() {
+	if err := searchForAllSolutionsSampleSat(); err != nil {
+		log.Exitf("searchForAllSolutionsSampleSat returned with error: %v", err)
+	}
+}
+```
+
 ## Stopping search early
 
 Sometimes, you might decide that the current solution is good enough. In this

ortools/sat/go/cp_solver.go

@@ -0,0 +1,184 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package cpmodel
+
+import (
+	"fmt"
+	"sync"
+	"unsafe"
+
+	"golang/protobuf/v2/proto/proto"
+
+	cmpb "ortools/sat/cp_model_go_proto"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+/*
+#include <stdlib.h> // for free
+#include <stdint.h>
+#include "ortools/sat/go/cp_solver_c.h"
+*/
+import "C"
+
+// SolveCpModel solves a CP Model with the given input proto and returns a CPSolverResponse.
+func SolveCpModel(input *cmpb.CpModelProto) (*cmpb.CpSolverResponse, error) {
+	return SolveCpModelWithParameters(input, nil)
+}
+
+// SolveCpModelWithParameters solves a CP Model with the given input proto and solver
+// parameters and returns a CPSolverResponse.
+func SolveCpModelWithParameters(input *cmpb.CpModelProto, params *sppb.SatParameters) (*cmpb.CpSolverResponse, error) {
+	// Transform `input` into bytes.
+	bReq, err := proto.Marshal(input)
+	if err != nil {
+		return nil, fmt.Errorf("marshaling `input` failed: %w", err)
+	}
+	cReq := C.CBytes(bReq)
+	defer C.free(cReq)
+
+	// Transform `params` into bytes.
+	bParams, err := proto.Marshal(params)
+	if err != nil {
+		return nil, fmt.Errorf("marshaling `params` failed: %w", err)
+	}
+	cParams := C.CBytes(bParams)
+	defer C.free(cParams)
+
+	var cRes unsafe.Pointer
+	var cResLen C.int
+	C.SolveCpModelWithParameters(cReq, C.int(len(bReq)), cParams, C.int(len(bParams)), &cRes, &cResLen)
+	defer C.free(cRes)
+
+	// Transform `cRes` into the Go response proto.
+	bRes := C.GoBytes(cRes, cResLen)
+	res := &cmpb.CpSolverResponse{}
+	if err = proto.Unmarshal(bRes, res); err != nil {
+		return nil, fmt.Errorf("unmarshaling `bRes` failed: %w", err)
+	}
+
+	return res, nil
+}
+
+// SolveCpModelInterruptibleWithParameters solves a CP Model with the given input proto
+// and parameters and returns a CPSolverResponse. The solve can be interrupted by triggering
+// the `interrupt`.
+func SolveCpModelInterruptibleWithParameters(input *cmpb.CpModelProto, params *sppb.SatParameters, interrupt <-chan struct{}) (*cmpb.CpSolverResponse, error) {
+	// Create the atomic bool for interrupting solves.
+	limitReached := newAtomicBoolWrapper()
+	defer limitReached.delete()
+
+	// Transform `input` into bytes.
+	bReq, err := proto.Marshal(input)
+	if err != nil {
+		return nil, err
+	}
+	cReq := C.CBytes(bReq)
+	defer C.free(cReq)
+
+	// Transform `params` input bytes.
+	bParams, err := proto.Marshal(params)
+	if err != nil {
+		return nil, err
+	}
+	cParams := C.CBytes(bParams)
+	defer C.free(cParams)
+
+	solveDone := make(chan struct{})
+	defer close(solveDone)
+	// Wait for either to solve to finish or the solve to be interrupted.
+	go func() {
+		select {
+		case <-interrupt:
+			limitReached.trigger()
+		case <-solveDone:
+		}
+	}()
+
+	// We want to make sure we trigger the atomic Bool before we call the solver
+	// if the input `interrupt` is already closed. We can't trust the
+	// scheduler to execute the previous goroutine immediately, even calling
+	// `runtime.Gosched()` (the unit test failed 3 out of 1000 times when doing
+	// so).
+	select {
+	case <-interrupt:
+		limitReached.trigger()
+	default:
+	}
+
+	var cRes unsafe.Pointer
+	var cResLen C.int
+	C.SolveCpInterruptible(limitReached.ptr, cReq, C.int(len(bReq)), cParams, C.int(len(bParams)), &cRes, &cResLen)
+	defer C.free(cRes)
+
+	// Transform `cRes` into the Go response proto.
+	bRes := C.GoBytes(cRes, cResLen)
+	result := &cmpb.CpSolverResponse{}
+	if err = proto.Unmarshal(bRes, result); err != nil {
+		return nil, fmt.Errorf("unmarshaling `bRes` failed: %w", err)
+	}
+
+	return result, nil
+}
+
+// atomicBoolWrapper keeps a pointer on a C++ AtomicBool instance.
+type atomicBoolWrapper struct {
+	mutex sync.Mutex
+	ptr   unsafe.Pointer // Guarded by mutex.
+}
+
+// newAtomicBoolWrapper returns a new instance of a C++ AtomicBool.
+//
+// The returned object must be destroyed with delete() for the C++ object not to
+// leak.
+//
+// This object is thread-safe: delete() and trigger() can be called
+// concurrently.
+func newAtomicBoolWrapper() *atomicBoolWrapper {
+	return &atomicBoolWrapper{
+		ptr: C.SolveCpNewAtomicBool(),
+	}
+}
+
+// trigger triggers the C++ SolveCpStopSolve method with the atomic bool.
+//
+// If the atomic bool has been deleted this has no effect.
+func (intr *atomicBoolWrapper) trigger() {
+	intr.mutex.Lock()
+	defer intr.mutex.Unlock()
+	if uintptr(intr.ptr) != 0 {
+		C.SolveCpStopSolve(intr.ptr)
+	}
+}
+
+// delete deletes the underlying C++ object.
+//
+// Calling it multiple times has not effect.
+func (intr *atomicBoolWrapper) delete() {
+	intr.mutex.Lock()
+	defer intr.mutex.Unlock()
+	// We don't test that intr.ptr is not nullptr here since C++ `delete` can be
+	// called with nullptr.
+	C.SolveCpDestroyAtomicBool(intr.ptr)
+	intr.ptr = unsafe.Pointer(uintptr(0))
+}
+
+// SolutionBooleanValue returns the value of BoolVar `bv` in the response.
+func SolutionBooleanValue(r *cmpb.CpSolverResponse, bv BoolVar) bool {
+	return bv.evaluateSolutionValue(r) != 0
+}
+
+// SolutionIntegerValue returns the value of LinearArgument `la` in the response.
+func SolutionIntegerValue(r *cmpb.CpSolverResponse, la LinearArgument) int64_t {
+	return la.evaluateSolutionValue(r)
+}

ortools/sat/go/cp_solver_c.cc

@@ -0,0 +1,84 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#include "ortools/sat/go/cp_solver_c.h"
+
+#include <atomic>
+#include <string>
+
+#include "absl/status/status.h"
+#include "ortools/base/logging.h"
+#include "ortools/base/status.pb.h"
+#include "ortools/sat/cp_model.pb.h"
+#include "ortools/sat/cp_model_solver.h"
+#include "ortools/sat/sat_parameters.pb.h"
+#include "ortools/util/time_limit.h"
+#include "strings/memutil.h"
+
+namespace operations_research::sat {
+
+namespace {
+
+CpSolverResponse solveWithParameters(std::atomic<bool>* const limit_reached,
+                                     const CpModelProto& proto,
+                                     const SatParameters& params) {
+  Model model;
+  model.Add(NewSatParameters(params));
+  model.GetOrCreate<TimeLimit>()->RegisterExternalBooleanAsLimit(limit_reached);
+  return SolveCpModel(proto, &model);
+}
+
+}  // namespace
+
+extern "C" {
+
+void SolveCpModelWithParameters(const void* creq, int creq_len,
+                                const void* cparams, int cparams_len,
+                                void** cres, int* cres_len) {
+  return SolveCpInterruptible(nullptr, creq, creq_len, cparams, cparams_len,
+                              cres, cres_len);
+}
+
+void* SolveCpNewAtomicBool() { return new std::atomic<bool>(false); }
+
+void SolveCpDestroyAtomicBool(void* const atomic_bool) {
+  delete static_cast<std::atomic<bool>*>(atomic_bool);
+}
+
+void SolveCpStopSolve(void* const atomic_bool) {
+  *static_cast<std::atomic<bool>*>(atomic_bool) = true;
+}
+
+void SolveCpInterruptible(void* const limit_reached, const void* creq,
+                          int creq_len, const void* cparams, int cparams_len,
+                          void** cres, int* cres_len) {
+  CpModelProto req;
+  CHECK(req.ParseFromArray(creq, creq_len));
+
+  SatParameters params;
+  CHECK(params.ParseFromArray(cparams, cparams_len));
+
+  CpSolverResponse res = solveWithParameters(
+      static_cast<std::atomic<bool>*>(limit_reached), req, params);
+
+  std::string res_str;
+  CHECK(res.SerializeToString(&res_str));
+
+  *cres_len = static_cast<int>(res_str.size());
+  *cres = strings::memdup(res_str.data(), *cres_len);
+  CHECK(*cres != nullptr);
+}
+
+}  // extern "C"
+
+}  // namespace operations_research::sat

ortools/sat/go/cp_solver_c.h

@@ -0,0 +1,41 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+#ifndef OR_TOOLS_SAT_GO_CP_SOLVER_C_H_
+#define OR_TOOLS_SAT_GO_CP_SOLVER_C_H_
+
+#include <stddef.h>
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+void SolveCpModelWithParameters(const void* creq, int creq_len,
+                                const void* cparams, int cparams_len,
+                                void** cres, int* cres_len);
+
+void* SolveCpNewAtomicBool();
+void SolveCpDestroyAtomicBool(void* atomic_bool);
+void SolveCpStopSolve(void* atomic_bool);
+// Allows for interruptible solves. Solves can be interrupted by calling
+// `SolveCpStopSolve` with the `limit_reached` atomic Boolean.
+void SolveCpInterruptible(void* limit_reached, const void* creq, int creq_len,
+                          const void* cparams, int cparams_len, void** cres,
+                          int* cres_len);
+
+#ifdef __cplusplus
+}  // extern "C"
+#endif
+
+#endif  // OR_TOOLS_SAT_GO_CP_SOLVER_C_H_

ortools/sat/go/cp_solver_test.go

@@ -0,0 +1,275 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package cpmodel
+
+import (
+	"testing"
+
+	"golang/protobuf/v2/proto/proto"
+
+	cmpb "ortools/sat/cp_model_go_proto"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func TestCpSolver_SolveIntVar(t *testing.T) {
+	model := NewCpModelBuilder()
+
+	x := model.NewIntVar(1, 10)
+	y := model.NewIntVar(1, 10)
+
+	model.AddEquality(NewLinearExpr().AddSum(x, y), NewConstant(15))
+	model.Maximize(NewLinearExpr().AddTerm(x, 7).AddTerm(y, 1))
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModel(m)
+	if err != nil {
+		t.Fatalf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	wantStatus := cmpb.CpSolverStatus_OPTIMAL
+	gotStatus := res.GetStatus()
+	if wantStatus != gotStatus {
+		t.Errorf("SolveCpModel() returned status = %v, want %v", gotStatus, wantStatus)
+	}
+	wantObj := float64(75)
+	gotObj := res.GetObjectiveValue()
+	if wantObj != gotObj {
+		t.Errorf("SolveCpModel() returned objective = %v, got %v", gotObj, wantObj)
+	}
+	wantX := int64_t(10)
+	wantY := int64_t(5)
+	gotX := SolutionIntegerValue(res, x)
+	gotY := SolutionIntegerValue(res, y)
+	if wantX != gotX || wantY != gotY {
+		t.Errorf("SolutionIntegerValue() returned (x, y) = (%v, %v), want (%v, %v)", gotX, gotY, wantX, wantY)
+	}
+}
+
+func TestCpSolver_SolveBoolVar(t *testing.T) {
+	model := NewCpModelBuilder()
+
+	x := model.NewBoolVar()
+	y := model.NewBoolVar()
+
+	model.AddBoolOr(x, y.Not())
+	model.Minimize(x)
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModel(m)
+	if err != nil {
+		t.Fatalf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	wantStatus := cmpb.CpSolverStatus_OPTIMAL
+	gotStatus := res.GetStatus()
+	if wantStatus != gotStatus {
+		t.Errorf("SolveCpModel() return status = %v, want %v", gotStatus, wantStatus)
+	}
+	wantObj := float64(0)
+	gotObj := res.GetObjectiveValue()
+	if wantObj != gotObj {
+		t.Errorf("SolveCpModel() returned objective = %v, want %v", gotObj, wantObj)
+	}
+	gotX := SolutionBooleanValue(res, x)
+	gotY := SolutionBooleanValue(res, y)
+	if gotX || gotY {
+		t.Errorf("SolutionBooleanValue() returned (x, y) = (%v, %v), want (false, false)", gotX, gotY)
+	}
+	gotNotX := SolutionBooleanValue(res, x.Not())
+	gotNotY := SolutionBooleanValue(res, y.Not())
+	if !gotNotX || !gotNotY {
+		t.Errorf("SolutionBooleanValue() returned (x.Not(), y.Not()) = (%v, %v), want (true, true)", gotX, gotY)
+	}
+	wantIntX := int64_t(0)
+	wantIntY := int64_t(0)
+	gotIntX := SolutionIntegerValue(res, x)
+	gotIntY := SolutionIntegerValue(res, y)
+	if wantIntX != gotIntX || wantIntY != gotIntY {
+		t.Errorf("SolutionIntegerValue() returned (x, y) = (%v, %v), want (%v, %v)", gotIntX, gotIntY, wantIntX, wantIntY)
+	}
+	wantNotX := int64_t(1)
+	wantNotY := int64_t(1)
+	gotIntNotX := SolutionIntegerValue(res, x.Not())
+	gotIntNotY := SolutionIntegerValue(res, y.Not())
+	if wantNotX != gotIntNotX || wantNotY != gotIntNotY {
+		t.Errorf("SolutionIntegerValue() returned (x, y) = (%v, %v), want (%v, %v)", gotIntNotX, gotIntNotY, wantNotX, wantNotY)
+	}
+}
+
+func TestCpSolver_InvalidModel(t *testing.T) {
+	model := NewCpModelBuilder()
+
+	x := model.NewIntVar(0, -1)
+	y := model.NewIntVar(0, 10)
+
+	model.Maximize(NewLinearExpr().AddSum(x, y))
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModel(m)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+
+	want := cmpb.CpSolverStatus_MODEL_INVALID
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModel() returned status = %v, want %v", got, want)
+	}
+}
+
+func TestCpSolver_InfeasibleModel(t *testing.T) {
+	model := NewCpModelBuilder()
+
+	x := model.NewIntVar(0, 5)
+	y := model.NewIntVar(0, 5)
+
+	// Infeasible constraint
+	model.AddEquality(NewLinearExpr().AddSum(x, y), NewConstant(-5))
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModel(m)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	want := cmpb.CpSolverStatus_INFEASIBLE
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModel() returned status = %v, want %v", got, want)
+	}
+}
+
+func TestCpSolver_SolveWithParameters(t *testing.T) {
+	model := NewCpModelBuilder()
+	x := model.NewIntVar(0, 5)
+	y := model.NewIntVar(0, 5)
+	model.AddAllDifferent(x, y)
+	model.Maximize(NewLinearExpr().AddTerm(x, 5).AddTerm(y, 6))
+
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(-1),
+	}.Build()
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModelWithParameters(m, params)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	want := cmpb.CpSolverStatus_MODEL_INVALID
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModelWithParameters() returned status = %v, want %v", got, want)
+	}
+}
+
+func TestCpSolver_SolveInterruptible(t *testing.T) {
+	interrupt := make(chan struct{})
+	close(interrupt)
+
+	model := NewCpModelBuilder()
+	x := model.NewIntVar(0, 5)
+	y := model.NewIntVar(0, 5)
+	model.AddAllDifferent(x, y)
+	model.Maximize(NewLinearExpr().AddTerm(x, 5).AddTerm(y, 6))
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(10),
+	}.Build()
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	res, err := SolveCpModelInterruptibleWithParameters(m, params, interrupt)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+
+	want := cmpb.CpSolverStatus_UNKNOWN
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModelInterruptibleWithParameters() returned status = %v, want %v", got, want)
+	}
+}
+
+func TestCpSolver_SolveInterruptible_NotCancelled(t *testing.T) {
+	model := NewCpModelBuilder()
+	x := model.NewIntVar(0, 5)
+	y := model.NewIntVar(0, 5)
+	model.AddAllDifferent(x, y)
+	model.Maximize(NewLinearExpr().AddTerm(x, 5).AddTerm(y, 6))
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(10),
+	}.Build()
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	interrupt := make(chan struct{})
+	res, err := SolveCpModelInterruptibleWithParameters(m, params, interrupt)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	want := cmpb.CpSolverStatus_OPTIMAL
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModelInterruptibleWithParameters() returned status = %v, want %v", got, want)
+	}
+}
+
+func TestCpSolver_SolveInterruptible_BadParameters(t *testing.T) {
+	model := NewCpModelBuilder()
+	x := model.NewIntVar(0, 5)
+	y := model.NewIntVar(0, 5)
+	model.AddAllDifferent(x, y)
+	model.Maximize(NewLinearExpr().AddTerm(x, 5).AddTerm(y, 6))
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(-1),
+	}.Build()
+
+	m, err := model.Model()
+	if err != nil {
+		t.Fatalf("Model() returned with unexpected error %v", err)
+	}
+
+	interrupt := make(chan struct{})
+	res, err := SolveCpModelInterruptibleWithParameters(m, params, interrupt)
+	if err != nil {
+		t.Errorf("SolveCpModel returned with unexpected err: %v", err)
+	}
+	want := cmpb.CpSolverStatus_MODEL_INVALID
+	got := res.GetStatus()
+	if want != got {
+		t.Errorf("SolveCpModelInterruptibleWithParameters() returned status = %v, want %v", got, want)
+	}
+}

ortools/sat/go/domain.go

@@ -0,0 +1,183 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package cpmodel
+
+import (
+	"fmt"
+	"math"
+	"sort"
+)
+
+// ClosedInterval stores the closed interval `[start,end]`. If the `Start` is greater
+// than the `End`, the interval is considered empty.
+type ClosedInterval struct {
+	Start int64_t
+	End   int64_t
+}
+
+// checkOverflowAndAdd first checks if adding `delta` to `i` will cause an integer overflow.
+// It will return the value of the summation if there is no overflow. Otherwise, it will
+// return MaxInt64 or MinInt64 depending on the direction of the overflow.
+func checkOverflowAndAdd(i, delta int64_t) int64_t {
+	if i == math.MinInt64 || i == math.MaxInt64 {
+		return i
+	}
+
+	s := i + delta
+	if delta < 0 && s > i {
+		return math.MinInt64
+	}
+	if delta > 0 && s < i {
+		return math.MaxInt64
+	}
+
+	return s
+}
+
+// Offset adds an offset to both the `Start` and `End` of the ClosedInterval `c`. If the `Start`
+// is equal to MinInt or if `End` is equal to MaxInt, the offset does not get added since those
+// values represent an unbounded domain. Both `Start` and `End` are clamped at math.MinInt64 and
+// Math.MaxInt64.
+func (c ClosedInterval) Offset(delta int64_t) ClosedInterval {
+	return ClosedInterval{checkOverflowAndAdd(c.Start, delta), checkOverflowAndAdd(c.End, delta)}
+}
+
+// Domain stores an ordered list of ClosedIntervals. This represents any subset
+// of `[MinInt64,MaxInt64]`. This type can be used to represent such a set efficiently
+// as a sorted and non-adjacent list of intervals. This is efficient as long as the
+// size of such a list stays reasonable.
+type Domain struct {
+	intervals []ClosedInterval
+}
+
+// joinIntervals sorts the intervals in domain and combines two consecutive intervals
+// if they overlap or the start of the second is exactly one more than the end of the first.
+// If an interval's `start` is greater than its `end`, then the interval is considered empty.
+func (d *Domain) joinIntervals() {
+	var itvs []ClosedInterval
+	for _, v := range d.intervals {
+		if v.Start <= v.End {
+			itvs = append(itvs, v)
+		}
+	}
+	d.intervals = itvs
+	if len(d.intervals) == 0 {
+		return
+	}
+	sort.Slice(d.intervals, func(i, j int) bool {
+		if d.intervals[i].Start != d.intervals[j].Start {
+			return d.intervals[i].Start < d.intervals[j].Start
+		}
+		return d.intervals[i].End < d.intervals[j].End
+	})
+	newIntervals := []ClosedInterval{d.intervals[0]}
+	for i := 1; i < len(d.intervals); i++ {
+		lastInt := &newIntervals[len(newIntervals)-1]
+		if lastInt.End+1 >= d.intervals[i].Start {
+			if lastInt.End < d.intervals[i].End {
+				lastInt.End = d.intervals[i].End
+			}
+		} else {
+			newIntervals = append(newIntervals, d.intervals[i])
+		}
+	}
+	d.intervals = newIntervals
+}
+
+// NewEmptyDomain creates an empty Domain.
+func NewEmptyDomain() Domain {
+	return Domain{}
+}
+
+// NewSingleDomain creates a new singleton domain `[val]`.
+func NewSingleDomain(val int64_t) Domain {
+	return Domain{[]ClosedInterval{{val, val}}}
+}
+
+// NewDomain creates a new domain of a single interval `[left,right]`.
+// If `left > right`, an empty domain is returned.
+func NewDomain(left, right int64_t) Domain {
+	if left > right {
+		return NewEmptyDomain()
+	}
+	return Domain{[]ClosedInterval{{left, right}}}
+}
+
+// FromValues creates a new domain from `values`. `values` need not be
+// sorted and can repeat.
+func FromValues(values []int64_t) Domain {
+	var d Domain
+	for _, v := range values {
+		d.intervals = append(d.intervals, ClosedInterval{v, v})
+	}
+	d.joinIntervals()
+	return d
+}
+
+// FromIntervals creates a domain from the union of the set of unordered `intervals`.
+// If an interval's `start` is greater than its `end`, the interval is considered empty.
+func FromIntervals(intervals []ClosedInterval) Domain {
+	itvs := make([]ClosedInterval, len(intervals))
+	copy(itvs, intervals)
+	domain := Domain{itvs}
+	domain.joinIntervals()
+	return domain
+}
+
+// FromFlatIntervals creates a new domain from a flattened list of intervals. If there is an
+// interval where the start is greater than the end, the interval is considered empty. Returns
+// an error if the length of `values` is not even.
+func FromFlatIntervals(values []int64_t) (Domain, error) {
+	if len(values) == 0 {
+		return NewEmptyDomain(), nil
+	}
+	if len(values)%2 != 0 {
+		return NewEmptyDomain(), fmt.Errorf("len(values)=%v must be a multiple of 2", len(values))
+	}
+	var intervals []ClosedInterval
+	for i := 1; i < len(values); i += 2 {
+		intervals = append(intervals, ClosedInterval{values[i-1], values[i]})
+	}
+	d := Domain{intervals}
+	d.joinIntervals()
+	return d, nil
+}
+
+// FlattenedIntervals returns the flattened list of interval bounds of the domain.
+// For example, if Domain d is equal to `[0,2][5,5][9,10]` will return `[0,2,5,5,9,10]`.
+func (d Domain) FlattenedIntervals() []int64_t {
+	var result []int64
+	for _, i := range d.intervals {
+		result = append(result, i.Start, i.End)
+	}
+	return result
+}
+
+// Min returns the minimum value of the domain, and returns false if no minimum exists,
+// i.e. if the domain is empty.
+func (d Domain) Min() (int64_t, bool) {
+	if len(d.intervals) == 0 {
+		return 0, false
+	}
+	return d.intervals[0].Start, true
+}
+
+// Max returns the maximum value of the domain, and returns false if no maximum exists,
+// i.e. if the domain is empty.
+func (d Domain) Max() (int64_t, bool) {
+	if len(d.intervals) == 0 {
+		return 0, false
+	}
+	return d.intervals[len(d.intervals)-1].End, true
+}

ortools/sat/go/domain_test.go

@@ -0,0 +1,273 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package cpmodel
+
+import (
+	"math"
+	"strings"
+	"testing"
+
+	"golang/cmp/cmp"
+)
+
+func TestDomain_NewEmptyDomain(t *testing.T) {
+	got := NewEmptyDomain()
+	want := Domain{}
+
+	if diff := cmp.Diff(want, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+		t.Errorf("NewEmptyDomain() returned with unexpected diff (-want+got);\n%s", diff)
+	}
+}
+
+func TestDomain_NewSingleDomain(t *testing.T) {
+	got := NewSingleDomain(-1)
+	want := Domain{[]ClosedInterval{{-1, -1}}}
+
+	if diff := cmp.Diff(want, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+		t.Errorf("NewSingleDomain(-1) returned with unexpected diff (-want+got);\n%s", diff)
+	}
+}
+
+func TestDomain_NewDomain(t *testing.T) {
+	testCases := []struct {
+		left  int64_t
+		right int64_t
+		want  Domain
+	}{
+		{
+			left:  -5,
+			right: 10,
+			want:  Domain{[]ClosedInterval{{-5, 10}}},
+		},
+		{
+			left:  10,
+			right: -1,
+			want:  Domain{},
+		},
+	}
+
+	for _, test := range testCases {
+		got := NewDomain(test.left, test.right)
+		if diff := cmp.Diff(test.want, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+			t.Errorf("NewDomain(%v, %v) returned with unexpected diff (-want+got);\n%s", test.left, test.right, diff)
+		}
+	}
+}
+
+func TestDomain_FromValues(t *testing.T) {
+	testCases := []struct {
+		values []int64
+		want   Domain
+	}{
+		{
+			values: []int64_t{},
+			want:   Domain{},
+		},
+		{
+			values: []int64_t{4},
+			want:   Domain{[]ClosedInterval{{4, 4}}},
+		},
+		{
+			values: []int64_t{1, 1, 3, 1, 2, 3, 2, 3},
+			want:   Domain{[]ClosedInterval{{1, 3}}},
+		},
+		{
+			values: []int64_t{1, 2, 3, 7, 8, -4},
+			want:   Domain{[]ClosedInterval{{-4, -4}, {1, 3}, {7, 8}}},
+		},
+		{
+			values: []int64_t{1, 2, 3, 5, 4, 6, 10, 12, 11, 15, 8},
+			want:   Domain{[]ClosedInterval{{1, 6}, {8, 8}, {10, 12}, {15, 15}}},
+		},
+	}
+
+	for _, test := range testCases {
+		got := FromValues(test.values)
+		if diff := cmp.Diff(test.want, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+			t.Errorf("FromValues(%v) returned with unexpected diff (-want+got);\n%s", test.values, diff)
+		}
+	}
+}
+
+func TestDomain_FromIntervals(t *testing.T) {
+	testCases := []struct {
+		intervals []ClosedInterval
+		want      Domain
+	}{
+		{
+			intervals: []ClosedInterval{{0, 1}, {0, 10}, {-4, -2}},
+			want:      Domain{[]ClosedInterval{{-4, -2}, {0, 10}}},
+		},
+		{
+			intervals: []ClosedInterval{{0, 10}, {1, 6}},
+			want:      Domain{[]ClosedInterval{{0, 10}}},
+		},
+		{
+			intervals: []ClosedInterval{{0, 10}, {-1, 5}},
+			want:      Domain{[]ClosedInterval{{-1, 10}}},
+		},
+		{
+			intervals: []ClosedInterval{{0, 10}, {0, 10}},
+			want:      Domain{[]ClosedInterval{{0, 10}}},
+		},
+		{
+			intervals: []ClosedInterval{{0, 10}, {11, 5}},
+			want:      Domain{[]ClosedInterval{{0, 10}}},
+		},
+	}
+
+	for _, test := range testCases {
+		got := FromIntervals(test.intervals)
+		if diff := cmp.Diff(test.want, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+			t.Errorf("FromIntervals(%v) returned with unexpected diff (-want+got);\n%s", test.intervals, diff)
+		}
+	}
+}
+
+func TestDomain_FromFlatIntervals(t *testing.T) {
+	testCases := []struct {
+		flatIntervals []int64
+		wantDomain    Domain
+		wantError     string
+	}{
+		{
+			flatIntervals: []int64_t{},
+			wantDomain:    Domain{},
+		},
+		{
+			flatIntervals: []int64_t{1},
+			wantError:     "must be a multiple of 2",
+		},
+		{
+			flatIntervals: []int64_t{-1, 1, 3, 3, 5, 10},
+			wantDomain:    Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}},
+		},
+		{
+			flatIntervals: []int64_t{3, 9, 6, 10},
+			wantDomain:    Domain{[]ClosedInterval{{3, 10}}},
+		},
+		{
+			flatIntervals: []int64_t{3, 5, 5, 10},
+			wantDomain:    Domain{[]ClosedInterval{{3, 10}}},
+		},
+		{
+			flatIntervals: []int64_t{5, 3, 4, -1},
+			wantDomain:    Domain{},
+		},
+	}
+
+	for _, test := range testCases {
+		got, err := FromFlatIntervals(test.flatIntervals)
+		if err != nil && (test.wantError == "" || !strings.Contains(err.Error(), test.wantError)) {
+			t.Errorf("FromFlatIntervals(%v) returned with unexpected error %v, want %q substring", test.flatIntervals, err, test.wantError)
+		}
+		if diff := cmp.Diff(test.wantDomain, got, cmp.AllowUnexported(Domain{}, ClosedInterval{})); diff != "" {
+			t.Errorf("FromFlatIntervals(%v) returned with unexpected diff (-want+got);\n%s", test.flatIntervals, diff)
+		}
+	}
+}
+
+func TestDomain_FlattenedIntervals(t *testing.T) {
+	d := Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}}
+
+	got := d.FlattenedIntervals()
+	want := []int64_t{-1, 1, 3, 3, 5, 10}
+	if diff := cmp.Diff(want, got); diff != "" {
+		t.Errorf("FlattenedIntervals() returned with unexpected diff (-want+got);\n%s", diff)
+	}
+}
+
+func TestDomain_Min(t *testing.T) {
+	d := Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}}
+
+	want := int64_t(-1)
+	if got, ok := d.Min(); got != want || !ok {
+		t.Errorf("Min() returned with unexpected value (%v, %v), want (%v, %v)", got, ok, want, true)
+	}
+}
+
+func TestDomain_MinEmptyDomain(t *testing.T) {
+	emptyDomain := NewEmptyDomain()
+
+	if got, ok := emptyDomain.Min(); got != 0 || ok {
+		t.Errorf("Min() returned with unexpected value (%v, %v), want (%v, %v)", got, ok, 0, false)
+	}
+}
+
+func TestDomain_Max(t *testing.T) {
+	d := Domain{[]ClosedInterval{{-1, 1}, {3, 3}, {5, 10}}}
+
+	want := int64_t(10)
+	if got, ok := d.Max(); got != want || !ok {
+		t.Errorf("Max() returned with unexpected value (%v, %v), want (%v, %v)", got, ok, want, true)
+	}
+}
+
+func TestDomain_MaxEmptyDomain(t *testing.T) {
+	emptyDomain := NewEmptyDomain()
+
+	if got, ok := emptyDomain.Max(); got != 0 || ok {
+		t.Errorf("Max() returned with unexpected value (%v, %v), want (%v, %v)", got, ok, 0, false)
+	}
+}
+
+func TestDomain_Offset(t *testing.T) {
+	testCases := []struct {
+		interval ClosedInterval
+		delta    int64_t
+		want     ClosedInterval
+	}{
+		{
+			interval: ClosedInterval{1, 2},
+			delta:    -2,
+			want:     ClosedInterval{-1, 0},
+		},
+		{
+			interval: ClosedInterval{math.MinInt64, 2},
+			delta:    -2,
+			want:     ClosedInterval{math.MinInt64, 0},
+		},
+		{
+			interval: ClosedInterval{1, math.MaxInt64},
+			delta:    2,
+			want:     ClosedInterval{3, math.MaxInt64},
+		},
+		{
+			interval: ClosedInterval{math.MinInt64, math.MinInt64},
+			delta:    -2,
+			want:     ClosedInterval{math.MinInt64, math.MinInt64},
+		},
+		{
+			interval: ClosedInterval{math.MaxInt64, math.MaxInt64},
+			delta:    2,
+			want:     ClosedInterval{math.MaxInt64, math.MaxInt64},
+		},
+		{
+			interval: ClosedInterval{-1, 5},
+			delta:    math.MaxInt64,
+			want:     ClosedInterval{math.MaxInt64 - 1, math.MaxInt64},
+		},
+		{
+			interval: ClosedInterval{-1, 5},
+			delta:    math.MinInt64,
+			want:     ClosedInterval{math.MinInt64, math.MinInt64 + 5},
+		},
+	}
+
+	for _, test := range testCases {
+		if got := test.interval.Offset(test.delta); got != test.want {
+			t.Errorf("%#v.Offset(%v) return %#v, want %#v", test.interval, test.delta, got, test.want)
+		}
+	}
+}

ortools/sat/linear_constraint.h

@@ -41,27 +41,15 @@ namespace sat {
 struct LinearConstraint {
   IntegerValue lb;
   IntegerValue ub;
+
+  // TODO(user): This class is almost always static, replace by a size
+  // and two [] to save 24 bytes per constraints.
   std::vector<IntegerVariable> vars;
   std::vector<IntegerValue> coeffs;
 
   LinearConstraint() = default;
   LinearConstraint(IntegerValue _lb, IntegerValue _ub) : lb(_lb), ub(_ub) {}
 
-  void AddTerm(IntegerVariable var, IntegerValue coeff) {
-    vars.push_back(var);
-    coeffs.push_back(coeff);
-  }
-
-  void Clear() {
-    lb = ub = IntegerValue(0);
-    ClearTerms();
-  }
-
-  void ClearTerms() {
-    vars.clear();
-    coeffs.clear();
-  }
-
   std::string DebugString() const {
     std::string result;
     if (lb.value() > kMinIntegerValue) {
@@ -176,6 +164,8 @@ class LinearConstraintBuilder {
   // TODO(user): Have a subclass so we can enforce that a caller using
   // AddLiteralTerm() must construct the Builder with an encoder.
   LinearConstraintBuilder() : encoder_(nullptr), lb_(0), ub_(0) {}
+  LinearConstraintBuilder(IntegerValue lb, IntegerValue ub)
+      : encoder_(nullptr), lb_(lb), ub_(ub) {}
 
   // Adds the corresponding term to the current linear expression.
   void AddConstant(IntegerValue value);

ortools/sat/linear_programming_constraint.cc

@@ -16,6 +16,7 @@
 #include <algorithm>
 #include <array>
 #include <cmath>
+#include <cstddef>
 #include <cstdint>
 #include <functional>
 #include <limits>
@@ -103,22 +104,22 @@ bool ScatteredIntegerVector::Add(glop::ColIndex col, IntegerValue value) {
 
 template <bool check_overflow>
 bool ScatteredIntegerVector::AddLinearExpressionMultiple(
-    const IntegerValue multiplier,
-    const std::vector<std::pair<glop::ColIndex, IntegerValue>>& terms) {
+    const IntegerValue multiplier, absl::Span<const glop::ColIndex> cols,
+    absl::Span<const IntegerValue> coeffs) {
   const double threshold = 0.1 * static_cast<double>(dense_vector_.size());
-  if (is_sparse_ && static_cast<double>(terms.size()) < threshold) {
-    for (const std::pair<glop::ColIndex, IntegerValue>& term : terms) {
-      if (is_zeros_[term.first]) {
-        is_zeros_[term.first] = false;
-        non_zeros_.push_back(term.first);
+  const int num_terms = cols.size();
+  if (is_sparse_ && static_cast<double>(num_terms) < threshold) {
+    for (int i = 0; i < num_terms; ++i) {
+      if (is_zeros_[cols[i]]) {
+        is_zeros_[cols[i]] = false;
+        non_zeros_.push_back(cols[i]);
       }
       if (check_overflow) {
-        if (!AddProductTo(multiplier, term.second,
-                          &dense_vector_[term.first])) {
+        if (!AddProductTo(multiplier, coeffs[i], &dense_vector_[cols[i]])) {
           return false;
         }
       } else {
-        dense_vector_[term.first] += multiplier * term.second;
+        dense_vector_[cols[i]] += multiplier * coeffs[i];
       }
     }
     if (static_cast<double>(non_zeros_.size()) > threshold) {
@@ -126,14 +127,13 @@ bool ScatteredIntegerVector::AddLinearExpressionMultiple(
     }
   } else {
     is_sparse_ = false;
-    for (const std::pair<glop::ColIndex, IntegerValue>& term : terms) {
+    for (int i = 0; i < num_terms; ++i) {
       if (check_overflow) {
-        if (!AddProductTo(multiplier, term.second,
-                          &dense_vector_[term.first])) {
+        if (!AddProductTo(multiplier, coeffs[i], &dense_vector_[cols[i]])) {
           return false;
         }
       } else {
-        dense_vector_[term.first] += multiplier * term.second;
+        dense_vector_[cols[i]] += multiplier * coeffs[i];
       }
     }
   }
@@ -322,6 +322,9 @@ bool LinearProgrammingConstraint::CreateLpFromConstraintManager() {
 
   // Fill integer_lp_.
   integer_lp_.clear();
+  integer_lp_cols_.clear();
+  integer_lp_coeffs_.clear();
+
   infinity_norms_.clear();
   const auto& all_constraints = constraint_manager_.AllConstraints();
   for (const auto index : constraint_manager_.LpConstraints()) {
@@ -342,18 +345,22 @@ bool LinearProgrammingConstraint::CreateLpFromConstraintManager() {
     IntegerValue infinity_norm = 0;
     infinity_norm = std::max(infinity_norm, IntTypeAbs(ct.lb));
     infinity_norm = std::max(infinity_norm, IntTypeAbs(ct.ub));
-    new_ct.terms.reserve(size);
+    new_ct.start_in_buffer = integer_lp_cols_.size();
+    new_ct.num_terms = size;
     for (int i = 0; i < size; ++i) {
       // We only use positive variable inside this class.
       const IntegerVariable var = ct.vars[i];
       const IntegerValue coeff = ct.coeffs[i];
       infinity_norm = std::max(infinity_norm, IntTypeAbs(coeff));
-      new_ct.terms.push_back({GetMirrorVariable(var), coeff});
+      integer_lp_cols_.push_back(GetMirrorVariable(var));
+      integer_lp_coeffs_.push_back(coeff);
     }
     infinity_norms_.push_back(infinity_norm);
 
     // It is important to keep lp_data_ "clean".
-    DCHECK(std::is_sorted(new_ct.terms.begin(), new_ct.terms.end()));
+    DCHECK(std::is_sorted(
+        integer_lp_cols_.data() + new_ct.start_in_buffer,
+        integer_lp_cols_.data() + new_ct.start_in_buffer + new_ct.num_terms));
   }
 
   // Copy the integer_lp_ into lp_data_.
@@ -394,8 +401,10 @@ bool LinearProgrammingConstraint::CreateLpFromConstraintManager() {
     lp_data_.SetConstraintBounds(
         row, ct.lb_is_trivial ? -infinity : ToDouble(ct.lb),
         ct.ub_is_trivial ? +infinity : ToDouble(ct.ub));
-    for (const auto& term : ct.terms) {
-      lp_data_.SetCoefficient(row, term.first, ToDouble(term.second));
+    for (int i = 0; i < ct.num_terms; ++i) {
+      const int index = ct.start_in_buffer + i;
+      lp_data_.SetCoefficient(row, integer_lp_cols_[index],
+                              ToDouble(integer_lp_coeffs_[index]));
     }
   }
   lp_data_.NotifyThatColumnsAreClean();
@@ -1229,7 +1238,7 @@ bool LinearProgrammingConstraint::PostprocessAndAddCut(
         const int slack_index = (var.value() - first_slack.value()) / 2;
         const glop::RowIndex row = tmp_slack_rows_[slack_index];
         if (!tmp_scattered_vector_.AddLinearExpressionMultiple(
-                coeff, integer_lp_[row].terms)) {
+                coeff, IntegerLpRowCols(row), IntegerLpRowCoeffs(row))) {
           VLOG(2) << "Overflow in slack removal";
           ++num_cut_overflows_;
           return false;
@@ -1329,18 +1338,6 @@ void LinearProgrammingConstraint::AddCGCuts() {
   }
 }
 
-namespace {
-
-template <class ListOfTerms>
-IntegerValue GetCoeff(ColIndex col, const ListOfTerms& terms) {
-  for (const auto& term : terms) {
-    if (term.first == col) return term.second;
-  }
-  return IntegerValue(0);
-}
-
-}  // namespace
-
 // Because we know the objective is integer, the constraint objective >= lb can
 // sometime cut the current lp optimal, and it can make a big difference to add
 // it. Or at least use it when constructing more advanced cuts. See
@@ -1502,10 +1499,11 @@ void LinearProgrammingConstraint::AddMirCuts() {
     non_zeros_.SparseClearAll();
 
     // Copy cut.
-    for (const std::pair<ColIndex, IntegerValue>& term :
-         integer_lp_[entry.first].terms) {
-      const ColIndex col = term.first;
-      const IntegerValue coeff = term.second;
+    const LinearConstraintInternal& ct = integer_lp_[entry.first];
+    for (int i = 0; i < ct.num_terms; ++i) {
+      const int index = ct.start_in_buffer + i;
+      const ColIndex col = integer_lp_cols_[index];
+      const IntegerValue coeff = integer_lp_coeffs_[index];
       non_zeros_.Set(col);
       dense_cut[col] += coeff * multiplier;
     }
@@ -1588,8 +1586,18 @@ void LinearProgrammingConstraint::AddMirCuts() {
       const RowIndex row_to_combine =
           possible_rows[std::discrete_distribution<>(weights.begin(),
                                                      weights.end())(*random_)];
-      const IntegerValue to_combine_coeff =
-          GetCoeff(var_to_eliminate, integer_lp_[row_to_combine].terms);
+
+      // Find the coefficient of the variable to eliminate.
+      IntegerValue to_combine_coeff = 0;
+      const LinearConstraintInternal& ct_to_combine =
+          integer_lp_[row_to_combine];
+      for (int i = 0; i < ct_to_combine.num_terms; ++i) {
+        const int index = ct_to_combine.start_in_buffer + i;
+        if (integer_lp_cols_[index] == var_to_eliminate) {
+          to_combine_coeff = integer_lp_coeffs_[index];
+          break;
+        }
+      }
       CHECK_NE(to_combine_coeff, 0);
 
       IntegerValue mult1 = -to_combine_coeff;
@@ -1638,10 +1646,10 @@ void LinearProgrammingConstraint::AddMirCuts() {
       for (ColIndex col : non_zeros_.PositionsSetAtLeastOnce()) {
         dense_cut[col] *= mult1;
       }
-      for (const std::pair<ColIndex, IntegerValue>& term :
-           integer_lp_[row_to_combine].terms) {
-        const ColIndex col = term.first;
-        const IntegerValue coeff = term.second;
+      for (int i = 0; i < ct_to_combine.num_terms; ++i) {
+        const int index = ct_to_combine.start_in_buffer + i;
+        const ColIndex col = integer_lp_cols_[index];
+        const IntegerValue coeff = integer_lp_coeffs_[index];
         non_zeros_.Set(col);
         dense_cut[col] += coeff * mult2;
       }
@@ -1672,7 +1680,8 @@ void LinearProgrammingConstraint::AddZeroHalfCuts() {
     if (status == glop::ConstraintStatus::FREE) continue;
 
     zero_half_cut_helper_.AddOneConstraint(
-        row, integer_lp_[row].terms, integer_lp_[row].lb, integer_lp_[row].ub);
+        row, IntegerLpRowCols(row), IntegerLpRowCoeffs(row),
+        integer_lp_[row].lb, integer_lp_[row].ub);
   }
   for (const std::vector<std::pair<RowIndex, IntegerValue>>& multipliers :
        zero_half_cut_helper_.InterestingCandidates(random_)) {
@@ -2038,7 +2047,7 @@ bool LinearProgrammingConstraint::ComputeNewLinearConstraint(
 
     // Update the constraint.
     if (!scattered_vector->AddLinearExpressionMultiple<check_overflow>(
-            multiplier, integer_lp_[row].terms)) {
+            multiplier, IntegerLpRowCols(row), IntegerLpRowCoeffs(row))) {
       return false;
     }
 
@@ -2113,9 +2122,11 @@ void LinearProgrammingConstraint::AdjustNewLinearConstraint(
     // TODO(user): we could relax a bit some of the condition and allow a sign
     // change. It is just trickier to compute the diff when we allow such
     // changes.
-    for (const auto& entry : integer_lp_[row].terms) {
-      const ColIndex col = entry.first;
-      const IntegerValue coeff = entry.second;
+    const LinearConstraintInternal& ct = integer_lp_[row];
+    for (int i = 0; i < ct.num_terms; ++i) {
+      const int index = ct.start_in_buffer + i;
+      const ColIndex col = integer_lp_cols_[index];
+      const IntegerValue coeff = integer_lp_coeffs_[index];
       DCHECK_NE(coeff, 0);
 
       // Moving a variable away from zero seems to improve the bound even
@@ -2208,7 +2219,7 @@ void LinearProgrammingConstraint::AdjustNewLinearConstraint(
       adjusted = true;
       CHECK(scattered_vector
                 ->AddLinearExpressionMultiple</*check_overflow=*/false>(
-                    to_add, integer_lp_[row].terms));
+                    to_add, IntegerLpRowCols(row), IntegerLpRowCoeffs(row)));
     }
   }
   if (adjusted) ++num_adjusts_;
@@ -2299,9 +2310,17 @@ bool LinearProgrammingConstraint::PropagateExactLpReason() {
   // The "objective constraint" behave like if the unscaled cp multiplier was
   // 1.0, so we will multiply it by this number and add it to reduced_costs.
   const IntegerValue obj_scale = scaling;
+
+  // TODO(user): Maybe avoid this conversion.
+  tmp_cols_.clear();
+  tmp_coeffs_.clear();
+  for (const auto [col, coeff] : integer_objective_) {
+    tmp_cols_.push_back(col);
+    tmp_coeffs_.push_back(coeff);
+  }
   CHECK(tmp_scattered_vector_
             .AddLinearExpressionMultiple</*check_overflow=*/false>(
-                obj_scale, integer_objective_));
+                obj_scale, tmp_cols_, tmp_coeffs_));
   CHECK(AddProductTo(-obj_scale, integer_objective_offset_, &rc_ub));
   AdjustNewLinearConstraint(&tmp_integer_multipliers_, &tmp_scattered_vector_,
                             &rc_ub);
@@ -2682,5 +2701,19 @@ LinearProgrammingConstraint::HeuristicLpReducedCostBinary() {
   };
 }
 
+absl::Span<const glop::ColIndex> LinearProgrammingConstraint::IntegerLpRowCols(
+    glop::RowIndex row) const {
+  const int start = integer_lp_[row].start_in_buffer;
+  const size_t num_terms = static_cast<size_t>(integer_lp_[row].num_terms);
+  return {integer_lp_cols_.data() + start, num_terms};
+}
+
+absl::Span<const IntegerValue> LinearProgrammingConstraint::IntegerLpRowCoeffs(
+    glop::RowIndex row) const {
+  const int start = integer_lp_[row].start_in_buffer;
+  const size_t num_terms = static_cast<size_t>(integer_lp_[row].num_terms);
+  return {integer_lp_coeffs_.data() + start, num_terms};
+}
+
 }  // namespace sat
 }  // namespace operations_research

ortools/sat/linear_programming_constraint.h

@@ -76,9 +76,9 @@ class ScatteredIntegerVector {
   // Returns false if we encountered any integer overflow. If the template bool
   // is false, we do not check for a bit of extra speed.
   template <bool check_overflow = true>
-  bool AddLinearExpressionMultiple(
-      IntegerValue multiplier,
-      const std::vector<std::pair<glop::ColIndex, IntegerValue>>& terms);
+  bool AddLinearExpressionMultiple(IntegerValue multiplier,
+                                   absl::Span<const glop::ColIndex> cols,
+                                   absl::Span<const IntegerValue> coeffs);
 
   // This is not const only because non_zeros is sorted. Note that sorting the
   // non-zeros make the result deterministic whether or not we were in sparse
@@ -418,6 +418,10 @@ class LinearProgrammingConstraint : public PropagatorInterface,
   // linearization level 2 and above.
   void UpdateSimplexIterationLimit(int64_t min_iter, int64_t max_iter);
 
+  // Returns the col/coeff of integer_lp_[row].
+  absl::Span<const glop::ColIndex> IntegerLpRowCols(glop::RowIndex row) const;
+  absl::Span<const IntegerValue> IntegerLpRowCoeffs(glop::RowIndex row) const;
+
   // This epsilon is related to the precision of the value/reduced_cost returned
   // by the LP once they have been scaled back into the CP domain. So for large
   // domain or cost coefficient, we may have some issues.
@@ -442,10 +446,20 @@ class LinearProgrammingConstraint : public PropagatorInterface,
   struct LinearConstraintInternal {
     IntegerValue lb;
     IntegerValue ub;
-    LinearExpression terms;
+
+    // Point in integer_lp_cols_/integer_lp_coeffs_ for the actual data.
+    int start_in_buffer;
+    int num_terms;
+
     bool lb_is_trivial = false;
     bool ub_is_trivial = false;
   };
+  std::vector<glop::ColIndex> integer_lp_cols_;
+  std::vector<IntegerValue> integer_lp_coeffs_;
+
+  std::vector<glop::ColIndex> tmp_cols_;
+  std::vector<IntegerValue> tmp_coeffs_;
+
   LinearExpression integer_objective_;
   IntegerValue integer_objective_offset_ = IntegerValue(0);
   IntegerValue objective_infinity_norm_ = IntegerValue(0);

ortools/sat/samples/assumptions_sample_sat.go

@@ -0,0 +1,67 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The assumptions_sample_sat command is an example of setting assumptions on a model.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+func assumptionsSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 10)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+	a := model.NewBoolVar().WithName("a")
+	b := model.NewBoolVar().WithName("b")
+	c := model.NewBoolVar().WithName("c")
+
+	model.AddGreaterThan(x, y).OnlyEnforceIf(a)
+	model.AddGreaterThan(y, z).OnlyEnforceIf(b)
+	model.AddGreaterThan(z, x).OnlyEnforceIf(c)
+
+	// Add assumptions
+	model.AddAssumption(a, b, c)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("status: %s\n", response.GetStatus())
+	if response.GetStatus() == cmpb.CpSolverStatus_INFEASIBLE {
+		fmt.Println("sufficient assumptions for infeasibility:")
+		for _, index := range response.GetSufficientAssumptionsForInfeasibility() {
+			fmt.Printf("%d\n", index)
+		}
+	}
+
+	return nil
+}
+
+func main() {
+	if err := assumptionsSampleSat(); err != nil {
+		log.Exitf("assumptionsSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/binpacking_problem_sat.go

@@ -0,0 +1,121 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The binpacking_problem_sat command is an example of a bin packing problem that uses channeling
+// constraints.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const (
+	binCapacity   = 100
+	slackCapacity = 20
+	safeCapacity  = binCapacity - slackCapacity
+	numBins       = 5
+)
+
+type item struct {
+	Cost, Copies int64_t
+}
+
+func binpackingProblemSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	items := []item{{20, 6}, {15, 6}, {30, 4}, {45, 3}}
+	numItems := len(items)
+
+	// Main variables.
+	x := make([][]cpmodel.IntVar, numItems)
+	for i, item := range items {
+		x[i] = make([]cpmodel.IntVar, numBins)
+		for b := 0; b < numBins; b++ {
+			x[i][b] = model.NewIntVar(0, item.Copies)
+		}
+	}
+
+	// Load variables.
+	load := make([]cpmodel.IntVar, numBins)
+	for b := 0; b < numBins; b++ {
+		load[b] = model.NewIntVar(0, binCapacity)
+	}
+
+	// Slack variables.
+	slacks := make([]cpmodel.BoolVar, numBins)
+	for b := 0; b < numBins; b++ {
+		slacks[b] = model.NewBoolVar()
+	}
+
+	// Links load and x.
+	for b := 0; b < numBins; b++ {
+		expr := cpmodel.NewLinearExpr()
+		for i := 0; i < numItems; i++ {
+			expr.AddTerm(x[i][b], items[i].Cost)
+		}
+		model.AddEquality(expr, load[b])
+	}
+
+	// Place all items.
+	for i := 0; i < numItems; i++ {
+		copies := cpmodel.NewLinearExpr()
+		for _, b := range x[i] {
+			copies.Add(b)
+		}
+		model.AddEquality(copies, cpmodel.NewConstant(items[i].Copies))
+	}
+
+	// Links load and slack through an equivalence relation.
+	for b := 0; b < numBins; b++ {
+		// slacks[b] => load[b] <= safeCapacity.
+		model.AddLessOrEqual(load[b], cpmodel.NewConstant(safeCapacity)).OnlyEnforceIf(slacks[b])
+		// slacks[b].Not() => load[b] > safeCapacity.
+		model.AddGreaterThan(load[b], cpmodel.NewConstant(safeCapacity)).OnlyEnforceIf(slacks[b].Not())
+	}
+
+	// Maximize sum of slacks.
+	obj := cpmodel.NewLinearExpr()
+	for _, s := range slacks {
+		obj.Add(s)
+	}
+	model.Maximize(obj)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Println("Status: ", response.GetStatus())
+	fmt.Println("Objective: ", response.GetObjectiveValue())
+	fmt.Println("Statistics: ")
+	fmt.Println("  - conflicts : ", response.GetNumConflicts())
+	fmt.Println("  - branches  : ", response.GetNumBranches())
+	fmt.Println("  - wall time : ", response.GetWallTime())
+
+	return nil
+}
+
+func main() {
+	if err := binpackingProblemSat(); err != nil {
+		log.Exitf("binpackingProblemSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/bool_or_sample_sat.go

@@ -0,0 +1,32 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The bool_or_sample_sat command is simple example of the BoolOr constraint.
+package main
+
+import (
+	"ortools/sat/go/cpmodel"
+)
+
+func boolOrSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar()
+	y := model.NewBoolVar()
+
+	model.AddBoolOr(x, y.Not())
+}
+
+func main() {
+	boolOrSampleSat()
+}

ortools/sat/samples/boolean_product_sample_sat.go

@@ -0,0 +1,73 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The boolean_product_sample_sat command is a simple example of the product of two literals.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func booleanProductSample() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar().WithName("x")
+	y := model.NewBoolVar().WithName("y")
+	p := model.NewBoolVar().WithName("p")
+
+	// x and y implies p, rewrite as not(x and y) or p.
+	model.AddBoolOr(x.Not(), y.Not(), p)
+
+	// p implies x and y, expanded into two implications.
+	model.AddImplication(p, x)
+	model.AddImplication(p, y)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	// Set `fill_additional_solutions_in_response` and `enumerate_all_solutions` to true so
+	// the solver returns all solutions found.
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(4),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		fmt.Printf("x: %v", additionalSolution.GetValues()[x.Index()])
+		fmt.Printf(" y: %v", additionalSolution.GetValues()[y.Index()])
+		fmt.Printf(" p: %v\n", additionalSolution.GetValues()[p.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	err := booleanProductSample()
+	if err != nil {
+		log.Exitf("booleanProductSample returned with error: %v", err)
+	}
+}

ortools/sat/samples/channeling_sample_sat.go

@@ -0,0 +1,81 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The channeling_sample_sat command is a simple example of a channeling constraint.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func channelingSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our two primary variables.
+	x := model.NewIntVar(0, 10)
+	y := model.NewIntVar(0, 10)
+
+	// Declare our intermediate Boolean variable.
+	b := model.NewBoolVar()
+
+	// Implement b == (x > 5).
+	model.AddGreaterOrEqual(x, cpmodel.NewConstant(5)).OnlyEnforceIf(b)
+	model.AddLessThan(x, model.NewConstant(5)).OnlyEnforceIf(b.Not())
+
+	// Create our two half-reified constraints.
+	// First, b implies (y == 10 - x).
+	model.AddEquality(cpmodel.NewLinearExpr().Add(x).Add(y), cpmodel.NewConstant(10)).OnlyEnforceIf(b)
+	// Second, b.Not() implies (y == 0).
+	model.AddEquality(y, cpmodel.NewConstant(0)).OnlyEnforceIf(b.Not())
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(11),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x: %v y: %v b: %v\n", vs[x.Index()], vs[y.Index()], vs[b.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := channelingSampleSat(); err != nil {
+		log.Exitf("channelingSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/earliness_tardiness_cost_sample_sat.go

@@ -0,0 +1,90 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The earliness_tardiness_cost_sample_sat command is an example of an implementation of a convex
+// piecewise linear function.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+const (
+	earlinessDate = 5
+	earlinessCost = 8
+	latenessDate  = 15
+	latenessCost  = 12
+	largeConstant = 1000
+)
+
+func earlinessTardinessCostSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our primary variable.
+	x := model.NewIntVar(0, 20)
+
+	// Create the expression variable and implement the piecewise linear function.
+	//
+	//  \        /
+	//   \______/
+	//   ed    ld
+	//
+	expr := model.NewIntVar(0, largeConstant)
+
+	// Link together expr and x through the 3 segments.
+	firstSegment := cpmodel.NewConstant(earlinessDate*earlinessCost).AddTerm(x, -earlinessCost)
+	secondSegment := cpmodel.NewConstant(0)
+	thirdSegment := cpmodel.NewConstant(-latenessDate*latenessCost).AddTerm(x, latenessCost)
+	model.AddMaxEquality(expr, firstSegment, secondSegment, thirdSegment)
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(21),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x= %v expr= %v\n", vs[x.Index()], vs[expr.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := earlinessTardinessCostSampleSat(); err != nil {
+		log.Exitf("earlinessTardinessCostSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/interval_sample_sat.go

@@ -0,0 +1,58 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The interval_sample_sat_go command is a simple example of the Interval variable.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 100
+
+func intervalSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVar(2, 4).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	// An interval can be created from three affine expressions.
+	intervalVar := model.NewIntervalVar(x, y, cpmodel.NewConstant(2).Add(z)).WithName("interval")
+
+	// If the size is fixed, a simpler version uses the start expression and the size.
+	fixedSizeIntervalVar := model.NewFixedSizeIntervalVar(x, 10).WithName("fixedSizeInterval")
+
+	// A fixed interval can be created using the same API.
+	fixedIntervalVar := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(5), 10).WithName("fixedInterval")
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	fmt.Printf("%v\n", m.GetConstraints()[intervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedSizeIntervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedIntervalVar.Index()])
+
+	return nil
+}
+
+func main() {
+	if err := intervalSampleSat(); err != nil {
+		log.Exitf("intervalSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/literal_sample_sat.go

@@ -0,0 +1,33 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The literal_sample_sat command is a simple example of literals.
+package main
+
+import (
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+func literalSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar().WithName("x")
+	notX := x.Not()
+
+	log.Infof("x = %d, x.Not() = %d", x.Index(), notX.Index())
+}
+
+func main() {
+	literalSampleSat()
+}

ortools/sat/samples/no_overlap_sample_sat.go

@@ -0,0 +1,90 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The no_overlap_sample_sat command is an example of the NoOverlap constraints.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 21 // 3 weeks
+
+func noOverlapSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	// Task 0, duration 2.
+	start0 := model.NewIntVarFromDomain(domain)
+	duration0 := cpmodel.NewConstant(2)
+	end0 := model.NewIntVarFromDomain(domain)
+	task0 := model.NewIntervalVar(start0, duration0, end0)
+
+	// Task 1, duration 4.
+	start1 := model.NewIntVarFromDomain(domain)
+	duration1 := cpmodel.NewConstant(4)
+	end1 := model.NewIntVarFromDomain(domain)
+	task1 := model.NewIntervalVar(start1, duration1, end1)
+
+	// Task 2, duration 3
+	start2 := model.NewIntVarFromDomain(domain)
+	duration2 := cpmodel.NewConstant(2)
+	end2 := model.NewIntVarFromDomain(domain)
+	task2 := model.NewIntervalVar(start2, duration2, end2)
+
+	// Weekends.
+	weekend0 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(5), 2)
+	weekend1 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(12), 2)
+	weekend2 := model.NewFixedSizeIntervalVar(cpmodel.NewConstant(19), 2)
+
+	// No Overlap constraint.
+	model.AddNoOverlap(task0, task1, task2, weekend0, weekend1, weekend2)
+
+	// Makespan.
+	makespan := model.NewIntVarFromDomain(domain)
+	model.AddLessOrEqual(end0, makespan)
+	model.AddLessOrEqual(end1, makespan)
+	model.AddLessOrEqual(end2, makespan)
+
+	model.Minimize(makespan)
+
+	// Solve.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Println(response.GetStatus())
+		fmt.Println("Optimal Schedule Length: ", response.GetObjectiveValue())
+		fmt.Println("Task 0 starts at ", cpmodel.SolutionIntegerValue(response, start0))
+		fmt.Println("Task 1 starts at ", cpmodel.SolutionIntegerValue(response, start1))
+		fmt.Println("Task 2 starts at ", cpmodel.SolutionIntegerValue(response, start2))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := noOverlapSampleSat(); err != nil {
+		log.Exitf("noOverlapSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/nqueens_sat.go

@@ -0,0 +1,81 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The nqueens_sat command is an OR-Tools solution to the N-queens problem.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const boardSize = 8
+
+func nQueensSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	// There are `boardSize` number of variables, one for a queen in each column
+	// of the board. The value of each variable is the row that the queen is in.
+	var queenRows []cpmodel.LinearArgument
+	for i := 0; i < boardSize; i++ {
+		queenRows = append(queenRows, model.NewIntVar(0, int64_t(boardSize-1)))
+	}
+
+	// The following sets the constraint that all queens are in different rows.
+	model.AddAllDifferent(queenRows...)
+
+	// No two queens can be on the same diagonal.
+	var diag1 []cpmodel.LinearArgument
+	var diag2 []cpmodel.LinearArgument
+	for i := 0; i < boardSize; i++ {
+		diag1 = append(diag1, cpmodel.NewConstant(int64_t(i)).Add(queenRows[i]))
+		diag2 = append(diag2, cpmodel.NewConstant(int64_t(-i)).Add(queenRows[i]))
+	}
+	model.AddAllDifferent(diag1...)
+	model.AddAllDifferent(diag2...)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+	fmt.Printf("Objective: %v\n", response.GetObjectiveValue())
+
+	fmt.Printf("Solution:\n")
+	for i := int64_t(0); i < boardSize; i++ {
+		for j := 0; j < boardSize; j++ {
+			if cpmodel.SolutionIntegerValue(response, queenRows[j]) == i {
+				fmt.Print("Q")
+			} else {
+				fmt.Print("_")
+			}
+		}
+		fmt.Println()
+	}
+
+	return nil
+}
+
+func main() {
+	err := nQueensSat()
+	if err != nil {
+		log.Exitf("nQueensSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/nurses_sat.go

@@ -0,0 +1,126 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The nurses_sat command is an example of a simple nurse scheduling problem.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const (
+	numNurses         = 4
+	numDays           = 3
+	numShifts         = 3
+	minShiftsPerNurse = (numShifts * numDays) / numNurses
+	maxShiftsPerNurse = (numShifts*numDays-1)/numNurses + 1
+)
+
+func nursesSat() error {
+	// Creates the model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Creates shift variables.
+	// shifts[shiftKey]: nurse 'n' works shift 's' on day 'd'.
+	type shiftKey struct {
+		nurse int
+		shift int
+		day   int
+	}
+	shifts := make(map[shiftKey]cpmodel.BoolVar)
+	for n := 1; n <= numNurses; n++ {
+		for d := 1; d <= numDays; d++ {
+			for s := 1; s <= numShifts; s++ {
+				key := shiftKey{nurse: n, shift: s, day: d}
+				shifts[key] = model.NewBoolVar().WithName(fmt.Sprintf("shift_n%vd%vs%v", n, d, s))
+			}
+		}
+	}
+
+	// Each shift is assigned to exactly one nurse in the schedule period.
+	for d := 1; d <= numDays; d++ {
+		for s := 1; s <= numShifts; s++ {
+			var nurses []cpmodel.BoolVar
+			for n := 1; n <= numNurses; n++ {
+				nurses = append(nurses, shifts[shiftKey{nurse: n, shift: s, day: d}])
+			}
+			model.AddExactlyOne(nurses...)
+		}
+	}
+
+	// Each nurse works at most one shift per day.
+	for n := 1; n <= numNurses; n++ {
+		for d := 1; d <= numDays; d++ {
+			var work []cpmodel.BoolVar
+			for s := 1; s <= numShifts; s++ {
+				work = append(work, shifts[shiftKey{nurse: n, shift: s, day: d}])
+			}
+			model.AddAtMostOne(work...)
+		}
+	}
+
+	// Try to distribute the shifts evenly so that each nurse works `minShiftsPerNurse` shifts.
+	// If this is not possible because the total number of shifts is not divisible by the number
+	// of nurses, some nurses will be assigned one more shift.
+	for n := 1; n <= numNurses; n++ {
+		shiftsWorked := cpmodel.NewLinearExpr()
+		for d := 1; d <= numDays; d++ {
+			for s := 1; s <= numShifts; s++ {
+				shiftsWorked.Add(shifts[shiftKey{nurse: n, shift: s, day: d}])
+			}
+		}
+		model.AddLessOrEqual(cpmodel.NewConstant(minShiftsPerNurse), shiftsWorked)
+		model.AddLessOrEqual(shiftsWorked, cpmodel.NewConstant(maxShiftsPerNurse))
+	}
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+	fmt.Printf("Objective: %v\n", response.GetObjectiveValue())
+
+	fmt.Printf("Solution:\n")
+	for d := 1; d <= numDays; d++ {
+		fmt.Printf("Day %v\n", d)
+		for n := 1; n <= numNurses; n++ {
+			var isWorking bool
+			for s := 1; s <= numShifts; s++ {
+				key := shiftKey{nurse: n, shift: s, day: d}
+				if cpmodel.SolutionBooleanValue(response, shifts[key]) {
+					isWorking = true
+					fmt.Printf("  Nurse %v works shift %v\n", n, s)
+				}
+			}
+			if !isWorking {
+				fmt.Printf("  Nurse %v does not work\n", n)
+			}
+		}
+	}
+
+	return nil
+}
+
+func main() {
+	if err := nursesSat(); err != nil {
+		log.Exitf("nursesSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/optional_interval_sample_sat.go

@@ -0,0 +1,56 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The optional_interval_sample_sat command is an example of an Interval variable that is
+// marked as optional.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"ortools/sat/go/cpmodel"
+)
+
+const horizon = 100
+
+func optionalIntervalSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+	domain := cpmodel.NewDomain(0, horizon)
+
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVar(2, 4).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+	presenceVar := model.NewBoolVar().WithName("presence")
+
+	// An optional interval can be created from three affine expressions and a BoolVar.
+	intervalVar := model.NewOptionalIntervalVar(x, y, cpmodel.NewConstant(2).Add(z), presenceVar).WithName("interval")
+
+	// If the size is fixed, a simpler version uses the start expression and the size.
+	fixedSizeIntervalVar := model.NewOptionalFixedSizeIntervalVar(x, 10, presenceVar).WithName("fixedSizeInterval")
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	fmt.Printf("%v\n", m.GetConstraints()[intervalVar.Index()])
+	fmt.Printf("%v\n", m.GetConstraints()[fixedSizeIntervalVar.Index()])
+
+	return nil
+}
+
+func main() {
+	if err := optionalIntervalSampleSat(); err != nil {
+		log.Exitf("optionalIntervalSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/rabbits_and_pheasants_sat.go

@@ -0,0 +1,63 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The rabbits_and_pheasants_sat command is an example of a simple sat program that
+// solves the rabbits and pheasants problem.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const numAnimals = 20
+
+func rabbitsAndPheasants() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	allAnimals := cpmodel.NewDomain(0, numAnimals)
+	rabbits := model.NewIntVarFromDomain(allAnimals).WithName("rabbits")
+	pheasants := model.NewIntVarFromDomain(allAnimals).WithName("pheasants")
+
+	model.AddEquality(cpmodel.NewLinearExpr().AddSum(rabbits, pheasants), cpmodel.NewConstant(numAnimals))
+	model.AddEquality(cpmodel.NewLinearExpr().AddTerm(rabbits, 4).AddTerm(pheasants, 2), cpmodel.NewConstant(56))
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	switch response.GetStatus() {
+	case cmpb.CpSolverStatus_OPTIMAL, cmpb.CpSolverStatus_FEASIBLE:
+		fmt.Printf("There are %d rabbits and %d pheasants.\n",
+			cpmodel.SolutionIntegerValue(response, rabbits),
+			cpmodel.SolutionIntegerValue(response, pheasants))
+	default:
+		fmt.Println("No solution found.")
+	}
+
+	return nil
+}
+
+func main() {
+	if err := rabbitsAndPheasants(); err != nil {
+		log.Exitf("rabbitsAndPheasants returned with error: %v", err)
+	}
+}

ortools/sat/samples/ranking_sample_sat.go

@@ -0,0 +1,165 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The ranking_sample_sat command is an example of ranking intervals in a NoOverlap constraint.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+const (
+	horizonLength = 100
+	numTasks      = 4
+)
+
+// rankTasks adds constraints and variables to link tasks and ranks. This method
+// assumes that all starts are disjoint, meaning that all tasks have a strictly
+// positive duration, and they appear in the same NoOverlap constraint.
+func rankTasks(starts []cpmodel.IntVar, presences []cpmodel.BoolVar, ranks []cpmodel.IntVar, model *cpmodel.Builder) {
+	// Creates precedence variables between pairs of intervals.
+	precedences := make([][]cpmodel.BoolVar, numTasks)
+	for i := 0; i < numTasks; i++ {
+		precedences[i] = make([]cpmodel.BoolVar, numTasks)
+		for j := 0; j < numTasks; j++ {
+			if i == j {
+				precedences[i][i] = presences[i]
+			} else {
+				prec := model.NewBoolVar()
+				precedences[i][j] = prec
+				model.AddLessOrEqual(starts[i], starts[j]).OnlyEnforceIf(prec)
+			}
+		}
+	}
+
+	// Treats optional intervals.
+	for i := 0; i+1 < numTasks; i++ {
+		for j := i + 1; j < numTasks; j++ {
+			// Make sure that if task i is not performed, all precedences are false.
+			model.AddImplication(presences[i].Not(), precedences[i][j].Not())
+			model.AddImplication(presences[i].Not(), precedences[j][i].Not())
+			// Make sure that if task j is not performed, all precedences are false.
+			model.AddImplication(presences[j].Not(), precedences[i][j].Not())
+			model.AddImplication(presences[j].Not(), precedences[j][i].Not())
+			// The following BoolOr will enforce that for any two intervals:
+			// 		i precedes j or j precedes i or at least one interval is not performed.
+			model.AddBoolOr(precedences[i][j], precedences[j][i], presences[i].Not(), presences[j].Not())
+			// Redundant constraint: it propagates early that at most one precedence
+			// is true.
+			model.AddImplication(precedences[i][j], precedences[j][i].Not())
+			model.AddImplication(precedences[j][i], precedences[i][j].Not())
+		}
+	}
+
+	// Links precedences and ranks.
+	for i := 0; i < numTasks; i++ {
+		sumOfPredecessors := cpmodel.NewConstant(-1)
+		for j := 0; j < numTasks; j++ {
+			sumOfPredecessors.Add(precedences[j][i])
+		}
+		model.AddEquality(ranks[i], sumOfPredecessors)
+	}
+}
+
+func rankingSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	starts := make([]cpmodel.IntVar, numTasks)
+	ends := make([]cpmodel.IntVar, numTasks)
+	intervals := make([]cpmodel.IntervalVar, numTasks)
+	presences := make([]cpmodel.BoolVar, numTasks)
+	ranks := make([]cpmodel.IntVar, numTasks)
+
+	horizon := cpmodel.NewDomain(0, horizonLength)
+	possibleRanks := cpmodel.NewDomain(-1, numTasks-1)
+
+	for t := 0; t < numTasks; t++ {
+		start := model.NewIntVarFromDomain(horizon)
+		duration := cpmodel.NewConstant(int64_t(t + 1))
+		end := model.NewIntVarFromDomain(horizon)
+		var presence cpmodel.BoolVar
+		if t < numTasks/2 {
+			presence = model.TrueVar()
+		} else {
+			presence = model.NewBoolVar()
+		}
+		interval := model.NewOptionalIntervalVar(start, duration, end, presence)
+		rank := model.NewIntVarFromDomain(possibleRanks)
+
+		starts[t] = start
+		ends[t] = end
+		intervals[t] = interval
+		presences[t] = presence
+		ranks[t] = rank
+	}
+
+	// Adds NoOverlap constraint.
+	model.AddNoOverlap(intervals...)
+
+	// Ranks tasks.
+	rankTasks(starts, presences, ranks, model)
+
+	// Adds a constraint on ranks.
+	model.AddLessThan(ranks[0], ranks[1])
+
+	// Creates makespan variables.
+	makespan := model.NewIntVarFromDomain(horizon)
+	for t := 0; t < numTasks; t++ {
+		model.AddLessOrEqual(ends[t], makespan).OnlyEnforceIf(presences[t])
+	}
+
+	// Create objective: minimize 2 * makespan - 7 * sum of presences.
+	// This is you gain 7 by interval performed, but you pay 2 by day of delays.
+	objective := cpmodel.NewLinearExpr().AddTerm(makespan, 2)
+	for t := 0; t < numTasks; t++ {
+		objective.AddTerm(presences[t], -7)
+	}
+	model.Minimize(objective)
+
+	// Solving part.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Println(response.GetStatus())
+		fmt.Println("Optimal cost: ", response.GetObjectiveValue())
+		fmt.Println("Makespan: ", cpmodel.SolutionIntegerValue(response, makespan))
+		for t := 0; t < numTasks; t++ {
+			rank := cpmodel.SolutionIntegerValue(response, ranks[t])
+			if cpmodel.SolutionBooleanValue(response, presences[t]) {
+				start := cpmodel.SolutionIntegerValue(response, starts[t])
+				fmt.Printf("Task %v starts at %v with rank %v\n", t, start, rank)
+			} else {
+				fmt.Printf("Task %v is not performed and ranked at %v\n", t, rank)
+			}
+		}
+	}
+
+	return nil
+}
+
+func main() {
+	if err := rankingSampleSat(); err != nil {
+		log.Exitf("rankingSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/reified_sample_sat.go

@@ -0,0 +1,42 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The reified_sample_sat command is a simple example of implication constraints.
+package main
+
+import (
+	"ortools/sat/go/cpmodel"
+)
+
+func reifiedSampleSat() {
+	model := cpmodel.NewCpModelBuilder()
+
+	x := model.NewBoolVar()
+	y := model.NewBoolVar()
+	b := model.NewBoolVar()
+
+	// First version using a half-reified bool and.
+	model.AddBoolAnd(x, y.Not()).OnlyEnforceIf(b)
+
+	// Second version using implications.
+	model.AddImplication(b, x)
+	model.AddImplication(b, y.Not())
+
+	// Third version using bool or.
+	model.AddBoolOr(b.Not(), x)
+	model.AddBoolOr(b.Not(), y.Not())
+}
+
+func main() {
+	reifiedSampleSat()
+}

ortools/sat/samples/search_for_all_solutions_sample_sat.go

@@ -0,0 +1,68 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The search_for_all_solutions_sample_sat command is an example for how to search for
+// all solutions.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func searchForAllSolutionsSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	// Currently, the CpModelBuilder does not allow for callbacks, so each feasible solution cannot
+	// be printed while solving. However, the CP Solver can return all of the enumerated solutions
+	// in the response by setting the following parameters.
+	params := sppb.SatParameters_builder{
+		EnumerateAllSolutions:             proto.Bool(true),
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(27),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	for i, solution := range response.GetAdditionalSolutions() {
+		vs := solution.GetValues()
+		fmt.Printf("Solution %v: x = %v, y = %v, z = %v\n", i, vs[x.Index()], vs[y.Index()], vs[z.Index()])
+	}
+
+	fmt.Println("Number of solutions found: ", len(response.GetAdditionalSolutions()))
+
+	return nil
+}
+
+func main() {
+	if err := searchForAllSolutionsSampleSat(); err != nil {
+		log.Exitf("searchForAllSolutionsSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/simple_sat_program.go

@@ -0,0 +1,60 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The simple_sat_program command is an example of a simple sat program.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+func simpleSatProgram() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	switch response.GetStatus() {
+	case cmpb.CpSolverStatus_OPTIMAL, cmpb.CpSolverStatus_FEASIBLE:
+		fmt.Printf("x = %d\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf("y = %d\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf("z = %d\n", cpmodel.SolutionIntegerValue(response, z))
+	default:
+		fmt.Println("No solution found.")
+	}
+
+	return nil
+}
+
+func main() {
+	if err := simpleSatProgram(); err != nil {
+		log.Exitf("simpleSatProgram returned with error: %v", err)
+	}
+}

ortools/sat/samples/solution_hinting_sample_sat.go

@@ -0,0 +1,65 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The solution_hinting_sample_sat command is an example of setting solution hints on the model.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+)
+
+func solutionHintingSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	model.Maximize(cpmodel.NewLinearExpr().AddWeightedSum([]cpmodel.LinearArgument{x, y, z}, []int64_t{1, 2, 3}))
+
+	// Solution hinting: x <- 1, y <- 2
+	hint := &cpmodel.Hint{Ints: map[cpmodel.IntVar]int64_t{x: 7}}
+	model.SetHint(hint)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	response, err := cpmodel.SolveCpModel(m)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Printf(" x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf(" y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf(" z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := solutionHintingSampleSat(); err != nil {
+		log.Exitf("solutionHintingSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.go

@@ -0,0 +1,70 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The solve_and_print_intermediate_solutions_sample_sat command
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func solveAndPrintIntermediateSolutionsSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	model.Maximize(cpmodel.NewLinearExpr().Add(x).AddTerm(y, 2).AddTerm(z, 3))
+
+	// Create a solver and solve with a fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+
+	// Currently, the CpModelBuilder does not allow for callbacks, so intermediate solutions
+	// cannot be printed while solving. However, the CP-SAT solver does allow for returning
+	// the intermediate solutions found while solving in the response.
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(10),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Println("Number of intermediate solutions found: ", len(response.GetAdditionalSolutions()))
+
+	fmt.Println("Optimal solution:")
+	fmt.Printf("  x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+	fmt.Printf("  y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+	fmt.Printf("  z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+
+	return nil
+}
+
+func main() {
+	if err := solveAndPrintIntermediateSolutionsSampleSat(); err != nil {
+		log.Exitf("solveAndPrintIntermediateSolutionsSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/solve_with_time_limit_sample_sat.go

@@ -0,0 +1,68 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The solve_with_time_limit_sample_sat command is an example of setting a time limit on the model.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func solveWithTimeLimitSampleSat() error {
+	model := cpmodel.NewCpModelBuilder()
+
+	domain := cpmodel.NewDomain(0, 2)
+	x := model.NewIntVarFromDomain(domain).WithName("x")
+	y := model.NewIntVarFromDomain(domain).WithName("y")
+	z := model.NewIntVarFromDomain(domain).WithName("z")
+
+	model.AddNotEqual(x, y)
+
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+
+	// Sets a time limit of 10 seconds.
+	params := sppb.SatParameters_builder{
+		MaxTimeInSeconds: proto.Float64(10.0),
+	}.Build()
+
+	// Solve.
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	if response.GetStatus() == cmpb.CpSolverStatus_OPTIMAL {
+		fmt.Printf(" x = %v\n", cpmodel.SolutionIntegerValue(response, x))
+		fmt.Printf(" y = %v\n", cpmodel.SolutionIntegerValue(response, y))
+		fmt.Printf(" z = %v\n", cpmodel.SolutionIntegerValue(response, z))
+	}
+
+	return nil
+}
+
+func main() {
+	if err := solveWithTimeLimitSampleSat(); err != nil {
+		log.Exitf("solveWithTimeLimitSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/samples/step_function_sample_sat.go

@@ -0,0 +1,99 @@
+// Copyright 2010-2024 Google LLC
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// The step_function_sample_sat command is an example of an implementation of a step function.
+package main
+
+import (
+	"fmt"
+
+	"ortools/base/go/log"
+	"golang/protobuf/v2/proto/proto"
+	cmpb "ortools/sat/cp_model_go_proto"
+	"ortools/sat/go/cpmodel"
+	sppb "ortools/sat/sat_parameters_go_proto"
+)
+
+func stepFunctionSampleSat() error {
+	// Create the CP-SAT model.
+	model := cpmodel.NewCpModelBuilder()
+
+	// Declare our primary variable.
+	x := model.NewIntVar(0, 20)
+
+	// Create the expression variable and implement the step function
+	// Note it is not defined for var == 2.
+	//
+	//        -               3
+	// -- --      ---------   2
+	//                        1
+	//      -- ---            0
+	//           1         2
+	// 012345678901234567890
+	//
+	expr := model.NewIntVar(0, 3)
+
+	// expr == 0 on [5, 6] U [8, 10]
+	b0 := model.NewBoolVar()
+	d0 := cpmodel.FromValues([]int64_t{5, 6, 8, 9, 10})
+	model.AddLinearConstraintForDomain(x, d0).OnlyEnforceIf(b0)
+	model.AddEquality(expr, cpmodel.NewConstant(0)).OnlyEnforceIf(b0)
+
+	// expr == 2 on [0, 1] U [3, 4] U [11, 20]
+	b2 := model.NewBoolVar()
+	d2 := cpmodel.FromIntervals([]cpmodel.ClosedInterval{{0, 1}, {3, 4}, {11, 20}})
+	model.AddLinearConstraintForDomain(x, d2).OnlyEnforceIf(b2)
+	model.AddEquality(expr, cpmodel.NewConstant(2)).OnlyEnforceIf(b2)
+
+	// expr = 3 when x = 7
+	b3 := model.NewBoolVar()
+	model.AddEquality(x, cpmodel.NewConstant(7)).OnlyEnforceIf(b3)
+	model.AddEquality(expr, cpmodel.NewConstant(3)).OnlyEnforceIf(b3)
+
+	// At least one Boolean variable is true.
+	model.AddBoolOr(b0, b2, b3)
+
+	// Search for x values in increasing order.
+	model.AddDecisionStrategy([]cpmodel.IntVar{x}, cmpb.DecisionStrategyProto_CHOOSE_FIRST, cmpb.DecisionStrategyProto_SELECT_MIN_VALUE)
+
+	// Create a solver and solve with fixed search.
+	m, err := model.Model()
+	if err != nil {
+		return fmt.Errorf("failed to instantiate the CP model: %w", err)
+	}
+	params := sppb.SatParameters_builder{
+		FillAdditionalSolutionsInResponse: proto.Bool(true),
+		EnumerateAllSolutions:             proto.Bool(true),
+		SolutionPoolSize:                  proto.Int32(21),
+		SearchBranching:                   sppb.SatParameters_FIXED_SEARCH.Enum(),
+	}.Build()
+	response, err := cpmodel.SolveCpModelWithParameters(m, params)
+	if err != nil {
+		return fmt.Errorf("failed to solve the model: %w", err)
+	}
+
+	fmt.Printf("Status: %v\n", response.GetStatus())
+
+	for _, additionalSolution := range response.GetAdditionalSolutions() {
+		vs := additionalSolution.GetValues()
+		fmt.Printf("x= %v expr= %v\n", vs[x.Index()], vs[expr.Index()])
+	}
+
+	return nil
+}
+
+func main() {
+	if err := stepFunctionSampleSat(); err != nil {
+		log.Exitf("stepFunctionSampleSat returned with error: %v", err)
+	}
+}

ortools/sat/zero_half_cuts.cc

@@ -18,6 +18,7 @@
 #include <vector>
 
 #include "absl/log/check.h"
+#include "absl/types/span.h"
 #include "ortools/base/logging.h"
 #include "ortools/lp_data/lp_types.h"
 #include "ortools/sat/integer.h"
@@ -66,23 +67,24 @@ void ZeroHalfCutHelper::AddBinaryRow(const CombinationOfRows& binary_row) {
   rows_.push_back(binary_row);
 }
 
-void ZeroHalfCutHelper::AddOneConstraint(
-    const glop::RowIndex row,
-    const std::vector<std::pair<glop::ColIndex, IntegerValue>>& terms,
-    IntegerValue lb, IntegerValue ub) {
-  if (terms.size() > kMaxInputConstraintSize) return;
+void ZeroHalfCutHelper::AddOneConstraint(const glop::RowIndex row,
+                                         absl::Span<const glop::ColIndex> cols,
+                                         absl::Span<const IntegerValue> coeffs,
+                                         IntegerValue lb, IntegerValue ub) {
+  const int num_terms = cols.size();
+  if (num_terms > kMaxInputConstraintSize) return;
 
   double activity = 0.0;
   IntegerValue magnitude(0);
   CombinationOfRows binary_row;
   int rhs_adjust = 0;
-  for (const auto& term : terms) {
-    const int col = term.first.value();
-    activity += ToDouble(term.second) * lp_values_[col];
-    magnitude = std::max(magnitude, IntTypeAbs(term.second));
+  for (int i = 0; i < num_terms; ++i) {
+    const int col = cols[i].value();
+    activity += ToDouble(coeffs[i]) * lp_values_[col];
+    magnitude = std::max(magnitude, IntTypeAbs(coeffs[i]));
 
     // Only consider odd coefficient.
-    if ((term.second.value() & 1) == 0) continue;
+    if ((coeffs[i].value() & 1) == 0) continue;
 
     // Ignore column in the binary matrix if its lp value is almost zero.
     if (shifted_lp_values_[col] > 1e-2) {

ortools/sat/zero_half_cuts.h

@@ -48,10 +48,9 @@ class ZeroHalfCutHelper {
   void ProcessVariables(const std::vector<double>& lp_values,
                         const std::vector<IntegerValue>& lower_bounds,
                         const std::vector<IntegerValue>& upper_bounds);
-  void AddOneConstraint(
-      glop::RowIndex,
-      const std::vector<std::pair<glop::ColIndex, IntegerValue>>& terms,
-      IntegerValue lb, IntegerValue ub);
+  void AddOneConstraint(glop::RowIndex, absl::Span<const glop::ColIndex> cols,
+                        absl::Span<const IntegerValue> coeffs, IntegerValue lb,
+                        IntegerValue ub);
   std::vector<std::vector<std::pair<glop::RowIndex, IntegerValue>>>
   InterestingCandidates(ModelRandomGenerator* random);