AIAI Seminar - 28 March 2022 - Talks by Paulius Dilkas and Mark Chevallier

Talks by Paulius Dilkas and Mark Chevallier

Speaker:              Paulius Dilkas

Title: 

Recursive Solutions to First-Order Model Counting

Abstract:

First-order model counting (FOMC) is a #P-complete computational problem that asks to count the models of a sentence in first-order logic. Despite being around for more than a decade, practical FOMC algorithms are still unable to compute functions as simple as a factorial. We argue that the capabilities of FOMC algorithms are severely limited by their inability to express arbitrary recursive computations. To enable arbitrary recursion, we relax the restrictions that typically accompany domain recursion and generalise circuits used to express a solution to an FOMC problem to graphs that may contain cycles. To this end, we enhance the most well-established (weighted) FOMC algorithm ForcLift with new compilation rules and an algorithm to check whether a recursive call is feasible. These improvements allow us to find efficient solutions to counting fundamental structures such as injections and bijections.

Speaker:              Mark Chevallier

Title:

A Formalisation of Markov Decision Processes with Rewards

Abstract:

We demonstrate a formalisation of Markov Decision Processes with rewards in the theorem proving tool Isabelle. MDPs are defined using sets of states and actions that define the possible transitions between them, and rewards are modelled with a function on transitions and the actions which caused them. We prove the existence of an optimal policy on MDPs as well as demonstrate that the dynamic programming methods of value iteration and policy iteration can lead us to such a policy (or an arbitrarily close approximation) in finite time. We discuss the specifics of the model we are using and compare it to other possibilities.