From formal verification to high-performance constraint solving

  • Robert Nieuwenhuis | Barcelona Tech

SAT and SAT Modulo Theories (SMT) are workhorses of formal verification. But they are also highly effective for constraint solving and optimization. In this talk we explain how this idea has been validated at Barcelogic.com and elsewhere. We shorty introduce SAT/SMT as well as our new IntSat method for Integer Linear Programming (ILP) and 0-1 ILP. Then we analyze some of our customers’ problems, explaining why we used our own tools or other classical ones. A short demo will illustrate easy logic-based modeling and cases where our solvers outperform the best-known commercial ones.

Speaker Details

Robert is a professor of Computer Science at Barcelona Tech. He and his team are well known for their work on automated reasoning, constraints, decision procedures, the efficient implementation of logics, and the Barcelogic SAT/SMT and combinatorial optimization tools. Robert has highly-cited publications and recognition as an invited speaker and PC-Chair (SAT, RTA, CADE, LPAR, IJCAR, CPAIOR). He is a co-founder and CEO of Barcelogic.com, the company that owns the Barcelogic tools and IP and uses them for solving hard combinatorial (optimization) problems.

    • Portrait of Jeff Running

      Jeff Running

Series: Microsoft Research Talks