资源论文Predicting Learnt Clauses Quality in Modern SAT Solvers

Predicting Learnt Clauses Quality in Modern SAT Solvers

2019-11-15 | |  71 |   47 |   0

Abstract Beside impressive progresses made by SAT solvers over the last ten years, only few works tried to understand why Conflflict Directed Clause Learning algorithms (CDCL) are so strong and effificient on most industrial applications. We report in this work a key observation of CDCL solvers behavior on this family of benchmarks and explain it by an unsuspected side effect of their particular Clause Learning scheme. This new paradigm allows us to solve an important, still open, question: How to designing a fast, static, accurate, and predictive measure of new learnt clauses pertinence. Our paper is followed by empirical evidences that show how our new learning scheme improves state-of-the art results by an order of magnitude on both SAT and UNSAT industrial problems

上一篇:On Solving Boolean Multilevel Optimization Problems

下一篇:Online Stochastic Optimization in the Large: Application to Kidney Exchange

用户评价
全部评价

热门资源

  • The Variational S...

    Unlike traditional images which do not offer in...

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • A Mathematical Mo...

    Direct democracy, where each voter casts one vo...

  • Rating-Boosted La...

    The performance of a recommendation system reli...