Tuning SAT Solvers for LTL Model Checking

Authors

Anissa Kheireddine, Étienne Renault, Souheib Baarir

Where

Proceedings of the 29th Asia-Pacific Software Engineering Conference (APSEC'22)

Type

inproceedings

Publisher

IEEE

Projects

Spot

Date

2022-12-09

Abstract

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 that classifies any property expressed through Linear-time Temporal Logic (LTL). By combining these two information with the classical Literal Block Distance (LBD) measure, 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.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  kheireddine.22.apsec,
  author	= {Anissa Kheireddine and \'Etienne Renault and Souheib
		  Baarir},
  title		= {Tuning {SAT} Solvers for {LTL} Model Checking},
  booktitle	= {Proceedings of the 29th Asia-Pacific Software Engineering
		  Conference (APSEC'22)},
  year		= {2022},
  pages		= {259--268},
  volume	= {???},
  publisher	= {IEEE},
  month		= dec,
  abstract	= {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 that classifies any property expressed
		  through Linear-time Temporal Logic (LTL). By combining
		  these two information with the classical Literal Block
		  Distance (LBD) measure, 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. },
  doi		= {10.1109/APSEC57359.2022.00038}
}