OCaml interface to Google OR-Tools

OR-Tools is an open source software suite for optimization, tuned for tackling the world's toughest problems in vehicle routing, flows, integer and linear programming, and constraint programming.

This interface allows for modeling problems in OCaml and exporting them, using Protocol Buffers, for solution by different solvers. At least in principle: for now, only the basic features of CP-SAT are supported.

The CP-SAT Primer gives an excellent introduction to constraint programming in general, and to the CP-SAT interface in particular. The examples are easily translated from Python to OCaml.

Building Models

• Ortools.Sat Build a model for CP-SAT

let model = Ortools.Sat.make () in

(* Add variables. *)
let ub = max [50; 45; 37] in
let x = Ortools.Sat.Var.new_int model ~lb:0 ~ub "x" in
let y = Ortools.Sat.Var.new_int model ~lb:0 ~ub "y" in
let z = Ortools.Sat.Var.new_int model ~lb:0 ~ub "z" in

(* Add constraints. *)
Ortools.Sat.(add model (2 * x + 7 * y + 3 * z <= of_int 50));
Ortools.Sat.(add model (3 * x - 5 * y + 7 * z <= of_int 45));
Ortools.Sat.(add model (5 * x + 2 * y - 6 * z <= of_int 37));

(* Set objective. *) 
Ortools.Sat.(maximize model (2 * x + 2 * y + 3 * z));

(* Solve the model. *)
let Ortools.Sat.Response.{ status;
		  objective_value;
		  solution;
		  num_conflicts;
		  num_branches;
		  wall_time; _ }
  = Ortools_solvers.Sat.solve ~parameters model
in

(match status with
| Optimal | Feasible ->
  printf "Maximum of objective function: %g\n\n" objective_value;
  printf "x = %d\n" solution.(Ortools.Sat.Var.to_index x);
  printf "y = %d\n" solution.(Ortools.Sat.Var.to_index y);
  printf "z = %d\n" solution.(Ortools.Sat.Var.to_index z)
| _ -> printf "No solution found.\n");

(* Statistics. *)
printf "\nStatistics\n";
printf "  status   : %s\n" (Ortools.Sat.Response.string_of_status status);
printf "  conflicts: %d\n" num_conflicts;
printf "  branches : %d\n" num_branches;
printf "  wall time: %g s\n" wall_time

In the example above, access to the solver is provided by the Ortools_solvers package. An alternative is to dump the model to a file:

let oc = open_out "cp_sat_example.pb" in
Ortools.Sat.pb_output model oc;
close_out oc

and invoke the solver via C++ or Python, e.g.,

from ortools.sat.python import cp_model

model = cp_model.CpModel()
model.Proto().ParseFromString(Path("cp_sat_example.pb").read_bytes())
solver = cp_model.CpSolver()
status = solver.solve(model)

if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print(f"Maximum of objective function: {solver.objective_value}\n")
    for i, v in enumerate(proto.variables):
	pv = cp_model.IntVar(proto, i, v.domain == [0, 1], None)
	print(f"{v.name} = {solver.value(pv)}")
else:
    print("No solution found.")

print("\nStatistics")
print(f"  status   : {solver.status_name(status)}")
print(f"  conflicts: {solver.num_conflicts}")
print(f"  branches : {solver.num_branches}")
print(f"  wall time: {solver.wall_time} s")

Note that when the protocol buffers are loaded in this way, the model data structures are not updated, that's why IntVar is used to create variables on-the-fly.

Raw Protocol Buffers

OCaml interfaces generated from cp_model.proto and sat_parameters.proto using ocaml-protoc.

Sat_parameters

• Ortools.Sat_parameters Code for sat_parameters.proto

Ortools.Sat.Parameters.defaults gives the set of default parameters.

Ortools.Sat_parameters.make_sat_parameters is used to specify non-default parameters for CP-SAT. For example:

let parameters = Sat_parameters.make_sat_parameters
		     ~max_time_in_seconds:60.
		     ~relative_gap_limit:0.05
		     (* ~absolute_gap_limit *)
		     ~log_search_progress:true
		     ~log_to_stdout:true
		     (* ~log_prefix *)
		      ~num_workers:8
		     ()

Cp_model

• Ortools.Cp_model Code for cp_model.proto

This raw interface is not normally used directly. Normally a CP-SAT model is constructed using the functions in Ortools.Sat and converted to a protcol buffer with either Ortools.Sat.to_proto, Ortools.Sat.pb_encode, or Ortools.Sat.pb_output.