东北大学学报（自然科学版）

东北大学学报:自然科学版 ›› 2014, Vol. 35 ›› Issue (7): 935-938.DOI: 10.12068/j.issn.1005-3026.2014.07.006

• 信息与控制 • 上一篇    下一篇

一种求解SAT问题的动态重启策略

郭莹，张长胜，张斌   

  1. (东北大学 信息科学与工程学院， 辽宁 沈阳110819)
  • 收稿日期:2013-04-01 修回日期:2013-04-01 出版日期:2014-07-15 发布日期:2014-04-11
  • 通讯作者: 郭莹
  • 作者简介:郭莹(1979-)，女，山东泰安人，东北大学博士研究生;张斌(1964-)，男，辽宁本溪人，东北大学教授，博士生导师.
  • 基金资助:
    国家自然科学基金资助项目(61073062，61100090);中央高校基本科研业务费专项资金资助项目(N11024006);宁夏回族自治区自然科学基金资助项目(NZ13265).

An Dynamic Restart Strategy for Solving SAT Problem

GUO Ying， ZHANG Changsheng， ZHANG Bin   

  1. School of Information Science & Engineering， Northeastern University， Shenyang 110819， China.
  • Received:2013-04-01 Revised:2013-04-01 Online:2014-07-15 Published:2014-04-11
  • Contact: ZHANG Bin
  • About author:-
  • Supported by:
    -

RichHTML

0

PDF (PC)

816

摘要： 为降低冲突驱动子句学习SAT求解器的运行计算成本，从“何时重启”和“何处重启”两个角度入手，提出一种动态启发式重启策略2WSAT.该策略将冲突决策层次和变量重启次数作为反映求解状态的重要参数，及时摆脱错误的求解分支，通过重启后选择更优的决策变量提高求解性能.采用实际应用的基准测试集，与两个流行的求解器进行了对比实验.结果表明，所提出的策略对求解速度、内存占用、冲突发生数、传播次数等关键指标有显著改善.

关键词: 可满足性问题, 重启策略, 启发式, 冲突决策层次, 变量重启次数

Abstract: In order to reduce the computational costs in conflictdriven clause learning solvers， an improved adaptive heuristic restart strategy named 2WSAT was proposed， which was based on two questions including“when to restart”and“where to restart”. In this strategy， the conflict decision levels and variable’s restart times were taken as important solving state parameters， so that overall performance could be improved by escaping from wrong search branches and choosing better decision variables. Comparative experiments were conducted among 2WSAT and two modern solvers， using the practical application benchmarks. The results showed that 2WSAT has higher scores in many key indicators such as solving speed， memory usage， conflicts number， propagation number etc.

Key words: propositional satisfiability problem, restart strategy, heuristic, conflict decision level, variable’s restart times

中图分类号: