Satisfiability solving with conflict driven clause learning and non-implicational inferences

Add to your list(s) Download to your calendar using vCal

• Sam Buss (University of California)
• Thursday 15 June 2023, 16:00-16:50
• UG05, Murray Learning Centre.

If you have a question about this talk, please contact George Kaye.

We will discuss propositional theorem proving and satisfiability algorithms based on conflict driven clause learning (cdcl) these methods have been extremely successful in solving large instances of satisfiability of practical interest, we will also discuss more recent non-implicational reasoning, including the drat proof system and substitution redundancy, which can potentially give satisfiability algorithms the full strength of extended resolution.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG05, Murray Learning Centre
• computer sience

Note that ex-directory lists are not shown.