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

Computer Engineering & Science

Previous Articles     Next Articles

A clause-based dynamical necessary
literal checking SAT solver

CHANG Wenjing1,2,XU Yang2   

  1. (1.School of Information Science and Technology,Southwest Jiaotong University,Chengdu 610036;
    2.NationalLocal Joint Engineering Laboratory of System Credibility Automatic Verification,
    Southwest Jiaotong University,Chengdu 610036,China)
     
     
  • Received:2017-12-25 Revised:2018-04-11 Online:2019-02-25 Published:2019-02-25

Abstract:

Necessary literal checking is an important preprocessing technique. by learning clauses, this paper proposes a clausebased dynamical necessary literal checking strategy (CNL) used in the solving process, and designs a lowcost data structure.  We implement two solvers, Glucose_PRE and Glucose_CNL. The former adopts the necessary literal checking as the preprocessing technique at the beginning of the solving process, and the latter implements the proposed clausebased dynamical necessary literal checking strategy. Experimental results show that the Glucose_CNL solves more instances with less time than the Glucose_PRE and Glucose 3.0 when solving the applicationtype instances in 2015 and 2016 SAT competitions, demonstrating the significance of the proposed strategy and data structure.

 

Key words: satisfiability problem, preprocessing technique, necessary literal, data structure