Community and LBD-based Clause Sharing Policy for Parallel SAT Solving

From LRDE

Abstract

Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as "the problem of identifying high-quality learnt clauses" that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term "high-quality clauses" is often defined in terms of metrics that solver designers have identified over years of empirical study. Some of the more well-known metrics to identify high-quality clauses for sharing include clause lengthliteral block distance (LBD), and clause usage in propagation. In this paper, we propose a new metric aimed at identifying high-quality learnt clauses and a concomitant clause-sharing policy based on a combination of LBD and community structure of Boolean formulas. The concept of community structure has been proposed as a possible explanation for the extraordinary performance of SAT solvers in industrial instances. Hence, it is a natural candidate as a basis for a metric to identify high-quality clauses. To be more precise, our metric identifies clauses that have low LBD and low community number as ones that are high-quality for applications such as verification and testing. The community number of a clause C measures the number of different communities of a formula that the variables in C span. We perform extensive empirical analysis of our metric and clause-sharing policy, and show that our method significantly outperforms state-of-the-art techniques on the benchmark from the parallel track of the last four SAT competitions.

Documents

Bibtex (lrde.bib)

@InProceedings{	  vallade.20.sat,
  author	= {Vincent Vallade and Ludovic {Le Frioux} and Souheib Baarir
		  and Julien Sopena and Vijay Ganesh and Fabrice Kordon},
  title		= {Community and {LBD}-based Clause Sharing Policy for
		  Parallel {SAT} Solving},
  booktitle	= {Proceedings of the 23rd International Conference on Theory
		  and Applications of Satisfiability Testing (SAT'20)},
  year		= 2020,
  month		= jun,
  volume	= {12178},
  pages		= {11--27},
  series	= {Lecture Notes in Computer Science},
  publisher	= {Springer, Cham},
  abstract	= {Modern parallel SAT solvers rely heavily on effective
		  clause sharing policies for their performance. The core
		  problem being addressed by these policies can be succinctly
		  stated as "the problem of identifying high-quality learnt
		  clauses" that when shared between the worker nodes of
		  parallel solvers results in improved performance than
		  otherwise. The term "high-quality clauses" is often defined
		  in terms of metrics that solver designers have identified
		  over years of empirical study. Some of the more well-known
		  metrics to identify high-quality clauses for sharing
		  include clause length, literal block distance (LBD), and
		  clause usage in propagation. In this paper, we propose a
		  new metric aimed at identifying high-quality learnt clauses
		  and a concomitant clause-sharing policy based on a
		  combination of LBD and community structure of Boolean
		  formulas. The concept of community structure has been
		  proposed as a possible explanation for the extraordinary
		  performance of SAT solvers in industrial instances. Hence,
		  it is a natural candidate as a basis for a metric to
		  identify high-quality clauses. To be more precise, our
		  metric identifies clauses that have low LBD and low
		  community number as ones that are high-quality for
		  applications such as verification and testing. The
		  community number of a clause C measures the number of
		  different communities of a formula that the variables in C
		  span. We perform extensive empirical analysis of our metric
		  and clause-sharing policy, and show that our method
		  significantly outperforms state-of-the-art techniques on
		  the benchmark from the parallel track of the last four SAT
		  competitions.}
}