Module signal_design 

Conflict-free traffic-signal PHASE DESIGNER (certified SAT synthesis).

Grouping intersection movements into green phases so no two conflicting movements ever share a phase is exactly graph k-colouring — a SAT problem. We encode it as a boolean ProofExpr and discharge it with the project’s own certified solver (logicaffeine_proof::sat), never Z3:

• a feasible plan is a SAT model (a witness that is trivially re-checkable), and
• the claim “fewer phases is impossible” is a prove_unsat Refuted result, which is RUP-certified — so the minimality of the plan is certified, not merely asserted.

The English frontend is a focused grammar (“X conflicts with Y, Z and …”) rather than the general FOL pipeline, so the designer is robust independent of that surface.

Structs

Intersection

An intersection: a set of movements and the pairs that may not be green together.

PhasePlan

A synthesized signal plan: each movement assigned to a green phase.

Functions

design_from_spec

Parse an English spec into an Intersection, then design its minimal plan.

design_phase_plan

Design the minimal-phase conflict-free plan for an intersection, or None if it has no movements.

is_valid_coloring

Re-check that a plan is a genuine conflict-free colouring (used by tests and as a guard).

parse_intersection

Parse a focused English spec into an Intersection.