Albert Atserias, Universitat Politècnica de Catalunya, Microsoft Research Lectures
Add to your list(s)
Download to your calendar using vCal
If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.
Resolution underlies most state-of-the-art satisfiability-solving algorithms that are used in practice. I will start my talk by discussing this. Then I will focus on explaining some new understanding of the power of these algorithms that emerged from a novel kind of analysis of the produced proofs of unsatisfiability. The outcome is that the current standard methods for satisfiability-solving have the potential of simulating bounded-width resolution with polynomial-time overhead, provided they do random decisions and restarts often enough.
This talk is part of the Microsoft Research Cambridge, public talks series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
|