A machine learning based splitting heuristic for divide-and-conquer solvers
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.