Enhance SAT Conflict Analysis for Model Checking

摘要：

Bounded model checking shows that satisfiability (SAT) problem can be widely used for model checking. The performance of SAT solver depends heavily on the quality of the learnt clauses in the conflict analysis process.Combining with the characters of model checking,we propose to add efficient implied clauses to the clause database to enhance the conflict analysis.Experimental results show that the average running time of our algorithm is reduced by 35% compared with the traditional FUIP algorithm.

关键词： Model checking Satisfiability problem Implication graph Conflict analysis

作者: Ming-e Jing Gengshen Chen Wenbo Yin Dian Zhou

作者单位: State Key Laboratory of ASIC & System,Fudan University,Shanghai,China Electrical Engineering Department,University of Texas at Dallas,Richardson,TX 75083-0688 USA

会议类型: 国际会议

会议名称: 2009 IEEE 8th International Conference on ASIC(第八届IEEE国际专用集成电路大会)

会议地点: 长沙

会议语种:英文

页码: 686-689

在线出版日期: 2009-10-20（万方平台首次上网日期，不代表论文的发表时间）