赞
踩
It use ALLSAT approach to perform existential quatification. And use increamental SAT to reduce the run time overhead.
But I think the major innovation is to use sorting network to find out the shortest prime clause. This is bettern than my approach in VMCAI05: Minimizing Counterexample with Unit Core Extraction and Incremental SAT, which reduce the size of a block clause by iteratively remove those literal not in the support set of a proof.
Copyright © 2003-2013 www.wpsshop.cn 版权所有,并保留所有权利。