Vijay Ganesh

In Proceedings of the 26 th international conference on principles and practice of constraint programming (CP’20)

Abstract In this paper, we present a machine learning based splitting heuristic for divide-and-conquer parallel Boolean SAT solvers. Splitting heuristics, whether they are look-ahead or look-back, are designed using proxy metrics, which when optimized, approximate the true metric of minimizing solver runtime on sub-formulas resulting from a split. The rationale for such metrics is that they have been empirically shown to be excellent proxies for runtime of solvers, in addition to being cheap to compute in an online fashion.

Community and LBD-based clause sharing policy for parallel SAT solving

By Vincent Vallade, Ludovic Le Frioux, Souheib Baarir, Julien Sopena, Vijay Ganesh, Fabrice Kordon

2020-06-01

In Proceedings of the 23rd international conference on theory and applications of satisfiability testing (SAT’20)

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.

A machine learning based splitting heuristic for divide-and-conquer solvers

Community and LBD-based clause sharing policy for parallel SAT solving

Search

Tags