基于扩展规则的启发式#SAT求解算法

作者：王强; 刘磊; 吕帅^*

来源：软件学报, 2018, 29(11): 3517-3527.

DOI：10.13328/j.cnki.jos.005298

• 扩展规则
• 模型计数
• 启发式算法
• 极大项空间
• 规约子句

#SAT在人工智能领域取得了广泛应用,很多现实问题可以规约成#SAT进行求解,得到命题理论的模型个数.通过对基于扩展规则的#SAT求解器的深入研究,发现选择规约子句的顺序对极大项空间的大小有着较大的影响,因此提出两种加速#SAT求解的启发式策略:MW和LC&MW.MW每次选择具有最大权值的子句作为规约子句;LC&MW每次选择最长子句作为规约子句,若最长子句存在多个,则在多个最长子句中选择具有最大权值的子句作为规约子句.利用MW策略设计了算法CERMW,利用LC&MW策略设计了算法CERLC&MW.实验结果表明,CERMW和CERLC&MW相对于先前的#SAT求解算法在求解效率和求解能力上都有显著的提高.在求解效率方面,CERMW和CERLC&MW的求解速度是其他算法的1.4倍100倍.在求解能力方面,CERMW和CERLC&MW在限定时间内可解的测试用例更多.

• 单位
  吉林大学