CVC4-SymBreak: Derived SMT solver at SMT Competition 2019
arxiv(2019)
摘要
We present CVC4-SymBreak, a derived SMT solver based on CVC4, and a non-competing participant of SMT-COMP 2019. Our technique exploits symmetries over the Boolean skeleton variables in an SMT problem to prune the search space. We use an ensemble of a solver with and without symmetries to be more effective. Our approach results in significantly faster solutions on a subset of available SMT benchmarks.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要