I was working through an example CP-SAT program on sports team scheduling, and I found a bit of AddBoolOr logic that I didn’t understand. So I wrote up a short program to explore what was going on.
Stringing together multiple AddBoolOrs
I was examining the logic in
sports_scheduling_sat.cc,
and came across the breaks logic. The idea of a break in the code is
a sequence of two home or two away games in a row. Breaks are
identified with a binary variable, and that break variable is reified
(if that is the right term) by using four AddBoolOr constraints.
a = model.NewBoolVar('home day 1')
b = model.NewBoolVar('home day 2')
c = model.NewBoolVar('break')
model.AddBoolOr([a.Not(), b.Not(), c])
model.AddBoolOr([a, b, c])
model.AddBoolOr([a.Not(), b, c.Not()])
model.AddBoolOr([a, b.Not(), c.Not()])
This will generates the truth table:
home day 1=1 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
I really didn’t understand this at all, so I broke it down. First of
all, AddBoolOr is defined as requiring that at least one of the
passed array of boolean variables is true. So line by line:
model.AddBoolOr([a.Not(), b.Not(), c])
This says if c==True then one or both of a.Not() or b.Not() can
be False, because the requirement that one value is true is taken
care of by c. On the other hand, if c==False, then one of
a.Not() or b.Not() must be true; they can’t both be false. Just
this constraint results in the following truth table:
home day 1=0 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=0 break=1
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
If break is true, then Not(home day 1) and Not(home day 2) can take on any value; if break is false, then the case of both Not(home day 1) and Not(home day 2) being false is forbidden. Removing the “Not”, that means that the case of both home day 1 and home day 2 being true is forbidden if break is false.
Similarly
model.AddBoolOr([a, b, c])
says if c==True then one or both of a or b can
be False, because the requirement that one value is true is taken
care of by c. And again, if c==False, then one of
a or b must be true; they can’t both be false. The resulting
truth table is the same when break is true, but slightly different for
when break is false:
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=0 break=1
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
When break is false, then it cannot be that both home day 1 and home day 2 are also false.
So combining these two constraints at the same time, I would expect that when break is false, it will not be possible to have both home day 1 and home day 2 be true, nor to have them both be false. Which we see is the case. The partially commented code
model.AddBoolOr([a.Not(), b.Not(), c])
model.AddBoolOr([a, b, c])
# model.AddBoolOr([a.Not(), b, c.Not()])
# model.AddBoolOr([a, b.Not(), c.Not()])
generates the truth table
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=0 break=1
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
These two constraints have no impact whatsoever on the cases in which break is true, as both home day 1 and home day 2 can take on any value in any combination.
Moving on to the break=False cases,
model.AddBoolOr([a.Not(), b, c.Not()])
generates the truth table:
home day 1=0 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
All the embeded Not() calls make this tricky to reason over, but
what it is saying is that if c==True (this period is a break) then
c.Not()==False, which means that at least one of the other variables
in the array must be true: [a.Not(),b] If a.Not()==True, that
means a==False. So the resulting cases can either be a==False and
b==False, or b==True and a==True, or both a==False and
b==True, but not a==True and b==False.
The next expression eliminates the case of a==False and b=True:
model.AddBoolOr([a, b.Not(), c.Not()])
home day 1=0 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=0 break=1
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
Both of these c.Not() constraints leave untouched the case of
c==True, and both of them leave alone the case of both a==True, b==True or a==False, b==False. So taken together, the resulting
truth table gets rid of the cases in which a and b are different when
c is true.
# model.AddBoolOr([a.Not(), b.Not(), c])
# model.AddBoolOr([a, b, c])
model.AddBoolOr([a.Not(), b, c.Not()])
model.AddBoolOr([a, b.Not(), c.Not()])
home day 1=0 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
So when you combine all four AddBoolOr constraints at once, the
first pair get rid of two cases when c==False, the second pair get
rid of two cases when c==True, and we get the truth table we want:
# eliminates conditions when c is false
model.AddBoolOr([a.Not(), b.Not(), c])
model.AddBoolOr([a, b, c])
# eliminates conditions when c is true
model.AddBoolOr([a.Not(), b, c.Not()])
model.AddBoolOr([a, b.Not(), c.Not()])
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
Why not use OnlyEnforceIf?
As I stared at the code, I thought to myself that it would be much
easier to understand if the constraint was simply written using
OnlyEnforceIf.
model.Add(a == b).OnlyEnforceIf(c)
model.Add(a != b).OnlyEnforceIf(c.Not())
This logic is pretty clear to me. It is saying that if c==True,
then a and b must be the same—both true, or both false. On the
other hand, if c==False, then a and b must be different.
So I ran that code, and lo and behold the truth table is exactly the same:
# model.AddBoolOr([a.Not(), b.Not(), c])
# model.AddBoolOr([a, b, c])
# model.AddBoolOr([a.Not(), b, c.Not()])
# model.AddBoolOr([a, b.Not(), c.Not()])
model.Add(a == b).OnlyEnforceIf(c)
model.Add(a != b).OnlyEnforceIf(c.Not())
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
So why would the example be written in terms of AddBoolOr when
OnlyEnforceIf makes the logic so much easier to understand?
What happens when just one of the constraints is on?
model.Add(a == b).OnlyEnforceIf(c)
# model.Add(a != b).OnlyEnforceIf(c.Not())
home day 1=0 home day 2=0 break=0
home day 1=0 home day 2=1 break=0
home day 1=1 home day 2=1 break=0
home day 1=1 home day 2=0 break=0
home day 1=1 home day 2=1 break=1
home day 1=0 home day 2=0 break=1
The same as the combination of the two AddBoolOr([...,c.Not()])
constraints. Similarly, just OnlyEnforceIf(c.Not()) has the same
effect as the two AddBoolOr([..,c]) constraints.
Flipping on logging shows that this is what is going on behind the
scenes somewhere. The log output for the AddBoolOr version is as
follows:
Parameters: log_search_progress: true search_branching: FIXED_SEARCH enumerate_all_solutions: true
Satisfaction model '':
Search strategy: on 1 variables, CHOOSE_FIRST, SELECT_MIN_VALUE
#Variables: 3
- 3 in [0,1]
#kBoolOr: 4 (#literals: 12)
*** starting model expansion at 0.00s
*** starting model presolve at 0.00s
- 0 affine relations were detected.
- 0 variable equivalence relations were detected.
Satisfaction model '':
Search strategy: on 1 variables, CHOOSE_FIRST, SELECT_MIN_VALUE
#Variables: 3
- 3 in [0,1]
#kBoolOr: 4 (#literals: 12)
*** starting to load the model at 0.00s
...
The output for the OnlyEnforceIf version is slightly different.
The model as stated is getting simplified by rules:
Parameters: log_search_progress: true search_branching: FIXED_SEARCH enumerate_all_solutions: true
Satisfaction model '':
Search strategy: on 1 variables, CHOOSE_FIRST, SELECT_MIN_VALUE
#Variables: 3
- 3 in [0,1]
#kLinear2: 2 (#enforced: 2)
*** starting model expansion at 0.00s
*** starting model presolve at 0.00s
- 0 affine relations were detected.
- 0 variable equivalence relations were detected.
- rule 'bool_or: removed enforcement literal' was applied 4 times.
- rule 'linear: simplified rhs' was applied 1 time.
- rule 'linear: small Boolean expression' was applied 2 times.
Satisfaction model '':
Search strategy: on 1 variables, CHOOSE_FIRST, SELECT_MIN_VALUE
#Variables: 3
- 3 in [0,1]
#kBoolOr: 4 (#literals: 12)
*** starting to load the model at 0.00s
...
The log output indicates that the enforcement literal is being replaced
by ‘bool_or’ four times, and then once it had finished up analyzing
the problem, there are 3 variables and 4 kBoolOr constraints in both
cases. So somehow, the two OnlyEnforceIf constraints are just syntactic sugar that get
boiled down to the combination of the four AddBoolOr constraints.
So I guess the lesson is to use what makes sense, and hope that the
solver can figure it out. The one caveat is that the inline
documentation for OnlyEnforceIf states contains the following
caveat:
// Important: as of September 2018, only a few constraint support enforcement:
// - bool_or, bool_and, linear: fully supported.
// - interval: only support a single enforcement literal.
// - other: no support (but can be added on a per-demand basis).