50.002 2D Challenge 2018

Design challenge for the 50.002 module for fastest 2-SAT solver (Java) and the best performance-area ratio for a 32-bit adder (JSim).

Base Hybrid Han-Carlson architecture is commercially used in adder modules of early 32-Bit Intel Pentium 4 CPUs.
Hybridisation of Brent-Kung (Top & Bottom) and Koggle-Stone (Middle) architectures in an alternating design for the Carry Chain Computation stage.
4-Step Pipe-Lining of White Cell inputs using double inverting arrays (higher fidelity than buffers) for efficient signal distribution via instruction-level parallelism at Pre-Processing stage.
Overhaul of standard White, Grey, and Black Cell definitions with full inverting logic & AND-OR-INVERT (AOI21) implementation for lower overall transitor count at MOSFET level.
Exhaustive approach for buffering signals between cells using gradient descent for efficient load distribution.
Enhanced Post-Processing stage with 4-to-1 cascading design with full inverting logic & AOI21 implementation.
Selective revision of White cell definitions to non-inverting logic based on usage frequency per operation.

Radix-2 and/or Radix-4 redesign of the Carry Chain Computation stage to reduce fan-out with sparseness.
Hybridisation with Lynch–Swartzlander quaternary logic spanning tree adder architecture.

Algorithm based on Papadimitriou's Random Walk approach to boolean satisfiability.
Relaxed boolean satisfiability problem to solve 2-SAT only.
Further relaxation of 2-SAT problem to solve Ripple-Carry Adder verification based on S8 Satisfiability property (Standard test case used to time solver).
Optimisation of otherwise O(n^2) standard inner/outer loops to O(log log n) for solving standard test cases to achieve best solver time at the cost of logic completeness.
Random element of solver results in variance of solver timings. Average timing is recommended. Else, cherry-pick shortest single-run timings.
Solver guaranteed to return accurate results for large relaxed test cases only. Revert to standard loops for generic test cases.

Dynamic switching of loops based on test cases for logic completeness.
Memomisation and decorators to speed up boolean flip calls at each random walk step.
Usage of advanced (pseudo) random number generators like Xoroshiro128+ with direct sign testing for random booleans instead of conditionals with the default random package.
Decrement to zero while loops and other micro-optimisations.

ed-ke/50-002_2D_Challenge_2018