Theoretical Foundation of Solvers: Context, Directions and Open Problems

          @misc{ scivideos_17235,
            doi = {},
            url = {https://simons.berkeley.edu/talks/tbd-263},
            author = {},
            keywords = {},
            language = {en},
            title = {Theoretical Foundation of Solvers: Context, Directions and Open Problems},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {feb},
            note = {17235 see, \url{https://scivideos.org/Simons-Institute/17235}}
          }
          

Abstract

Topics:  Vijay Ganesh: Perspectives on Practice and Theory of SAT Solving Abstract: Over the last two decades, SAT solvers have revolutionized many sub-fields of software engineering, security, and AI. This is largely due to a dramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Boolean satisfiability problem is NP-complete, believed to be intractable, and yet these solvers easily solve industrial instances containing millions of variables and clauses in them. How can that be? In my talk, I will briefly survey what we know about the power of SAT solvers through the lens of parameterized and proof complexity, as well as how we can build better SAT solvers by combining machine learning and proof systems. Laurent Simon: Towards an (experimental) Understanding of SAT Solvers Abstract: Despite important progresses in the practical solving of SAT problems, the behavior of CDCL solvers are only partially understood. In this talk, we will review some of the experimental studies that have been conducted so far, uncovering some surprising structures CDCL solvers are working on. David Mitchell: On Using Structural Properties to Improve CDCL Solver Performance Abstract: Instance structure is widely discussed and studied in the SAT solving community, but has never been explicitly made use of in dominant "industrial" SAT solvers.  We briefly review some structural properties of CNF formulas that have received attention, and some recent efforts to improve CDCL SAT solver performance using these properties.