Combinational equivalence checking (CEC) is essential for verifying the correctness of circuit designs. With the growing complexity of circuits, effective verification techniques have become increasingly critical. Recently, a conjunctive normal form (CNF)-based approach, converting circuits to CNF for Boolean satisfiability (SAT) solvers, has shown competitive performance compared to state-of-the-art hybrid SAT sweeping approaches. The capability of this CNF-based approach depends on effective CNF conversion. This work presentsCirOPT, which is the first CNF conversion method using compiler optimization to equivalently simplify circuits. Extensive experiments are conducted on a broad range of real-world benchmarks, which are far more than the number of benchmarks typically used in empirical studies. The results reveal that, when paired with the state-of-the-art CNF SAT solverKissat,CirOPTconsiderably outperforms existing approaches in CEC.

Satisfiability Modulo Theories (SMT) plays a critical role in various software engineering applications, including program verification, symbolic execution, and automated test generation. Over the years, a wide range of SMT solvers has been developed, typically designed for general purposes or tailored to specific background theories, such as bit-vectors or nonlinear arithmetic. Due to the diversity and complexity of SMT instances, no single solver consistently outperforms others across all problem domains. This motivates the need for algorithm selection strategies that can adaptively choose solvers based on the characteristics of the instances.To overcome the limitations of single-solver selection, solving SMT as a scheduling problem, enabling a more fault-tolerant and effective use of multiple solvers in sequence. We model algorithm scheduling as a hyperparameter optimization problem, enabling efficient black-box search over solver sequences while treating the dataset as a whole, thus achieving globally optimized and robust scheduling strategies. The resulting scheduler called SMTgazer. To further enhance scheduling efficiency and solver performance, we propose two optimizations: leveraging unsupervised X-means clustering to create semantically coherent instance groups for localized model training, and augmenting the Bayesian optimization surrogate with boosting and bagging ensembles to improve generalization and mitigate overfitting, thereby yielding more reliable performance predictions for the sequential portfolio scheduler.Extensive experiments are conducted to evaluate the performance of SMTgazer, utilizing six SMT benchmarks derived from real-world applications. It shows that our approach consistently outperforms current state-of-the-art methods. Particularly, SMTgazer achieves a 44.65% reduction in PAR-2 score and 69.11% decrease in the number of unsolved instances, compared to the strongest competitor, Sibyl, demonstrating the effectiveness of formulating SMT algorithm scheduling as a hyperparameter optimization problem. We further analyze the generated scheduling sequences to uncover the design principles that explain the success of our method. Finally, we also empirically show that our approach is both robust and generalizable, and the proposed strategies are effective.