Algebraic Polynomial-based Synthesis for Abstract Boolean Network Analysis

Function synthesis is the problem of automatically constructing functions that fulfil a given specification. Using templates to limit the form of those functions is a popular way of reducing the search-space while still allowing interesting functions to be found. We present an investigation of restrictions to templates over Boolean functions of polynomial shape, based on their algebraic normal form. These polynomials are then lazily created in such a way that completeness of the search is still guaranteed, while performance is improved. This method is then implemented using an SMT-solver (Z3) and illustrated on a biological problem, the goal of which is to synthesise (Boolean) gene regulatory networks that capture specifications derived from experimental measurements.