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
    Mar 12 at 7:07
  • $\begingroup$ Can you say a bit more about what is happening during presolve? $\endgroup$
    – Hanno
    Mar 12 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
    Mar 12 at 16:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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