  Effective formulation of problems into Conjunctive Normal Form (CNF) is
critical in modern Boolean Satisfiability (SAT) solving for optimizing solver
performance. Addressing the limitations of existing methods, our Electronic
Design Automation (EDA)-driven preprocessing framework introduces a novel
methodology for preparing SAT instances, leveraging both circuit and CNF
formats for enhanced flexibility and efficiency. Central to our approach is the
integration of a new logic synthesis technique, guided by a reinforcement
learning agent, and a novel cost-customized LUT mapping strategy, enabling
efficient handling of diverse SAT challenges. By transforming the SAT
competition benchmarks into circuit instances, our framework demonstrates
substantial performance improvements, as evidenced by a 52.42% reduction on
average compared to solving directly. Moreover, our framework achieves a
remarkable 96.14% runtime reduction on average for a set of logic equivalence
checking problems that exhibit inherent circuit structures. These results
highlight the effectiveness and versatility of our approach in handling both
CNF and circuit instances. The code is available at
https://github.com/cure-lab/EDA4SAT.
