Counters in SAT

Here's a visualization of a SAT formula of a BooleanCountingFunction. Four circles in the middle are the variables of interest. Five circles on the periphery are variables encoding the number of true assignments of the four circles in the middle. Squares are clauses, and color of the edge indicates whether the variable is negated in that clause. You can see from the color that rightmost circle represents "all variables are true" and leftmost circle represents "all variables are false".



Notebook