Trustworthy Automated Reasoning

Channel:
United States Simons Institute for the Theory of Computing
Subscribers:
68,700
Published on ● Video Link: https://www.youtube.com/watch?v=dFTPC8cQ3Z4


Duration: 1:02:56
292 views
7

Marijn Heule (Carnegie Mellon University)
https://simons.berkeley.edu/talks/marijn-heule-carnegie-mellon-university-2023-04-20
Satisfiability: Theory, Practice, and Beyond

Automated reasoning has become increasingly powerful and popular. This enabled solving very hard problems ranging from determining the correctness of complex systems to answering long-standing open questions in mathematics. Moreover, we can have full confidence in the correctness of the solutions by producing certificates (proofs of unsatisfiability) that can be validated using trustworthy systems.

The talk covers some successes, including the solutions with proofs of the Boolean Pythagorean Triples problem, Keller's conjecture, and the packing chromatic number of the infinite square grid. The proofs are gigantic, but they have been validated using a formally-verified proof checker. These results underscore the effectiveness of automated reasoning to solve hard challenges arising in mathematics and elsewhere, while having stronger guarantees of correctness than pen-and-paper proofs.



Other Videos By Simons Institute for the Theory of Computing


2023-04-22SAT Beyond Boolean Interpretations
2023-04-22Unification of SAT, Constraint Programming, and Pseudo-Boolean Solving: A Personal Story
2023-04-22Explaining SAT Solving Using Causal Reasoning
2023-04-22Knowledge Compilation for Quantification and Synthesis
2023-04-22Proving UNSAT in Zero Knowledge
2023-04-22Analysis of Core-Guided MaxSat Using Cores and Correction Sets
2023-04-21Homomorphism Counts: Expressive Power and Query Algorithms
2023-04-21Proof Logging for Constraint Programming
2023-04-21Proof Logging for MaxSAT – The Past, The Present and The Future
2023-04-21Certified Static and Dynamic Symmetry Breaking
2023-04-21Trustworthy Automated Reasoning
2023-04-21MCSat Approaches for Solving Non-linear Modular Arithmetic
2023-04-21Reactive Synthesis Empowered by Logical Reasoning
2023-04-20The Power of Extended Resolution: A Practitioner's Perspective
2023-04-20Exploiting Combinatorial Structure in Constraint Programming: ...
2023-04-20Benefits of Abstract Modelling using Conjure
2023-04-20Exact Covering with Colours
2023-04-20Rado numbers: SAT methods and connections to Nullstellensatz complexity
2023-04-20Modern Constraint Programming, For People Who Know SAT
2023-04-20ASP: Theory, Practice, and Beyond
2023-04-19Logic, Optimization, and Constraint Programming: A Fruitful Collaboration


Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Satisfiability: Theory Practice and Beyond
Marijn Heule