16969

Video URL

https://simons.berkeley.edu/talks/pseudo-boolean-solving-and-optimization-0

Pseudo-Boolean Solving and Optimization

(2021). Pseudo-Boolean Solving and Optimization. The Simons Institute for the Theory of Computing. https://simons.berkeley.edu/talks/pseudo-boolean-solving-and-optimization-0

Pseudo-Boolean Solving and Optimization. The Simons Institute for the Theory of Computing, Feb. 04, 2021, https://simons.berkeley.edu/talks/pseudo-boolean-solving-and-optimization-0 

          @misc{ scivideos_16969,
            doi = {},
            url = {https://simons.berkeley.edu/talks/pseudo-boolean-solving-and-optimization-0},
            author = {},
            keywords = {},
            language = {en},
            title = {Pseudo-Boolean Solving and Optimization},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {feb},
            note = {16969 see, \url{https://scivideos.org/Simons-Institute/16969}}
          }
Jakob Nordström (University of Copenhagen & Lund University)
Talk number16969
Source RepositorySimons Institute
Subject

Abstract

Pseudo-Boolean solving is the task of finding a solution to a collection of (linear) pseudo-Boolean constraints, also known as a 0-1 integer linear program, possibly optimizing some linear objective function. This problem can be approached using methods from conflict-driven clause learning (CDCL) SAT solving as in MaxSAT solvers, or "native" pseudo-Boolean reasoning based on variants of the cutting planes proof system, or (mixed) integer linear programming (MIP). The purpose of this tutorial is to provide a brief survey of pseudo-Boolean reasoning, MaxSAT solving, and integer linear programming, focusing on the potential for synergy between these different approaches and highlighting many open problems on both the applied and the theoretical side.