A circuit-based SAT solver that operates directly on AIG (And-Inverter Graph) representations, using circuit-aware reasoning with AIGER format support for hardware verification and combinational equivalence checking.