Towards Better Heuristics for Solving Bounded Model Checking Problems

From LRDE

Abstract

This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics. We extend these study and applied the above methodology on parallel approaches, especially to refine the sharing measure which shows promising results.

Documents

Bibtex (lrde.bib)

@Article{	  kheireddine.22.constraints,
  author	= {Anissa Kheireddine and \'Etienne Renault and Souheib
		  Baarir},
  title		= {Towards Better Heuristics for Solving Bounded Model
		  Checking Problems},
  journal	= {Constraints},
  editor	= {Mark Wallace},
  series	= {Leibniz International Proceedings in Informatics
		  (LIPIcs)},
  year		= {2023},
  pages		= {45--66},
  volume	= {28},
  publisher	= {Springer},
  month		= mar,
  abstract	= {This paper presents a new way to improve the performance
		  of the SAT-based bounded model checking problem on
		  sequential and parallel procedures by exploiting relevant
		  information identified through the characteristics of the
		  original problem. This led us to design a new way of
		  building interesting heuristics based on the structure of
		  the underlying problem. The proposed methodology is generic
		  and can be applied for any SAT problem. This paper compares
		  the state-of-the-art approaches with two new heuristics for
		  sequential procedures: Structure-based and Linear
		  Programming heuristics. We extend these study and applied
		  the above methodology on parallel approaches, especially to
		  refine the sharing measure which shows promising results.},
  doi		= {10.1007/s10601-022-09339-8},
  note		= {First published online on 27 December 2022.}
}