Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification
摘要
This paper introduces a novel dynamic weighting framework for clause management in Satisfiability Modulo Theories (SMT) solvers. By employing real-time metric adaptation, the proposed framework circumvents the limitations of conventional evaluation criteria. The core contribution lies in a phase-aware weight calibration strategy that dynamically aligns conflict pattern characteristics with optimal combinations of evaluation metrics. Experimental evaluations, including integration with Yices2, demonstrate solving speed enhancements of up to 97.67% and 119.80% compared to conventional approaches in Yices2 across three SMT-COMP benchmark sets. Furthermore, the proposed framework exhibits exceptional performance in real-world scenarios, particularly for the formal verification of circuit designs. Overall, this dynamic weighting framework significantly improves solver adaptability to evolving search space characteristics, thereby offering substantial benefits for formal circuit verification.