• 中国计算机学会会刊
  • 中国科技核心期刊
  • 中文核心期刊

计算机工程与科学

• 高性能计算 • 上一篇    下一篇

基于频次的SAT问题学习子句混合评估算法

吴贯锋1,2,徐扬2,3,陈青山1,2,何星星2,3,常文静1,2   

  1. (1.西南交通大学信息科学与技术学院,四川 成都 610031;
    2.西南交通大学系统可信性自动验证国家地方联合工程实验室,四川 成都 610031;
    3.西南交通大学数学学院,四川 成都 610031)

     
  • 收稿日期:2018-08-13 修回日期:2018-11-08 出版日期:2019-08-25 发布日期:2019-08-25
  • 基金资助:

    国家自然科学基金(61673320);中央高校基本科研业务费专项资金(2682017ZT12,2682018ZT10,2682018CX59,2682018ZT25)

A hybrid learnt clause evaluation algorithm
for SAT problem based on frequency

WU Guan-feng1,2,XU Yang2,3,CHEN Qing-shan1,2,HE Xing-xing2,3,CHANG Wen-jing1,2   

  1. (1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610031;
    2.National-Local Joint Engineering Laboratory of System Credibility Automatic Verification,
    Southwest Jiaotong University,Chengdu  610031;
    3.School of Mathematics,Southwest Jiaotong University,Chengdu 610031,China)
  • Received:2018-08-13 Revised:2018-11-08 Online:2019-08-25 Published:2019-08-25

摘要:

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器(GLUCOSE 4.1并行版本)为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。

关键词: SAT问题, 并行求解器, LBD, GLUCOSE

Abstract:

In order to effectively manage learnt clauses, avoid a geometrical growth of their scale, reduce the memory cost of redundant learnt clauses and improve the efficiency of the Boolean satisfiability problem (SAT) solver, we need to evaluate learnt clauses and delete some redundant ones. Traditional evaluation methods are based on the length of learnt clauses, and short-length ones are kept. Two current mainstream clause evaluation methods are the variable state independent decaying sum (VSIDS), and a method based on the evaluation of the literals blocks distance (LBD), and the combination of the above two is also used as the basis for clause evaluation. We analyze the relationship between the number of learnt clauses used in conflict analysis and problem solving, and combine the frequency of learnt clauses with the LBD evaluation algorithm, which not only reflects the role of learnt clauses in conflict analysis, but also makes full use of the information between text and decision-making layer. Taking the Syrup solver (GLUCOSE 4.1 parallel version) as baseline, experiments are carried out to evaluate the algorithm and the parallel clause sharing strategy. The experimental comparison shows that the the proposed hybrid evaluation algorithm outperforms the LBD evaluation algorithm, and the number of solving problems is significantly increased.
 

Key words: SAT problem, parallel solver, LBD, GLUCOSE