Reading a CP-SAT Solver Log

When CP-SAT solves a model, it prints a structured log with four sections: a model summary, a presolve report, a stream of search-progress lines, and a final response. Reading each section tells us how the solver transformed the problem and how close to optimal the returned solution is.

The model summary enumerates variables and constraints. A typical block reads:

$$\texttt{Initial model:}$$ $$\texttt{\#Variables: 1200 (\#bools: 400 \#ints: 800)}$$ $$\texttt{\#kLinear2: 600}$$ $$\texttt{\#kAllDiff: 25}$$ $$\texttt{\#kIntervalVar: 50}$$

• $\texttt{\#Variables}$ counts decision variables. $\texttt{\#bools}$ are $0/1$ variables; $\texttt{\#ints}$ are integer variables with a finite domain.
• Lines beginning with $\texttt{\#k}\ldots$ count constraints by kind. $\texttt{kLinear2}$ is a linear constraint with two terms, $\texttt{kAllDiff}$ is an all-different constraint, $\texttt{kIntervalVar}$ is an interval variable used in scheduling.

The presolve report follows, listing the simplified model:

$$\texttt{Presolved model:}$$ $$\texttt{\#Variables: 500 (\#bools: 200 \#ints: 300)}$$ $$\texttt{\#kLinear2: 250}$$

The number of variables (or constraints of each kind) eliminated by presolve is the initial count minus the presolved count. Here, presolve removed $1200 - 500 = 700$ variables and $600 - 250 = 350$ linear-2 constraints. Smaller presolved models generally search faster.