关于永久存储学习子句的实验研究
人工智能
2021-10-28 v1 计算机科学中的逻辑
摘要
现代CDCL SAT求解器快速学习子句，而一个重要的启发式方法是子句删除方案。当前大多数求解器有两个（或更多）子句存储区。一个存储“有价值”的、永不被删除的子句。大多数学习到的子句被加入另一个存储区，并采用激进的删除策略以限制其大小。MapleSAT系列近期的求解器具有相对复杂的删除方案，并且表现良好。许多求解器仅永久存储二元子句，但MapleLCMDistChronoBT永久存储具有小LBD的子句。我们报道了对MapleLCMDistChronoBT中永久子句存储区的实验研究。我们观察到该存储区可能变得相当大，但几种限制其大小的方法都降低了性能。我们还表明，基于交替的大小和LBD准则可提升性能，同时仍保持较大的永久存储区。具体而言，保存大小不超过8的子句，并添加少量高中心性子句，均改善了性能，且同时使用两种方法时改善最佳。
引用
@article{arxiv.2110.14187,
title = {An Experimental Study of Permanently Stored Learned Clauses},
author = {Sima Jamali and David Mitchell},
journal= {arXiv preprint arXiv:2110.14187},
year = {2021}
}