| labeling/1 | Enumerate concrete solutions. |
| random_labeling/2 | Select a single random solution. |
| sat/1 | True iff Expr is a satisfiable Boolean expression. |
| sat_count/2 | Count the number of admissible assignments. |
| taut/2 | Tautology check. |
| weighted_maximum/3 | Enumerate weighted optima over admissible assignments. |