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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Adaptive Clause Management in SMT Solvers: A Dynamic Weighting Framework for Formal Verification

  • Wenda Leng,
  • Meihua Liu,
  • Yufeng Jin

摘要

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.