Boolean operations on constraints in Google or-tools library

Question

I'm beginner in constraint programming and I'm using Google or-tools library in my c# program.

I want to add following constraint to my solver:

((t1 >= 12 && t1 <= 15) || (t2 >= 16 && t2 <= 18)) && ( t1 + t2 ) < 30

So I write following piece of code in c#:

var solver = new Solver("My_CP_Colver");
var t1 = solver.MakeIntVar(12, 20,"t1");
var t2 = solver.MakeIntVar(12, 20,"t2");

solver.Add(???)//<-((t1 >= 12 && t1 <= 15)||(t2 >= 16 && t2 <= 18)) && ( t1 + t2 ) < 30

Any help to make above constraint please?

Answer 1

My language is python, I think it should easy translate follow pytho code to C#.

model = cp_model.CpModel()

t1 = model.NewIntVar(12, 20, "t1")
t1_bool_ge = model.NewBoolVar("t1_bool_ge")
t1_bool_le = model.NewBoolVar("t1_bool_le")
t1_bool_and =  model.NewBoolVar("t1_bool_and")
tmp_t1 = []
tmp_t1.append(t1_bool_ge)
tmp_t1.append(t1_bool_le)
model.Add(t1 >= 12).OnlyEnforceIf(t1_bool_ge) # t1 >=12
model.Add(t1 <= 15).OnlyEnforceIf(t1_bool_le) # t1 <= 15
model.Add(t1_bool_and==1).OnlyEnforceIf(tmp_t1) # (t1 >=12)&&(t1 <= 15)

t2 = model.NewIntVar(12, 20, "t2")
t2_bool_ge = model.NewBoolVar("t2_bool_ge")
t2_bool_le = model.NewBoolVar("t2_bool_le")
t2_bool_and =  model.NewBoolVar("t2_bool_and")
tmp_t2 = []
tmp_t2.append(t2_bool_ge)
tmp_t2.append(t2_bool_le)
model.Add(t2 >= 16).OnlyEnforceIf(t2_bool_ge) # t2 >=16
model.Add(t2 <= 18).OnlyEnforceIf(t2_bool_le) # t2 <= 18
model.Add(t2_bool_and==1).OnlyEnforceIf(tmp_t2) #(t2 >=16) && (t2 <=18)

tmp_t1_t2 = []
tmp_t1_t2.append(t2_bool_and)
tmp_t1_t2.append(t1_bool_and)
model.Add(sum(tmp_t1_t2)==1) #((t1 >=12)&&(t1 <= 15))||((t2 >=16) && (t2 <=18))

model.Add(t1 + t2 < 30) # ( t1 + t2 ) < 30

Answer 2

Unfortunately, Google or-tools library does not provide rich logical constraints. If you can develop your implementation in Java, I recommend you to use Choco Solver which includes a SAT solver with extensive number of SAT constraints.

The current way of formulating logical constraints in Google or-tools is converting them into linear constraints. It would be better to check this first to understand the concept of transformation, then, have a look at Who killed Agatha example from HakanK. Here a part of this implementation related to logical constraints :

//   if (i != j) =>
//       ((richer[i,j] = 1) <=> (richer[j,i] = 0))
for(int i = 0; i < n; i++) {
  for(int j = 0; j < n; j++) {
    if (i != j) {
      solver.Add((richer[i, j]==1) - (richer[j, i]==0) == 0);
    }
  }
}

You can also check this post.

Answer 3

You can use MakeMin and MakeMax to encode the conjunctions and disjunctions respectively. Doing so for each piece, you end up with something like the following:

var solver = new Solver("MY_CP_Solver");
var t1 = solver.MakeIntVar(12, 20, "t1");
var t1ge = solver.MakeGreaterOrEqual(t1, 12);
var t1le = solver.MakeLessOrEqual(t1, 15);
var t1both = solver.MakeMin(t1ge, t1le);

var t2 = solver.MakeIntVar(12, 20, "t2");
var t2ge = solver.MakeGreaterOrEqual(t2, 16);
var t2le = solver.MakeLessOrEqual(t2, 18);
var t2both = solver.MakeMin(t2ge, t2le);
var or = solver.MakeMax(t1both, t2both);

solver.Add(or == 1);
solver.Add(t1 + t2 < 30);

var db = solver.MakePhase(new[] {t1, t2}, Solver.CHOOSE_FIRST_UNBOUND, Solver.ASSIGN_MIN_VALUE);
solver.Solve(db);

while (solver.NextSolution())
    Console.WriteLine($"t1: {t1.Value()}, t2: {t2.Value()}");

Output:

t1: 12, t2: 12
t1: 12, t2: 13
t1: 12, t2: 14
t1: 12, t2: 15
t1: 12, t2: 16
t1: 12, t2: 17
t1: 13, t2: 12
t1: 13, t2: 13
t1: 13, t2: 14
t1: 13, t2: 15
t1: 13, t2: 16
t1: 14, t2: 12
t1: 14, t2: 13
t1: 14, t2: 14
t1: 14, t2: 15
t1: 15, t2: 12
t1: 15, t2: 13
t1: 15, t2: 14

In particular, the first constraint in your disjunction is always active.

Using the newer Google.OrTools.Sat.CpSolver, you could do something like the following where we introduce an auxiliary boolean b, which has the property that it ensures that at least one of the clauses in the disjunction is satisfied:

var model = new CpModel();
var t1 = model.NewIntVar(12, 20, "t1");
var t2 = model.NewIntVar(12, 20, "t2");
var b = model.NewBoolVar("First constraint active");

model.Add(t1 >= 12).OnlyEnforceIf(b);
model.Add(t1 <= 15).OnlyEnforceIf(b);
model.Add(t2 >= 16).OnlyEnforceIf(b.Not());
model.Add(t2 <= 18).OnlyEnforceIf(b.Not());
model.Add(t1 + t2 < 30);
var solver = new CpSolver();
var cb = new SolutionPrinter(new [] { t1, t2 });
solver.SearchAllSolutions(model, cb);

Here, the printer is defined as follows:

public class SolutionPrinter : CpSolverSolutionCallback
{
    public VarArraySolutionPrinter(IntVar[] v) => this.v = v;
    public override void OnSolutionCallback() => Console.WriteLine($"t1: {Value(v[0])}, t2: {Value(v[1])}");
    private readonly IntVar[] v;
}

Note that this will find the same (t1, t2)-pairs multiple times (but with different values of b)