Talks
Spring 2021

Bringing Proof Logging to Things That Aren't SAT
Wednesday, June 15th, 2022, 3:30 pm–4:00 pm
Speaker:
Ciaran McCreesh (University of Glasgow)
Location:
Calvin Lab Room 116
Proof logging is one of the greatest things to come out of Boolean satisfiability solving: as well as producing an answer, solvers are expected to give an independently verifiable mathematical proof that their answer is correct. What would it take to bring this technology to other solving paradigms? By going from Boolean models to pseudo-Boolean models, and from extended resolution to extended cutting planes, we can provide proof logging for the state of the art in subgraph finding algorithms, and make a good start on proof logging for fully general constraint programming solvers with large domains and rich constraints.
Attachment | Size |
---|---|
![]() | 12.4 MB |