Lesson 2

A working encoding can be strengthened without changing its solutions. Examples include forbidding unused gates, ordering commutative predecessors, requiring every non-output gate to feed a later gate, and excluding operations that ignore one predecessor. These constraints remove multiple descriptions of essentially the same circuit.

Symmetry breaking should be justified carefully: a constraint is safe only if every equivalence class of circuits retains at least one representative. An aggressive but incorrect constraint may turn a satisfiable synthesis instance into an unsatisfiable one.