结合Riss的基于Lazy框架的SMT求解技术

摘要

SMT涉及很多相关的理论,并且可以描述很多SAT不能描述的问题。因此,对SMT求解器的研究有非常重要的意义。文章提出了另一种求解SMT问题的方法。首先,编译SMT公式并转换为命题变量的合取范式;然后借鉴了在2014SAT竞赛中的Riss求解算法,得到一个的可满足的一组赋值;最后把得当前解与理论求解器进行交互并且验证与在特定理论背景下的可满足性。由于在SMT的求解的过程中结合了先进的Riss求解算法,因此在求解某些SMT问题的时候效果比较好。