Tuning SAT solvers for LTL Model Checking
Anissa Kheireddine, Étienne Renault, Souheib Baarir · 2022
Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli [33] that classmes any property expressed through Linear-time Temporal Logic (LTL). By combining these two information with the classical Literal Block Distance (LBD) measure [46], we designed a new heuristic, well suited for solving BMC problems. In particular, our work identifies and exploits a new set of relevant (learnt) clauses. We experiment with these ideas by developing a tool dedicated for SAT-based LTL BMC solvers, called BSaLTic. Our experiments over a large database of BMC problems, show promising results. In particular, BSaLTic provides good performance on UNSAT problems. This work highlights the importance of considering the structure of the underlying problem in SAT procedures.