The last assignment should not win

A layout loop sets left from width, then width from right, then revises left when a preference fails. Reordering statements changes the result even though the desired relationships are simultaneous: left plus width equals right; width is nonnegative; a preferred width yields to required bounds.

Constraint variables and relations form the carrier; adding a relation narrows the feasible set. A solver returns an assignment or a typed explanation of infeasibility. Boolean decision diagrams similarly represent a bounded Boolean function by ordered decisions and shared residual subproblems.

Restriction buys decidability. Linear arithmetic has procedures that a general user-defined programming language does not. Fixed variable order gives a reduced decision diagram a canonical form. Adding arbitrary code to a policy language discards these guarantees.

Where the model stops

Two transparent formulas do not justify a solver. Constraints also need an explicit policy for conflicting preferences and numerical precision. Never hide unbounded search behind a timeout; state variable, node, and step budgets and return exhaustion as an explanatory result.

Lessons

• Simultaneous relations should not inherit source order.
• A bounded language purchases termination and analysis.
• Canonical decision forms need a fixed variable order.
• Small direct calculations may be the deeper interface.

Practice

1. Rewrite a three-branch layout rule as equations and inequalities.
2. Distinguish required constraints from preferences.
3. Transfer the model to feature compatibility or scheduling.

A solver can return an answer. The next chapter makes the derivation travel with it.

References

1. “Alan Borning et al., Cassowary papers and implementation archive.” — incremental linear constraints for interfaces.
2. “Randal Bryant, “Graph-Based Algorithms for Boolean Function Manipulation” resources.” — ordered decision diagrams and canonical representation.