SAT - integer programming backend

Problem: choose integer values for two variables that maximize the objective while satisfying linear limits.

Show code 
import { initMPSolver, MPSolver, setWorkerBridgeEnabled } from 'or-tools-wasm/mp-solver';

setWorkerBridgeEnabled(true);
await initMPSolver();

const solver = MPSolver.CreateSolver('SAT');
if (!solver) throw new Error('SAT backend is unavailable');
solver.SetNumThreads(4);

const x = solver.IntVar(0, solver.infinity(), 'x');
const y = solver.IntVar(0, solver.infinity(), 'y');
const c0 = solver.Constraint(-solver.infinity(), 17.5);
c0.SetCoefficient(x, 1);
c0.SetCoefficient(y, 7);
const c1 = solver.Constraint(-solver.infinity(), 3.5);
c1.SetCoefficient(x, 1);

const objective = solver.Objective();
objective.SetCoefficient(x, 1);
objective.SetCoefficient(y, 10);
objective.SetMaximization();

const workers = 4;
await solver.SolveWithProto({ solverSpecificParameters: `num_workers: ${workers}` });
console.log(x.solution_value(), y.solution_value());

Direct port of simple_mip_program.py through the MPSolver SAT integer backend.

Model

  • The decision variables are integer values for x and y.
  • The linear constraints define which integer points are feasible.
  • The objective maximizes a linear score over those feasible points.
  • The SAT backend searches the integer feasible set and returns the best assignment.
Run the solver to view the solution.

Status / Response: