Microsoft at FLoC 2022

Advancing Science with Platforms and Driving Scenarios: a perspective from a researcher at Microsoft Research

Nikolaj Bjørner

What does a research career in industry look like? While there is no single answer to this question, I will approximate by describing perspective based on personal experiences based on a career spanning work in a research institute, a startup, the core file systems group at Microsoft and at Microsoft Research. In each of the experiences, a background with a graduate degree specifically with an emphasis on logic and program logics, proved useful but in very different ways. The perspective of Microsoft Research is distinguished as it is based on the pursuit of advancing science that both aims much wider than business objectives and at the same time benefits, and is of benefit to, business and product groups. I will describe an example of a platform as a research tool (in this case the SMT solver z3) for driving foundational research and drive user scenarios. Platforms represent a researcher’s aim for long term, general results that establish and test methodologies. I describe experiences with combining platforms with driving scenarios based on business needs.

Nina Narodytska (Presenter) and Nikolaj Bjørner

Core-guided solvers are among best performing algorithms for solving maximum satisfiability problems. These solvers perform a sequence of relaxations of the formula to increase the lower bound on the optimal solution on each relaxation step. In addition, the relaxations allow generating a large set of minimal cores (MUSes) of the original formula. However, properties of these cores have not been investigated. In contrast, maximum hitting set-based (maxhs) solvers also extract a set of cores that posses a set of properties, e.g. the size of the minimal hitting set of the discovered cores equals the optimum when a maxhs solver terminates.

In this work, we analyze minimal cores and minimum correction sets (MinCSes) of the input formula and its sub-formulas that core-guided solvers produce during the execution. We demonstrate that a set of MUSes that a core-guided algorithm discovers posses the same key properties as cores extracted by maxhs solvers. For instance, we prove the size of a minimum hitting set of these the discovered cores equals to the optimal cost. We also show that it discovers all MinCSes of special subformulas of the input formula. We discuss theoretical and practical implications of our results.

Nikolaj Bjørner, Clemens Eisenhofer (Presenter), Laura Kovacs

We present ongoing work on developing the user-propagator framework in SMT solving. We argue that the integration of user-propagators in SMT solving yields an efficient approach towards custom theory reasoning, without bringing fundamental changes in the underlining SMT architecture. We showcase our approach in the SMT solver Z3, provide practical evidence of our work, and also discuss potential venues for further improvements.