Henkin Synthesis: DQBF meets Machine Learning

Abstract

Quantified Boolean Formulas (QBF) extend propo- sitional logic with quantification ∀, ∃ for propositional variables. In QBF an existentially quantified variable is allowed to depend on all universally quantified variables in its scope. Dependency Quantified Boolean Formulas (DQBF) restricts the dependen- cies of existentially quantified variables. In DQBF, existentially quantified variables have explicit dependencies on subset of universally quantified variables, called Henkin dependencies. Given a Boolean specification between the set of inputs and set of outputs, the problem of Henkin synthesis is to synthesise each output variable as a function of its Henkin dependencies such that the specification is met. Henkin synthesis has wide- ranging applications, including verification of partial circuits, the synthesis of safe controllers, analysis of games. In this work, we propose a machine learning-based approach to Henkin synthesis, called DepManthan. DepManthan is the first general-purpose technique that can synthesise Henkin functions for both True and False DQBF instances. On an extensive evaluation over 550 instances, we demonstrate that DepManthan can synthesise functions for 350 instances compared to 101 instances by the prior state-of-the-art.

Publication
30th International Workshop on Logic & Synthesis

Next
Previous