3
$\begingroup$

The solver API for CP-SAT offers the attribute NumBooleans, which is documented as "Returns the number of boolean variables managed by the SAT solver".

Excuse my ignorance, but why is this a property of the solution rather than the model itself? Should I think about the solver as applying some simplifying preprocessing steps to the model, and the number indicating the complexity of the model after that, or what is the right mental model here?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
$\begingroup$

This does not count Boolean variables in the model. It counts Boolean variables in the SAT solver. This is vastly different. Presolve is happening, some constraints are expanded, search and conflicts create Boolean variables. It differs even among workers solving the same model.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks! It sounds like when creating statistics about the relation between problem size and solver time, NumBooleans would be a useful measure to take into account as well. $\endgroup$
    – Hanno
    Commented Mar 12, 2023 at 7:07
  • $\begingroup$ Can you say a bit more about what is happening during presolve? $\endgroup$
    – Hanno
    Commented Mar 12, 2023 at 7:42
  • 2
    $\begingroup$ a bit complex. Presolve is 17k lines of code. Three things happen in presolve: (a) constraint simplification/rewriting, domain reduction, and constraint expansion. One particularity of CP-SAT is constraint expansion. A lot of CP constraints, and sometimes a linear constraints are expanded. Domains of integer variables can be rewritten as an array of Boolean variables. In all these cases, new Boolean variables are introduced. $\endgroup$
    – Laurent Perron
    Commented Mar 12, 2023 at 16:56

Not the answer you're looking for? Browse other questions tagged or ask your own question.