How to derive good lower bounds on resolution proof length?
Session date: 25 March 2024
Session host: Konstantin Sidorov
Summary:
In this brainstorm, we have discussed the problem of proof minimization for resolutional proofs of unsatisfiability, and the key challenge of deriving tight lower bounds on the proof size.