面向动态包含的学习
人工智能
2009-04-02 v1
摘要
本文提出了一种针对布尔合取范式公式的新的动态包含技术。该技术利用简单且充分的条件,在冲突分析过程中检测原始公式中可通过包含约简的子句。在学习子句推导过程中,以及在归结过程的每一步,我们只需检查当前归结式与原始公式中编码在蕴含图中的子句之间的反向包含。我们的方法产生了一种强大且动态的简化技术,该技术利用学习来消除原始子句中的文字。实验结果表明,将我们的动态包含方法集成到最先进的SAT求解器Minisat和Rsat中,在特定实例(尤其是手工构造的实例)上取得了显著的改进。
引用
@article{arxiv.0904.0029,
title = {Learning for Dynamic subsumption},
author = {Youssef Hamadi and Said Jabbour and Lakhdar Sais},
journal= {arXiv preprint arXiv:0904.0029},
year = {2009}
}