Exploiting Dynamically Propositional Logic Structures in SAT

Jingchao Chen

The 32-bit hwb (hwb-n32 for short) problem is from equivalence checking that arises in combining two circuits computing the hidden weighted bit function. Since 2002, it remains sti…