Boolean Variables and Clauses in CP-SAT

Boolean variables in CP-SAT are integer variables restricted to the domain {0, 1}. This lesson introduces Boolean variables and their negated literals, then builds up the core CP-SAT clause types (AddBoolOr, AddBoolAnd, AddAtMostOne, AddExactlyOne, AddImplication) and shows how to combine them to model logical conditions.

Step 1 of 157%

Tutorial

Boolean Variables and Literals

In CP-SAT, a Boolean variable is an integer variable whose domain is restricted to $\{0, 1\}$ . We create one with the call

b = \texttt{model.NewBoolVar("b")}.

The value $1$ represents true and the value $0$ represents false.

Every Boolean variable $b$ has an associated negated literal, written $\texttt{b.Not()}$ , whose value is

\texttt{b.Not()} = 1 - b.

So if $b = 1$ , then $\texttt{b.Not()} = 0$ ; if $b = 0$ , then $\texttt{b.Not()} = 1$ .

A literal is either a Boolean variable or its negation. All of the clauses introduced in this lesson take lists of literals as arguments.

For example, if $a = 1$ and $c = 0$ , the literals

a,\qquad c, \qquad \texttt{a.Not()},\qquad \texttt{c.Not()}

have values $1,\ 0,\ 0,\ 1$ respectively.