CirSAT: An Efficient Circuit-based SAT Solver via Fanout-driven Decision Heuristic

Circuit-based Boolean satisfiability (SAT) solver is efficient for solving electronic design automation (EDA) problems. Compared to widely-used conjunctive normal form (CNF)based SAT solvers, circuit-based SAT is rarely publicly available. In this paper, we propose an open-source circuit-based SAT solver, CirSAT, which implements several efficient SAT algorithms directly on circuits. In particular, we make use of the fanout of logic gates as a heuristic to guide conflict decision. Experimental results on ISCAS’85 benchmark suites indicate our method achieves 47.7x (upto 267. 8x) CPU time acceleration and saves 18.9x time compared to MiniSAT.