通过少量简单预言机查询计算极大自洽赋值
计算机科学中的逻辑
2016-04-06 v2 离散数学
数据结构与算法
摘要
我们考虑为子句集F计算极大自洽赋值（autarky）的算法任务，即一个部分赋值，它满足其所触及的F的每条子句，且若添加任意非空进一步赋值集合则会破坏此性质。我们采用SAT求解器作为预言机，利用其多种能力。使用标准SAT预言机时，log_2(n(F))次预言机调用即足够，其中n(F)为变量数，但缺点是使用了（转换后的）基数约束，这使得该方法在实践中效率较低。利用受现代SAT求解器能力启发的扩展SAT预言机，我们展示了如何通过2 n(F)^{1/2}次更简单的预言机调用来计算极大自洽赋值。这一新算法结合了先前两种主要方法，分别基于自洽-消解对偶性与SAT转换。
引用
@article{arxiv.1505.02371,
title = {Computing maximal autarkies with few and simple oracle queries},
author = {Oliver Kullmann and Joao Marques-Silva},
journal= {arXiv preprint arXiv:1505.02371},
year = {2016}
}
备注
18 pages; second version with editorial changes, to appear in LNCS for Theory and Applications of Satisfiability Testing - SAT 2015