1. Deterministic clock speeds.
2. Loadable formula registers.
3. Single cycle parallel implication/transmission.
4. Scalable (linear) design.
5. Heuristic clause evaluation.
