Google OR tools: how to evaluate complex or multi-level boolean constraints

Question

Set up

I am using the google OR tools as a constraint programming solver:

from ortools.sat.python import cp_model

I have defined the following BoolVars

model = cp_model.CpModel()
a = model.NewBoolVar("a")
b = model.NewBoolVar("b")
c = model.NewBoolVar("c")
d = model.NewBoolVar("d")
e = model.NewBoolVar("e")
f = model.NewBoolVar("f")
g = model.NewBoolVar("g")

Question

I need to add a complex boolean constraint to the model. Something like

(a || b) && (d || e) == g

How can I add a complex boolean constraint like this to the model?

PS: I couldn't find this information immediately online, but found a solution based on an answer I got on a related problem here and another related problem of another person here. I summarize my findings here in Q&A style in the hope that they will be useful for someone.

Answer 1

This kind of constraint cannot be added at once to the model. The constraint needs to be split up in its components (and & or gates). Each basic component needs to be set equal to a new BoolVar. These are then combined to add the final constraint.

Breakdown to basic components

We'll do this as follows:

(a || b) == c
(d || e) == f
(c && f) == g

This last equation is equivalent to the original equation:

(a || b) && (d || e) == g

Storing basic constraints in new BoolVars

An "OR" type of equation can be evaluated with the following function:

def evaluate_or(a, b, c):
    # Either a or b or both must be 1 if c is 1.
    model.AddBoolOr([a, b]).OnlyEnforceIf(c)

    # The above line is not sufficient, as no constraints are defined if c==0 (see reference documentation of
    # "OnlyEnforceIf". We therefore add another line to cover the case when c==0:

    # a and b must both be 0 if c is 0
    model.AddBoolAnd([a.Not(), b.Not()]).OnlyEnforceIf([c.Not()])

An "AND" type of equation can similarily be evaluated with the following function:

def evaluate_and(a, b, c):
    # Both a and b must be 1 if c is 1
    model.AddBoolAnd([a, b]).OnlyEnforceIf(c)

    #What happens if c is 0? This is still undefined thus let us add another line:

    # Either a or b or both must be 0 if c is 0.
    model.AddBoolOr([a.Not(), b.Not()]).OnlyEnforceIf(c.Not())

In this specific case the basic constraints are twice an OR gate. We store them in c and f:

evaluate_or(a, b, c)
evaluate_or(d, e, f)

Adding the complex constraint

This is now really simple and can be done using the BoolVars from the previous step and an AND gate:

evaluate_and(c, f, g)

Discussion

Any complex constraint can be added using intermediary BoolVars and the defined OR and AND gate functions above. The constraint just needs to be broken down into its basic components.

Full program

This is the full program:

from ortools.sat.python import cp_model

model = cp_model.CpModel()
a = model.NewBoolVar("a")
b = model.NewBoolVar("b")
c = model.NewBoolVar("c")
d = model.NewBoolVar("d")
e = model.NewBoolVar("e")
f = model.NewBoolVar("f")
g = model.NewBoolVar("g")

def evaluate_or(a, b, c):
    # Either a or b or both must be 1 if c is 1.
    model.AddBoolOr([a, b]).OnlyEnforceIf(c)

    # The above line is not sufficient, as no constraints are defined if c==0 (see reference documentation of
    # "OnlyEnforceIf". We therefore add another line to cover the case when c==0:

    # a and b must both be 0 if c is 0
    model.AddBoolAnd([a.Not(), b.Not()]).OnlyEnforceIf([c.Not()])

def evaluate_and(a, b, c):
    # Both a and b must be 1 if c is 1
    model.AddBoolAnd([a, b]).OnlyEnforceIf(c)

    #What happens if c is 0? This is still undefined thus let us add another line:

    # Either a or b or both must be 0 if c is 0.
    model.AddBoolOr([a.Not(), b.Not()]).OnlyEnforceIf(c.Not())

#Add the constraints
evaluate_or(a, b, c)
evaluate_or(d, e, f)
evaluate_and(c, f, g)


# Solve the model.
solver = cp_model.CpSolver()
solver.parameters.enumerate_all_solutions = True
status = solver.Solve(model, cp_model.VarArraySolutionPrinter([a, b, c, d, e, f, g]))

Output

The following output is obtained:

Solution 0, time = 0.00 s
  a = 0   b = 0   c = 0   d = 1   e = 0   f = 1   g = 0 
Solution 1, time = 0.00 s
  a = 0   b = 0   c = 0   d = 1   e = 1   f = 1   g = 0 
Solution 2, time = 0.00 s
  a = 0   b = 0   c = 0   d = 0   e = 1   f = 1   g = 0 
Solution 3, time = 0.00 s
  a = 0   b = 0   c = 0   d = 0   e = 0   f = 0   g = 0 
Solution 4, time = 0.00 s
  a = 0   b = 1   c = 1   d = 0   e = 0   f = 0   g = 0 
Solution 5, time = 0.00 s
  a = 0   b = 1   c = 1   d = 1   e = 0   f = 1   g = 1 
Solution 6, time = 0.00 s
  a = 0   b = 1   c = 1   d = 1   e = 1   f = 1   g = 1 
Solution 7, time = 0.00 s
  a = 0   b = 1   c = 1   d = 0   e = 1   f = 1   g = 1 
Solution 8, time = 0.00 s
  a = 1   b = 1   c = 1   d = 0   e = 1   f = 1   g = 1 
Solution 9, time = 0.00 s
  a = 1   b = 1   c = 1   d = 1   e = 1   f = 1   g = 1 
Solution 10, time = 0.00 s
  a = 1   b = 1   c = 1   d = 1   e = 0   f = 1   g = 1 
Solution 11, time = 0.00 s
  a = 1   b = 1   c = 1   d = 0   e = 0   f = 0   g = 0 
Solution 12, time = 0.00 s
  a = 1   b = 0   c = 1   d = 0   e = 0   f = 0   g = 0 
Solution 13, time = 0.00 s
  a = 1   b = 0   c = 1   d = 0   e = 1   f = 1   g = 1 
Solution 14, time = 0.00 s
  a = 1   b = 0   c = 1   d = 1   e = 1   f = 1   g = 1 
Solution 15, time = 0.00 s
  a = 1   b = 0   c = 1   d = 1   e = 0   f = 1   g = 1