资源论文An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)1

An Improved Separation of Regular Resolution from Pool Resolution and Clause Learning (Extended Abstract)1

2019-11-11 | |  58 |   42 |   0
Abstract We establish the unexpected power of conflict driven clause learning (CDCL) proof search by proving that the sets of unsatisfiable clauses obtained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. We further show that, under the correct heuristic choices, these refutations can be carried out in polynomial time by CDCL proof search without restarts, even when restricted to greedy, unitpropagating search. The guarded graph tautologies had been conjectured to separate CDCL without restarts from resolution; our results refute this conjecture.

上一篇:Twitter-Based User Modeling for News Recommendations

下一篇:The Complexity of One-Agent Refinement Modal Logic

用户评价
全部评价

热门资源

  • Learning to Predi...

    Much of model-based reinforcement learning invo...

  • Stratified Strate...

    In this paper we introduce Stratified Strategy ...

  • The Variational S...

    Unlike traditional images which do not offer in...

  • A Mathematical Mo...

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

  • Rating-Boosted La...

    The performance of a recommendation system reli...