基于反例引导扩展的QBF求解
计算机科学中的逻辑
2018-07-30 v4 人工智能
摘要
我们引入了反例引导归纳综合（CEGIS）的一种新颖推广，并将其实例化以产生一种求解量化布尔公式（QBF）的新颖且具有竞争力的算法。当前基于反例引导扩展的QBF求解器采用递归方法，其随量词交替次数的增加扩展性差。我们对CEGIS的推广消除了对这种递归方法的需求，并将其实例化以产生一种简单高效的QBF求解算法。最后，本研究得到了该算法的一个具有竞争力但直接的实现的支持，使得研究我们算法设计决策的实际影响以及各种优化成为可能。
引用
@article{arxiv.1611.01553,
title = {QBF Solving by Counterexample-guided Expansion},
author = {Roderick Bloem and Nicolas Braud-Santoni and Vedad Hadzic},
journal= {arXiv preprint arXiv:1611.01553},
year = {2018}
}
备注
This is a **very** old version of the paper arXiv:1807.08964 and should be taken down. I did not know you could just replace papers, and did not know whether I could change authors and similar, so that is why I made a different submission. Please take it down