Logic models

ROOC lets you write boolean logic directly in a model. Formulas over binary variables are compiled to linear constraints automatically, so you can state properties like "at least one of these", "if this then that" or "exactly one of the two" without encoding them by hand. A model can be entirely made of logic, or mix logic with ordinary linear constraints.

The operators

Every operator also has a symbolic alias, use whichever you prefer:

• and &&: true when both operands are true
• or ||: true when at least one operand is true
• not !: negation
• xor: true when exactly one operand is true
• implies ->: false only when the left side is true and the right side is false
• iff <->: true when both sides have the same value

The literals true and false are also available. Operands must be binary: Boolean variables, or expressions whose value is 0 or 1. Use parentheses to group formulas.

Logic constraints

A constraint that consists of a logic formula alone is an assertion: the formula must be true in every solution. There is no need to write a comparison, although the explicit form ... = true is accepted and means the same thing. The for iteration works exactly like in ordinary constraints. This is a full model for the vertex cover problem:

Assertions compile to compact rows whenever possible: each x_u or x_v above becomes the single linear constraint x_u + x_v >= 1, without any auxiliary variable.

Logic blocks

Like sum and avg, logic has its own expansion blocks: all { } is the conjunction of a list of formulas, any { } is the disjunction, and xor { } chains exclusive disjunctions. They also exist in the scoped form, for example any(v in nodes(G)) { x_v } is the disjunction over all nodes. Combined with assertions, a set of logic requirements reads almost like a specification:

Here solve is used instead of an objective: the solver only needs to find any assignment that satisfies the formulas, like a small SAT problem.

Logic as values

A logic formula can also be used inside arithmetic, where it counts as 1 when true and 0 when false. This makes counting satisfied conditions natural. The following model maximizes the number of satisfied clauses, a MAX-SAT instance:

When a formula is used as a value, the compiler introduces one auxiliary binary variable for it, tied to the operands by linear constraints, so the compiled model is still an ordinary mixed integer linear model.

Mixing logic and linear constraints

Logic constraints and linear constraints can share the same variables. A common pattern is to use Boolean variables both in formulas, to express decisions, and in linear constraints, to gate quantities. Booleans used in arithmetic count as 0 or 1 just like formulas do:

Here x <= 10 * open_1 forces production to zero when the facility is closed, while open_1 xor open_2 is a purely logical requirement on the same decision variables. The best solution opens one facility and produces 10 units there.

For complete models using logic, including a dominating set problem written both ways, see the examples page.