Invited Speakers
SMT-Based Weighted Model Integration
Abstract: Weighted Model Integration (WMI) is a recent formalism generalizing Weighted Model Counting (WMC) to run probabilistic inference over hybrid domains, characterized by both discrete and continuous variables and relationships between them. WMI is computationally very demanding.
In this talk I will introduce WMI and its usage. Then I'll present our theoretical framework and algorithms for WMI, which allow to exploit the power of SMT-based AllSMT and SMT-based predicate-abstraction techniques in designing efficient inference procedures. Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference. I conclude by describing recent developments, plus ongoing and future work.
Programming Z3
Abstract: We give a programmer's introduction to the Satisfiability Modulo Theories Solver Z3. With the python scripting interface as starting point we describe ways to interact with Z3 and selected algorithms underlying the decision procedures. We present a set of case studies to cover some of the main available features while uncovering some of the internals.