Enhance SAT conflict analysis for model checking
Minge Jing, Gengshen Chen, Wenbo Yin, Dian Zhou · 2009
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.