Function synthesis is the problem of automatically constructing functions that ful l a given speci cation. 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 speci cations derived from experimental measurements.
Synthesis techniques aim towards the automated construction of correct-by-design systems from
speci cations of desired behaviour, often expressed as temporal logic speci cations [14]. These
techniques have been successfully applied in a number of elds, including software [
Abstraction techniques are often applied as part of computational modelling, both to
describe the system at a su cient level of detail, and to increase the runtime performance of
synthesis algorithms. For example, the genetic regulation that arises via complex biochemical
processes, which governs many cellular processes can be represented by Gene Regulatory
Networks (GRNs). Further, these networks can be modelled as Boolean networks (BNs), under the
assumption that each involved gene can be abstracted into active or inactive states [
The challenge of constructing a BN for a given biological system lies in identifying the
network topology, i.e. the interactions between components which comprise a model that
reproduces all observed behaviour. To address this challenge, Dunn et al. [
An SMT-based synthesis approach, implemented as part of the RE:IN tool [
An alternative strategy to the iterative enumeration of concrete BNs from a constrained ABN is to synthesise a template function, parametrised by unknown, optional interactions, that describes all concrete models consistent with the observations. Such a representation of all consistent models is easily interrogated to reveal dependencies between interactions and expose all di erent mechanisms capable of producing the observed behaviour. If su ciently concise, this representation also serves as a valuable tool for understanding system properties and guiding further biological studies. For the speci c application to ABNs, function synthesis focuses on restricted sets of Boolean functions, through the instantiation of parametrised function templates. However, the problem of choosing appropriate templates is non-trivial. Here, we focus on this problem and propose a lazy algorithm that combines templates in a sound and complete manner. 2
Pnueli and Rosner were among the rst to suggest a theoretical framework for program
synthesis and accompanying algorithms, based on automata theory and temporal logic [14]. Since
then, this and similar techniques have been used in many applications, with varying degrees of
success. Examples include software synthesis, such as the recent work by Gulwani et al. [
Hardware synthesis has been a subject of research for many years. Given that some systems
are required to be nite-state, or have a very limited number of inputs and output, the resulting
synthesis problems are of moderate degree and often practically feasible. To this end, various
modelling, veri cation, and synthesis techniques are applied, many of them based on
automatatheoretic principles like the various classes of automata used in synthesis of temporal logic
speci cations; recent examples include distributed synthesis algorithms by Chatterjee et al. [
The synthesis algorithm that we propose in Sec. 4.2 is strongly inspired by more general
quanti er instantiation techniques in the wider area of automated theorem proving. Our
algorithm can be seen as an instance of Model-Based Quanti er Instantiation [
Originally introduced by Kau man [
For many (if not most) interactions between genes, it is not known whether they are indeed
present in a particular system and if so whether they are positive or negative, and it is very much
on the agenda of computational biology to discover and establish the type of these interactions.
For our models to encompass such partial knowledge, we add to each interaction a label that is
either optional or de nite. Where the presence of an optional interaction is unknown, a de nite
is assumed to be present. We thus de ne abstract Boolean networks over a set G := fg1; : : : ; gng
(in accordance with the semantics attached to them by Dunnet al. [
nite state-space Q = Bn = hg1; : : : ; gni
ABN models allow us to incorporate uncertainty about the precise topology of a BN. Some of the many concrete BNs (CBNs) captured by an ABN may produce behaviour that is consistent with experimental observations of the biological system, while others might not. Therefore a set of experimentally-derived constraints is imposed over the behaviour of ABNs to exclude networks that are inconsistent with observations. We then say that an ABN satis es an observation i there exists at least one concrete BN that satis es all such constraints.
Experimental observations are represented as reachability predicates over the states of some or all components at di erent time steps during the execution of the system. Every concrete execution of an ABN is a sequence of states q0; :::; qk. An observation is a set of concrete traces, which may be speci ed by a predicate that restricts the set of all traces, e.g., all traces starting in a particular starting state q0 and that reach a nal state qf .
De nition 2 (Observation satisfaction). An ABN satis es an observation i there exists at least one concrete BN, for which there exists at least one trace that satis es all conditions on initial, nal, and other states.
empty input alphabet, set of initial states Qi set of nal states F
Q,
Q, and transition relation : Q ri for each gene gi.
Q = (q; hr1(q); : : : ; rn(q)i); for all q 2 Q with an update function Example 1. Consider the network in Fig. 1(a). This depicts a small ABN where each circle represents a gene, each solid edge represents a de nite interaction, and each dashed edge represents an optional interaction (the bidirectional edge between Klf4 and Essrb represents two optional interactions). Fig. 1(b) shows all unique instantiations of optional interactions forming a CBN consistent with some set of observations (not shown here). Each column represents one CBN, where a green square indicates that the corresponding interaction was included, and a black square indicates that it was not. Fig. 1(c) shows the CBN corresponding to column 1 of Fig. 1(b) where only the rst interaction is instantiated.
In previous work, Dunn et al. [
We start by de ning parametrised templates that enable us to transform the problem of synthesising ( nding) a function into an equivalent problem of nding parameters or coe cient values. Note that our goal is not to synthesise or nd update functions ri of ABNs. Instead, the goal is to synthesise a concise description of the topology and the properties of ABNs (e.g., observational constraints), also encoded in Boolean functions. Such a template can be used to construct SMT queries to nd the coe cients required to model certain properties of a system.
To this end, we observe that all Boolean functions have an Algebraic Normal Form (ANF) polynomial, which provides a canonical representation of functions of n inputs in terms of 2n coe cients (in the worst case). Further, this representation also allows us to order Boolean functions in a manner that enables us to de ne a class of abstract function re nement procedures. We begin by stating the basic completeness property of ANF.
Theorem 1 (Folklore). Every Boolean formula f over variables fx1; : : : ; xng has an equivalent and unique Algebraic Normal Form (ANF) taking the form of f (x1; : : : ; xn) = a0 (a1 ^ x1) (a1;2 ^ x1 ^ x2) a1;:::;n ^ x1 ^ ^ xn (an ^ xn) (an 1;n ^ xn 1 ^ xn) for some a1; : : : ; a1;:::;n 2 f0; 1g where
is the exclusive-or operator.
We chose this representation of Boolean functions, because it allows us to easily identify and to specify some simple sub-classes of functions; for instance, constants are indeed just a single constant term, linear functions contain only monomials, etc. Mathematically, any other representation of Boolean functions may be equivalent, but we suspect that presenting functions in ANF may help computational biologists to interpret our results. To make this more explicit, we de ne algebraic polynomials as a symbolic representation of Boolean functions: De nition 3. Let X = fx1; : : : ; xng be a set of Boolean variables. A Boolean formula p over X, i.e., p(x1; : : : ; xn), is an algebraic normal form polynomial (or simply algebraic polynomial) if it is of the form p(x1; : : : ; xn) = c0 t1 tk where k < 2n, each ti is distinct from all others, and of the form ci ^ VjlX=0jj xl, where Xj is the j-th subset of 2X and xl is the l-th item in Xj , and fci j 0 i < 2ng is a set of distinct Boolean constants which we call the `coe cients'.
An algebraic polynomial is conveniently described as a subset of the ANF monomials in its representation, and it represents a set of Boolean functions (those representable by concrete choices of values for the coe cients ci). This de nition also allows us to order functions based on the lexicographical ordering of the coe cients. The maximal polynomial is the one equivalent to the (2n 1)-monomial ANF (with all coe cients ci = 1).
Lemma 1. For every non-maximal algebraic polynomial p, there is a polynomial p0 every monomial in p is included in p0. p s.t. 4.1
Given that we have established an ordering of ANF polynomials, we are now able to de ne directed search strategies that are designed to exhaust a particular class of functions. The search for a particular function representable within an algebraic polynomial is ultimately performed by checking a propositional formula for satis ability (in practice by an SMT solver), such that a satisfying assignment to all ci identi es a speci c function.
Example 2. The algebraic polynomial c (c1 ^ x1 ^ x2) corresponds to the Boolean functions ff (x1; x2) = 0; f (x1; x2) = 1; f (x1; x2) = x1 ^ x2; f (x1; x2) = 1 (x1 ^ x2)g.
Looking at Ex. 2, a query could be posted to a SMT solver that checks whether any of the functions corresponding to the given ANF is equivalent to a sought after Boolean function ( (x)). Such a query could be on the following form: ' = 9c; c1:8x: (x) , c (c1 ^ x1 ^ x2)
This query will only consider two of the arguments in x, this might of course not be enough, in which case a larger ANF must be tried. The key to e ciency lies in knowing which monomials to include in the ANF to make it feasible to nd suitable coe cients quickly.
The universal quanti er is necessary to ensure the ANF instantiated with coe cients behaves likes the given function. It could be eliminated by using enumeration of the whole domain (or partially, using some kind of bounded model checking), this has not been further developed at this point. However, this does not ensure a quanti er-free formula, since (x) might contain quanti ers (which is the case in many applications, including ABN synthesis).
Lem. 1 tells us that every Boolean function represented by p has an equivalent representation in some p0 p. If p is maximal, then all Boolean functions are included. We may therefore traverse any set of algebraic polynomials to search for a particular function, f , that has a representation in p, yet we are still able to guarantee to nd any Boolean function if we include (at least) the maximal polynomial. In practice, this is of course (too) expensive. Often, a much smaller set of functions, or a set of smaller functions, is su cient.
This leads us to a simple, sound, and complete search procedure: start with any algebraic polynomial p and see if it can represent f . If it cannot, then pick the next polynomial p0 p according to the ordering and retry. This is repeated until a suitable polynomial has been found. The process is guaranteed to terminate since there is only a nite number of algebraic polynomials over a xed set of variables, and the maximal algebraic polynomial is guaranteed to be able to represent f . 4.2
Let '(x) be a Boolean function and suppose that the problem is to synthesise another function f'(x) = '(x), i.e., for each assignment to x 2 X, we want f'(x) to compute the same result as '(x), but preferably in a smaller or more `general' representation. The idea is to slice the domain of assignments into subsets that are easily solvable, have small representations, and ultimately yield a description of f' that pairs predicates (functions that map inputs to 1 or 0), identifying parts of functions, with (function)-terms that e ciently describe the desired functional relationships between variables in '. Formally, we are looking for a model, that is a formula equivalent to '(x) but in a di erent form or representation.
We propose an iterative procedure: we begin by stating the formula to be modelled, f', and we construct an initial arbitrary model function m = 0, for f'(x). We then search for a counter-example, c, to the current model, m, i.e. an assignment to the variables x such that m(x) 6= '(x). Then a predicate find and a function fix is constructed s.t. find(c) = 1 ^ 8x : find(x) ) m(x) 6= '(x) and 8x : find(x) ) (fix(x) = '(x)). A new, improved model is then easily constructed from those parts: m0'(x) = IT E(find(x); fix(x); m(x)), where IT E is the if-then-else operator. The algorithm is summarised in Alg. 1.
This procedure can be relaxed in two ways while still maintaining completeness, approximating either the find or the fix predicate. This means that in each iteration a counter-example c is generated, w.r.t. the current model m. The task is then to \patch" the current model s.t. m(c) now computes the correct value. We synthesise find and fix, where find must identify at least one counter-example c, but is allowed to be imprecise elsewhere. The new model will be correct for c (per construction) and for no other function points will it be incorrect where it previously was correct (fix being exact). Therefore, the number of inputs for which the new model is correct, will be guaranteed to be larger than for the older model (by at least one). The m(x) 0; while 9x:m(x) 6= '(x) do c x s.t. m(x) 6= '(x); fd f d s.t. f d(c) ^ (8x:f d(x) ) m(x) 6= '(x)) ; fx f x s.t. 8x:f d(x) ) f x(x) = '(x) ; m(x) IT E(fd(x); fx(x); m(x)); end
Algorithm 1: The find and fix loop algorithm is described in Alg. 2. The reasoning for approximate fix is similar and summarised by Alg. 3.
m(x) 0 while 9c:m(c) 6= '(c) do fd f d s.t. f d(c) fx f x s.t. 8x:
f d(x) ) f x(x) = '(x) m(x)
IT E(fd(x); fx(x); m(x)) end Algorithm 2: Approximate find m(x) 0 while 9c:m(c) 6= '(c) do fd f d s.t. f d(c)^ 8x:f d(x) ) m(x) 6= '(x)
f x s.t. f x(x) = '(x) fx m(x)
IT E(fd(x); fx(x); m(x)) end Algorithm 3: Approximate fix 4.3
Combining find and fix with algebraic polynomial function templates leads to a Boolean function synthesis procedure, as outlined in Alg. 4. It rst looks for a counter-example ce to the m 0 ; while 9ce : m(ce) 6= '(ce) do p f indRepresentingP olynomial(ce; p0) ; while 9k : p(k) ^ ('(k) = 0) do p nextRepresentingP olynomial(k; p) ; m IT E(p; 1; m) ; end end
Algorithm 4: Approx. find, Exact fix-model search for formula ' initial model m.1 ndRepresentingPolynomial(ce, p0) generates an algebraic polynomial that contains ce (starting from an arbitrary but xed initial polynomial p0) and nextRepresentingPolynomial(k, p) generates an algebraic polynomial greater than p that contains k.
In ndRepresentingPolynomial as well as nextRepresentingPolynomial there is a lot of room for heuristics. A simple way of nding the next representing polynomial is by considering all possible ANFs and selecting the next one according to a lexicographical ordering (which is easy to construct) until a suitable is found. This will often be very slow and, so better heuristics are necessary. Our prototype implementation (FSREIN) implements a method based 1In essence, this is the query RE:IN uses to enumerate solutions. on identifying relevant variables from unsatis able core reasoning, and only adds monomials over those variables that appear in the core. An important insight here is that any heuristic that always produces larger polynomials is guaranteed to be complete. 5
Using the techniques presented in Sec. 4.3 a tool was implemented, FSREIN, which is capable
of synthesizing a Boolean function describing all concrete Boolean network, for a given ABN,
that are valid with resepect to some observational constraints. We present in this section a
comparison between this and the state-of-the-art tool for ABN reasoning (RE:IN [
Reduced Models. Consider the problem presented earlier in Fig. 1. The ABN shown in Fig. 1(a) is a module of the more extensive gene regulatory network that governs the mouse pluripotent embryonic stem cell (ESC) state dynamics. Experimental measurement of gene expression under di erent inputs allows us to de ne experimental observations of the pluripotency network, which we impose as constraints. Using RE:IN to enumerate consistent CBNs yields the table shown in Fig. 1(b). Eight unique CBNs are consistent with the experiments. From the table it is quite easy to see that the interaction Esrrb ! Oct4 is part of every solution, and it is thus a required interaction. The output of FSREIN are the two find-functions (Esrrb-->Oct4) OR ((not Esrrb-->Oct4) = (Esrrb-->Klfnn4 and Esrrb-->Oct4)) where the corresponding fix functions are both 1, from which it is trivial to see (or to deduce) that Esrrb ! Oct4 is a required interaction.
For another, larger example (16 genes, 8 optional interactions, 2 experiments) a similar result was found. When RE:IN was executed it enumerated 96 solutions, while FSREIN produces the following functions:
crafted a set of 39 simple benchmark problems on which to test both tools. Fig. 2 summarises the re- Figure 2: A comparison of the model sults after running each of the tools, comparing the size produced by RE:INand FSREIN. 10 100 1k 10k 100k RE:IN [# CBNs] ((Nanog --> Sox2) AND (Klf2 --> Oct4)) OR ((Sall4 --> Sox2) AND (Klf2 --> Oct4))
three orders of magnitude slower than running the RE:IN-tool, which can of course be a major obstruction, but there is plenty of room to greatly improve the e ciency of the procedure. However, the major improvement is the readability of the model. The FSREIN model is easy to understand and clearly shows the interactions between genes that is in a more `natural' form for computational biologists than the list of counter-examples obtained from RE:IN. 100k ] s e ta 10k c i d re 1k p [#100 N I ER 10 S F 1 1 size of the model expressions (the number of enumerated models for RE:IN and the number of find and fix-pairs for FSREIN) for each tool. Observe that FSREIN never produces a model larger than that of RE:IN, but it is interesting to see that in some cases it produces signi cantly smaller representations. 6
In this paper we present a function synthesis approach based on the find and fix-strategy, using algebraic polynomials to describe sets of Boolean functions to be synthesised. We apply this technique to problems that arise in computational biology; speci cally the abstract Boolean network synthesis problem, and show that in small instances it is able to produce functions describing the set of concrete Boolean networks that are consistent with the abstract network, and with experimental observations obtained through wet-lab experiments. The average runtime of our implementations is not better than the state-of-the-art, but it has the bene t of removing the burden of having to analyse a large set of enumerated models to nd patterns within the data. Rather, the functions describing the networks are kept in a compact and expressive representation, which is much more amenable to scienti c testing and interpretation. [14] Amir Pnueli and Roni Rosner. A framework for the synthesis of reactive modules. In Intl. Conf.
on Concurrency (Concurrency 1988), volume 335 of LNCS. Springer, 1988. [15] Mohammad Raza, Sumit Gulwani, and Natasa Milic-Frayling. Compositional program synthesis from natural language and examples. In IJCAI 2015. AAAI Press, 2015. [16] Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, and Clark W. Barrett.
Counterexample-guided quanti er instantiation for synthesis in SMT. In CAV 2015, volume 9207 of LNCS. Springer, 2015. [17] Andrew Reynolds, Cesare Tinelli, Amit Goel, Sava Krstic, Morgan Deters, and Clark W. Barrett.
Quanti er instantiation techniques for nite model nding in SMT. In CADE 2013, volume 7898.
Springer, 2013. [18] Armando Solar-Lezama. Program sketching. STTT, 15(5-6):475{495, 2013. [19] Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo de Moura. E ciently solving quanti ed bit-vector formulas. FMSD, 42(1):3{23, 2013.