Encodings of Bounded Synthesis
Peter Faymonville Bernd Finkbeiner Markus N. Rabe Leander Tentrup




Saarland University University of California, Berkeley

Encodings of Bounded SynthesisSupported by the European Research Council (ERC) Grant OSARES (No. 683300).
    Peter Faymonville1 Bernd Finkbeiner1 Markus N. Rabe2 Leander Tentrup1
    ?; revised ?; accepted ?. - To be entered by editorial office
=========================================================================================================




The reactive synthesis problem is to compute a system satisfying a  given specification in temporal logic. 
Bounded synthesis is the approach to bound the maximum size of the system that we accept as a solution to the reactive synthesis problem. 
As a result, bounded synthesis is decidable whenever the corresponding verification problem is decidable, and can be applied in settings where classic synthesis fails, such as in the synthesis of distributed systems.
In this paper, we study the constraint solving problem behind bounded synthesis.
We consider different reductions of the bounded synthesis problem of linear-time temporal logic (LTL) to constraint systems given as boolean formulas (SAT), quantified boolean formulas (QBF), and dependency quantified boolean formulas (DQBF).
The reductions represent different trade-offs between conciseness and algorithmic efficiency.
In the SAT encoding, both inputs and states of the system are represented explicitly; in QBF, inputs are symbolic and states are explicit; in DQBF, both inputs and states are symbolic.
We evaluate the encodings systematically using benchmarks from the reactive synthesis competition (SYNTCOMP) and state-of-the-art solvers.
Our key, and perhaps surprising, empirical finding is that QBF clearly dominates both SAT and DQBF.





§ INTRODUCTION




There has been a recent surge of new algorithms and tools for the
synthesis of reactive systems from temporal specifications <cit.>. Roughly,
these approaches can be classified into two categories:
game-based synthesis <cit.> translates the specification into an
deterministic automaton and subsequently determines the
winner in a game played on the state graph of this automaton; 
bounded synthesis <cit.> constructs a constraint system that
characterizes all systems, up to a fixed bound on the size of the
system, that satisfy the specification.

The success of game-based synthesis is largely due to the fact that
it is often possible to represent and analyze the game arena symbolically,
in particular with BDDs (cf. <cit.>). As a result, it has been possible to scale
synthesis to realistic benchmarks such as the AMBA bus protocol <cit.>.
However, because the deterministic automaton often contains many more
states than are needed by the implementation, the synthesized
systems are often unnecessarily (and impractically) large (cf. <cit.>).

This problem is addressed by bounded synthesis, where an
iteratively growing bound can ensure that the synthesized system is
actually the smallest possible realization of the
specification. However, bounded synthesis has not yet reached the same
scalability as game-based synthesis. A likely explanation for the
phenomenon is that the encoding of bounded synthesis into the
constraint system is “less symbolic” than the BDD-based
representation of the game arena.  Even though bounded synthesis tools typically
use powerful SMT solvers, a careful study of the standard encoding shows
that both the states of the synthesized system and its inputs are enumerated explicitly <cit.>.

The question arises whether it is the encodings that need to be
improved, or whether the poor scalability points to a more fundamental
flaw in the underlying solver technology. To answer this question, we
reduce the bounded synthesis problem of linear-time temporal logic
(LTL) to constraint systems given as boolean formulas (SAT),
quantified boolean formulas (QBF), and dependency quantified boolean
formulas (DQBF).  The reductions are landmarks on the
spectrum of symbolic vs. explicit encodings.

All encodings represent the synthesized system in terms of its
transition function, which identifies the successor state in terms of
the current state and the input, and additionally in terms of an
output function, which identifies the output signals in terms of the
current state and the input, and annotation functions, which relate
the states of the system to the states of a universal automaton
representing the specification.

In the SAT encoding of the transition function, a separate boolean
variable is used for every combination of a source state, an input
signal, and a target state. The encoding is thus explicit in both the
state and the input.  In the QBF encoding, a universal quantification
over the inputs is added, so that the encoding becomes symbolic in the
inputs, while staying explicit in the states. Quantifying universally
over the states, just like over the input signals, is not possible in QBF
because the states occur twice in the transition function, as source
and as target. Separate quantifiers over sources and targets would
allow for models where, for example, the value of the output function
differs, even though both the source state and the input are the same.
In DQBF we can avoid such artifacts and obtain
a “fully symbolic” encoding in both the states and the input.

We evaluate the encodings systematically using benchmarks from the
reactive synthesis competition (SYNTCOMP) and state-of-the-art
solvers.  Our empirical finding is that QBF clearly dominates both SAT
and DQBF. While the dominance of QBF over SAT fits with our intuition
that a more symbolic encoding provides opportunities for optimization
in the solver, the dominance of QBF over DQBF is surprising. This
indicates that with the currently available solvers, the most symbolic
encoding (DQBF) is not the best choice. Of course, with better
DQBF solvers, this may change: our benchmarks identify
opportunities for improvement for current DQBF solvers.




  §.§.§ Related Work.



The game-based approach to the synthesis of reactive systems dates back to Büchi and Landweber's seminal 1969 paper <cit.>.
Modern implementations of this approach exploit symbolic representations of the game arena, using BDDs (cf. <cit.>) or decision procedures for the satisfiability of Boolean formulas (SAT-, QBF- and DQBF-solvers). We refer to <cit.> for a detailed comparison of the different methods.

Bounded synthesis belongs to the class of Safraless decision procedures <cit.>. Safraless synthesis algorithms avoid the translation of the specification into an equivalent deterministic automaton via Safra's determinization procedure. Instead, the specification is first translated into an equivalent universal co-Büchi automaton, whose language is then approximated in a sequence of deterministic safety automata, obtained by bounding the number of visits to rejecting states <cit.>. Most synthesis tools for full LTL, including Unbeast <cit.>, and Acacia+ <cit.>, are based on this idea. 

Bounded synthesis <cit.> limits not only the number of visits to rejecting states, but also the number of states of the synthesized system itself.
As a result, the bounded synthesis problem can be represented as a decidable constraint system, even in settings where the classic synthesis problem is undecidable, such as
the synthesis of asynchronous and distributed systems (cf. <cit.>). 
There have been several proposals for encodings of bounded synthesis.
The first encoding <cit.> was based on first-order logic modulo finite integer arithmetic. Improvements to the original encoding include the representation of transition systems that are not necessarily input-preserving, and, hence, often significantly smaller <cit.>, the lazy generation of the constraints from model checking runs <cit.>, and specification rewriting and modular solving <cit.>. Recently, a SAT-based encoding was proposed <cit.>.ä
Another SAT-based encoding <cit.> bounds, in addition to the number of states, also the number of loops. A QBF-based encoding has been used in the related problem of solving Petri games <cit.>. Petri games can be used to solve certain distributed synthesis problems. They have, however, a significantly simpler winning condition than the games resulting from LTL specifications.

This paper presents the first encodings of bounded synthesis based on QBF and DQBF, and the first comprehensive evaluation of the spectrum of encodings from SAT to DQBF with state-of-the-art solvers. The encodings are significantly more concise than the previous SAT-based encodings and provide opportunities for solvers to exploit the symbolic representation of inputs and states. The empirical evidence shows that, with current solvers, the QBF encoding is superior to the SAT and DQBF encodings. A further contribution of the paper are the benchmarks themselves, which pinpoint opportunities for the improvement of the solvers, in particular for DQBF.






§ PRELIMINARIES



Given a finite set of variables V, we identify boolean assignments α : V → as elements from the powerset of V, i.e., given V and α, then v⃗ =  v |α(v) = ∈ 2^V is a representation of α.
We use (V) to denote the set of propositional boolean formulas over the variables V. 




  
LTL.


Linear-time temporal logic (LTL) is the standard specification language for linear-time properties.
Let Σ be a finite alphabet, i.e., a finite set of atomic propositions.
The grammar of  is given by

    φ
      p |φ|φψ|φψ|φ|φψ|φψ,

where p ∈Σ is an atomic proposition.
The abbreviations p  p, ,  φ = φ, and φ = φ are defined as usual.
We assume standard semantics and write σφ if σ∈ (2^Σ)^ω satisfies φ.
The language of φ, written (φ), is the set of ω-words that satisfy φ.




  
Automata.


A universal co-Büchi automaton  over finite alphabet Σ is a tuple Q,q_0,δ,F, where
Q is a finite set of states,
q_0 ∈ Q the designated initial state,
δ:Q × 2^Σ× Q is the transition relation, and
F ⊆ Q is the set of rejecting states.
Given an infinite word σ∈ (2^Σ)^ω, a run of σ on  is an infinite path q_0 q_1 q_2 …∈ Q^ω where for all i ≥ 0  it holds that (q_i,σ_i,q_i+1) ∈δ.
A run is accepting, if it contains only finitely many rejecting states.
 accepts a word σ, if all runs of σ on  are accepting.
The language of , written (), is the set σ∈ (2^Σ)^ω| accepts σ.

We represent automata as directed graphs with vertex set Q and a symbolic representation of the transition relation δ as propositional boolean formulas (Σ). The rejecting states in F are marked by double lines.


  Given an LTL formula φ, we can construct a universal co-Büchi automaton _φ with (2^φ) states that accepts the language (φ).



  Consider the  formula ψ =  (r_1  g_1)  (r_2  g_2) (g_1  g_2).
  Whenever there is a request r_i, the corresponding grant g_i must be set eventually.
  Further, it is disallowed to set both grants simultaneously.
  The universal co-Büchi automaton _ψ that accepts the same language as ψ is shown in Fig. <ref>fig:automaton-arbiter.






  
Transition Systems.


In the following, we partition the set of atomic propositions into a set I that contains propositions controllable by the environment and a set O that contains propositions controllable by the system.
A transition system  is a tuple T,t_0,τ where
T is a finite set of states,
t_0 ∈ T is the designated initial state, and
τ : T ×IO× T is the transition function.
The transition function τ maps a state t and a valuation of the inputs i⃗∈ 2^I to a valuation of the outputs, also called labeling, and a next state t'.
If the labeling produced by τ(t,i⃗) is independent of i⃗, we call  a state-labeled (or Moore) transition system and transition-labeled (or Mealy) otherwise.
Formally,  is a state-labeled transition system if, given a state t ∈ T and any i⃗≠i⃗'⃗∈I with τ(t,i⃗)=(o⃗,_) and τ(t,i⃗'⃗)=(o⃗'⃗,_) it holds that o⃗ = o⃗'⃗.

Given an infinite word i⃗_⃗0⃗i⃗_⃗1⃗…∈ (2^I)^ω over the inputs,  produces an infinite trace (t_0∪i⃗_0 ∪o⃗_⃗0⃗) (t_1∪i⃗_1 ∪o⃗_⃗1⃗) …∈ (T ∪ I ∪ O)^ω where τ(t_j,i⃗_⃗j⃗) = (o⃗_⃗j⃗, t_j+1) for every j ≥ 0.
A path w ∈ (I ∪ O)^ω is the projection of a trace to the atomic propositions.
We denote the set of all paths generated by a transition system  as ().
A transition system realizes an  formula if () ⊆(φ).


  Figure <ref>fig:solution-arbiter depicts the two-state (state-labeled) transition system _𝑎𝑟𝑏 = t_0,t_1,t_0,τ with τ(t_0,i⃗) = (g_1,t_1) and τ(t_1,i⃗) = (g_2,t_0) for every i⃗∈ 2^I.
  The set of paths is () = (g_1g_2)^ω∪ (2^i_1,i_2)^ω.








§ BOUNDED SYNTHESIS



Bounded synthesis <cit.> is a synthesis procedure for  specifications that produces size-optimal transition systems.
A given  formula φ is translated into a universal co-Büchi automaton  that accepts the language (φ).
A transition system  realizes specification φ if, and only if, every trace generated by  is in the language (φ).
 is accepted by  if every path of the unique run graph, that is the product of  and , has only finitely many visits to rejecting states.
This acceptance is witnessed by a bounded annotation on this product.

The bounded synthesis approach is to synthesize a transition system of bounded size n, by solving a constraint system that asserts the existence of a transition system and labeling function of  as well as a valid annotation. 
In this section we discuss how to construct a formula that represents that a given annotation is correct. 
We will use this formula as a building block for different bounded synthesis constraint systems in Section <ref>.


The product of a transition system = T,t_0,τ and a universal co-Büchi automaton = Q,q_0,δ,F is a run graph = V,E, where
V = T × Q is the set of vertices and
E ⊆ V × V is the edge relation with

    ((t,q),(t',q')) ∈ E   iff  ∃i⃗∈ 2^I ∃o⃗∈ 2^O τ(t,i⃗) = (o⃗,t')  and  (q,i⃗∪o⃗,q') ∈δ .

An annotation λ : T × Q →∪ is a function that maps nodes from the run graph to either unreachable  or a natural number k.
An annotation is valid if it satisfies the following conditions:

  
  * the pair of initial states (t_0,q_0) is labeled by a natural number (λ(t_0,q_0) ≠), and
  
  * if a pair of states (t,q) is annotated with a natural number (λ(t,q) = k ≠) then for every i⃗∈ 2^I and o⃗∈ 2^O with τ(t,i⃗) = (o⃗,t') and (q,i⃗∪o⃗,q') ∈δ, the successor pair (t',q') is annotated with a greater number, which needs to be strictly greater if q' ∈ F is rejecting. That is, λ(t',q') q' k where q' > if q' ∈ F and ≥ otherwise.





  Figure <ref> shows the run graph of _𝑎𝑟𝑏 and _ψ from our earlier example (Fig. <ref>).
  Additionally, a valid annotation λ is provided at the second component of every node.
  One can verify that the annotation is correct by checking every edge individually.
  For example, the annotation has to increase from t_0,q_0→t_1,q_2 and from t_0,q_2→t_1,q_2 as q_2 is rejecting.
  As λ(t_0,q_0) = 0 and λ(t_0,q_2) = 1, it holds that λ(t_1,q_2) must be at least 2.


Given , , and λ, we want to derive a propositional constraint that is satisfiable if, and only if, the annotation is valid.
First, by the characterization above, we know that we can verify the annotation by local checks, i.e., we have to consider only one step in the product graph.

To derive a propositional encoding, we encode , , and λ:

  
  * = T,t_0,τ. We represent the transition function τ by one variable o_t,i⃗ for every output proposition o ∈ O and one variable τ_t,i⃗,t' representing a transition form t to t'. Given (t,t') ∈ T × T and i⃗∈ 2^I, it holds that (1) τ_t,i⃗,t' is true if, and only if, τ(t,i⃗) = (_,t'), and (2) o_t,i⃗ is true if, and only if, τ(t,i⃗) = (o⃗,_) and o ∈o⃗.
  
  * = Q,q_0,δ,F. We represent δ : (Q × 2^I ∪ O× Q) as propositional formulas δ_t,q,i⃗,q' over the output variables o_t,i⃗. 
      That is, an assignment o⃗ to the variables o_t,i⃗ satisfies δ_t,q,i⃗,q' iff (q,i⃗∪o⃗,q') ∈δ.
  
  * We first split the annotation λ into two parts: The first part λ^ : T × Q → represents the reachability constraint and the second part λ^# : T × Q → represents the bound. 
  For every t∈ T and q∈ Q we introduce variables λ^_t,q that we assign to be true iff the state pair is reachable from the initial state pair and a bit vector λ^#_t,q of length (log(T·Q)) that we assign the binary encoding of the value λ(t,q). 

Using the variables o_t,i⃗, τ_t,i⃗,t', λ^_t,q, and λ^#_t,q (which have a unique assignment for a given 𝒯, 𝒜, and λ) as well as the propositional formulas δ_t,q,i⃗,q', we construct a formula that represents that the annotation is valid:

    ⋀_q ∈ Q⋀_t ∈ T(λ^_t,q⋀_q' ∈ Q⋀_i⃗∈ 2^I( δ_t,q,i⃗,q'⋀_t' ∈ T( τ_t,i⃗,t'λ^_t',q'λ^#_t',q'q'λ^#_t,q)
        )
      )



  Given , , and an annotation λ.
  If the propositional encoding of , , and λ satisfy the constraint system, then λ is a valid annotation.








§ ENCODINGS




Using the constraints developed in the last section for checking the validity of a given annotation, we now consider the problem of finding a transition system with a valid annotation.

This section introduces four encodings, starting with the most explicit encoding and moving first to an input-symbolic variant, then to a input- and state-symbolic variant and then further to a “fully symbolic” variant which treats inputs, transition systems states and the specification automaton symbolically. The first encoding can be solved using a SAT solver, the second requires a QBF solver, and the remaining two encodings require a DQBF solver. 
We will indicate for each encoding the difficulty to switch from the decision variant of the problem (realizability) to the constructive variant of the problem (synthesis).




 §.§ SAT: The Basic Encoding
 


The basic encoding of bounded synthesis follows almost immediately from the last section. 
Instead of checking that for given 𝒯, 𝒜, and λ, the unique assignment to the variables satisfies the formula, we existentially quantify over the variables to find an assignment. 
We only have to add constraints that assert that the reachability information, represented in the variables λ^_t,q, is consistent, and that the transition relation, represented in the variables τ_t,i⃗,t', provides at least one transition for every source state and every input. 
The consistency of the reachability annotation is given once we assert λ^_t_0,q_0, as the formula itself asserts that the λ^_t,q annotations are consistent with the transition relation. 

     ∃λ^_t,q, λ^#_t,q |t ∈T, q ∈Q    

     ∃τ_t,i⃗,t' |(t,t') ∈T ×T, i⃗ ∈2^I    

     ∃o_t,i⃗ |o ∈O, t ∈T, i⃗ ∈2^I    

     λ^_t_0,q_0 ⋀_t ∈T ⋀_i⃗ ∈2^I ⋁_t' ∈T τ_t,i⃗,t'    

     ⋀_q ∈Q
  ⋀_t ∈T
    (λ^_t,q ⋀_q' ∈Q
    ⋀_i⃗ ∈2^I
    ( δ_t,q,i⃗,q' ⋀_t' ∈T ( τ_t,i⃗,t' λ^_t',q' λ^#_t',q' q' λ^#_t,q )
    )
  )    



  The size of the constraint system is in (n m^2 · 2^I· (δ_q,q' + n log(nm))) and the number of variables is in (n (m log(nm) + 2^I· ( O + n ))), where n = T and m = Q.


Since we only quantify existentially over propositional variables, the encoding can be solved by a SAT solver. The synthesized transition system can be directly extracted from the satisfying assignment of the solver. 
For each state and each input, there is at least one true variable, indicating a possible successor. The variables o_t,i⃗ indicate whether output o is given at state t for input i. 




 §.§ QBF: The Input-Symbolic Encoding
 


One immediate drawback of the encoding above is the explicit handling of the inputs in the existential quantifiers representing the transition relation τ and the outputs o, which introduces several variables for each possible input i⃗∈ 2^I.
This leads to a constraint system that is exponential in the number of inputs, both in the size of the constraints and in the number of variables. Also, since all variables are quantified on the same level, some of the inherent structure of the problem is lost and the solver will have to assign a value to each propositional variable, which may lead to non-minimal solutions of τ and o due to unnecessary interdependencies.

By adding a universal quantification over the input variables, we obtain a quantified boolean formula (QBF) and avoid this exponential blow-up.
In this encoding, the variables representing the λ-annotation remain in the outer existential quantifier - they cannot depend on the input.
We then universally quantify over the valuations of the input propositions I (interpreted as variables in this encoding) before we existentially quantify over the remaining variables. 

By the semantics of QBF, the innermost quantified variables, representing the transition function τ of , can be seen as boolean functions (Skolem functions) whose domain is the set of assignments to I.
Indicating the dependency on the inputs in the quantifier hierarchy, we can now drop the indices i⃗ from the variables τ_t,i⃗,t' and o_t,i⃗. 
Further, we now represent δ : (Q × 2^I ∪ O× Q) as propositional formulas δ_t,q,q' over the inputs I and output variables o_t⃗ (which depend on I) with the following property: an assignment i⃗∪o⃗ satisfies δ_t,q,q' iff (q,i⃗∪o⃗,q') ∈δ.
We obtain the following formula for the input-symbolic encoding.
(The gray box highlights the changes in the quantifier prefix compared to the previous encoding.)

     ∃λ^_t,q, λ^#_t,q |t ∈T, q ∈Q    

     ∀I    

     ∃τ_t,t' |(t,t') ∈T ×T    

     ∃o_t |o ∈O, t ∈T    

     λ^_t_0,q_0 ⋀_t ∈T ⋁_t' ∈T τ_t,t'    

     ⋀_q ∈Q
  ⋀_t ∈T
    (λ^_t,q ⋀_q' ∈Q
    ( δ_t,q,q' ⋀_t' ∈T ( τ_t,t' λ^_t',q' λ^#_t',q' q' λ^#_t,q )
    )
  )    



  Let n = T and m = Q.
  The size of the input-symbolic constraint system is in (nm^2 (δ_q,q' + n log(nm))).
  The number of existential and universal variables is in (n (m log(nm) + O + n)) and (I), respectively.


The input-symbolic encoding is not only exponentially smaller (in |I|) than the basic encoding, but also enables the solver to exploit the dependency between I and the transition function τ. 
An additional property of this encoding that we use in the implementation is the following: If we fix the values of the λ-annotation, the resulting 2QBF query represents all transition systems that are possible with respect to the λ-annotation.
Since the outermost variables are existentially quantified, their assignments (in case the formula is satisfiable) can be extracted easily, even from non-certifying QBF solvers.
For synthesis, we thus employ a two-step approach.
We first solve the complete encoding and, if the formula was satisfiable, extract the assignment of the annotation variables λ^_t,q, and λ^#_t,q. 
In the second step we instantiate the formula by the satisfiable λ-annotation and solve the remaining formula with a certifying solver to generate boolean functions for the inner existential variables.
Those can be then be translated into a realizing transition system.




 §.§ DQBF/EPR: The State- and Input-Symbolic Encoding
 


The previous encoding shows how to describe the functional dependency between the inputs I and the transition function τ and outputs o as a quantifier alternation. 
The reactive synthesis problem, however, contains more functional dependencies that we can exploit.

In the following we describe an encoding that also treats the states of the system to generate symbolically. 
First, we change the definition of T slightly.
Where before, T was the set of states of the transition system, we now consider T as the set of state bits of the transition system.
Consequently, the state space of  is now 2^T and we consider the initial state to be the all-zero assignment to the variables T. 

Since all variables depend on the state, we no longer have propositional variables.
Instead, we quantify over the existence of boolean functions.
Candidate logics for solving this query are dependency-quantified boolean formulas (DQBF) and the effective propositional fragment of first-order logic (EPR).
While the existential quantification over functions is not immediately available in DQBF, we can encode them in a quadratic number of constraints, which is known as Ackermannization <cit.>. 

    ∃λ^_q 2^T →, λ^#_q 2^T →^b |q ∈Q    

     ∃τ: 2^T ×2^I →2^T    

     ∃ o 2^T ×2^I →|o ∈O    

     ∀I ∀T, T'     

     (T = 0 λ^_q_0(T))    

     ⋀_q ∈Q
    (λ^_q(T) ⋀_q' ∈Q
    ( δ_q,q' (τ(T,I) ⇒T') λ^_q'(T') λ^#_q'(T') q' λ^#_q(T) )
  )    



  Let n = T and m = Q.
  The size of the state-symbolic constraint system is in (m^2 (δ_q,q' + log(nm))).
  The number of existential and universal variables is in (n + m log(nm) + O) and (n + I), respectively.







  
Encoding the states of the specification automaton.


The last dependency that we consider here is the dependency on the state space of the specification automaton.

As a precondition, we need a symbolic representation = Q,q_init,δ,q_reject of a universal co-Büchi automaton over alphabet I ∪ O, where
Q is a set of variables whose valuations represent the state space,
q_init∈(Q) is a propositional formula representing the initial state,
δ∈(Q,I ∪ O,Q') is the transition relation (q⃗∪i⃗∪o⃗∪q⃗'⃗ satisfies δ iff q⃗q⃗'⃗), and
q_reject∈(Q) is a formula representing the rejecting states.

    ∃λ^2^T ×2^Q →, λ^# 2^T ×2^Q →^b    

     ∃τ: 2^T ×2^I →2^T    

     ∃ o 2^T ×2^I →|o ∈O    

     ∀I ∀T, T' ∀Q, Q'     

     (t_init q_init →λ^(T, Q))     

      (λ^(T, Q) ( δ(τ(T,I) ⇒T') λ^(T',Q') λ^#(T',Q') q'_reject λ^#(T, Q) )
  )    



  Let n = T and m = Q.
  The size of the state-symbolic constraint system is in (n + m + δ + log(nm)).
  The number of existential and universal variables is in (log n + O) and (n + m + I), respectively.






 §.§ Comparison



Table <ref> compares the sizes of the encodings presented in this paper.
From the basic propositional encoding, we developed more symbolic encodings by making dependencies explicit and employing Boolean functions.
This conciseness, however, comes with the price of higher solving complexity.
In the following section we study this tradeoff empirical.








§ EXPERIMENTAL EVALUATION








 §.§ Implementation



We implemented the encodings described in this paper in a tool called BoSy[The tool is available at <https://react.uni-saarland.de/tools/bosy/>].
The  to automaton conversion is provided by the tool ltl3ba <cit.>.
We reduce the number of counters and their size by only keeping them for automaton states within a rejecting strongly connected component, as proposed in <cit.>.
The tool searches for a system implementation and a counter-strategy for the environment in parallel. An exponential search strategy is employed for the bound on the size of the transition system. 
In synthesis mode, we apply as a post-processing step circuit minimization provided by ABC <cit.>.


For solving the non-symbolic encoding, we translate the propositional query to the DIMACS file format and solve it using the CryptoMiniSat SAT solver in version 5.
The satisfying assignment is used to construct the realizing transition system.

The input-symbolic encoding is translated to the QDIMACS file format and is solved by a combination of the QBF preprocessor Bloqqer <cit.> and QBF solver RAReQS <cit.>.
The solution extraction is implemented in two steps.
For satisfiable queries, we first derive a top level (λ) assignment <cit.> and instantiate the QBF query using this assignment which results in a 2QBF query that represents transition systems that satisfy the specification.
This is then solved using a certifying QBF solver, such as QuAbS <cit.>, CADET <cit.>, or CAQE <cit.>.
Among those, QuAbS performed best and was used in the evaluation.
The resulting resulting Skolem functions, represented as AIGER circuit, are transformed into a representation of the transition system.

The symbolic encodings are translated to DQDIMACS file format and solved by the DQBF solver iDQ <cit.>.
Due to limited solver support, we have not implemented solution extraction.

For comparison, we also implemented an SMT version using the classical encoding <cit.>.
We also tested the state-symbolic and symbolic encoding with state-of-the art EPR solvers, but the solving times were not competitive. 
Table <ref> gives an overview over the capabilities of the implemented encodings.






 §.§ Setup & Benchmarks



For our experiments, we used a machine with a 3.6 GHz quad-core Intel Xeon processor and 32 GB of memory.
The timeout and memout were set to 1 hour and 8 GB, respectively.

We use the LTL benchmark sets from the latest reactive synthesis competition (SYNTCOMP 2016) <cit.>. The benchmarks include a variety of arbiter specifications of increasing complexity, load balancers, buffers, detectors as well as benchmark suites from previously existing tools. Some of the benchmark classes are parameterized in the number of clients or masters, which allows scaling them for experimental purposes. In total, the realizability benchmark suite of SYNTCOMP 2016 consists of 195 benchmarks. We have additionally added six instances from scalable benchmark classes of this set to cover larger parameter values, resulting in a total size of 201 benchmarks for our benchmark set.

For comparison, we run the other two solves that participated in the SYNTCOMP 2016, that is Acacia <cit.>, a game-based solver, and Party <cit.>, a variant of the SMT bounded synthesis.


	



 §.§ Realizability







In Table <ref>, we report results on realizability for all scalable instances from the aforementioned competition. We have omitted the results of our fully symbolic encoding from the table, since it could not solve a single instance of the selected benchmarks. The results from our own SMT encoding are also omitted, since they are very close to the results of the tool Party. Highlighted are those entries which reach the highest parameter value among the solvers and the best cumulative runtime within the class of instances.	
	
An overall comparison of all realizability solvers on the full benchmark set is provided in Figure <ref>. For the individual solvers, we track the number of instances solved by this solver within a a certain time bound.	









 §.§ Synthesis




To evaluate the different encodings in terms of their solutions to the synthesis problem and to compare with other competing tools, we measure the size of the provided solutions. In line with the rules of SYNTCOMP, the synthesized transition system is encoded as an AIGER circuit. The size of the result is measured in terms of the number of AND gates. In the comparisons, we only consider instances where both solvers in the comparison had a result. All resulting circuits have been minimized using ABC.

First, we compare in the scatter plot of Figure <ref> the propositional, non-symbolic encoding to the input-symbolic encoding. Since most points are below the diagonal and are therefore smaller than their counterparts, the input-symbolic solutions are better in size compared to the non-symbolic encoding. 




In Figure <ref>, we compare our input-symbolic encoding against two competing tools. On the left, we observe that the solution sizes of our input-symbolic encoding are significantly better (observe the log-log scale) than the solutions provided by Acacia. The reason for the size difference is that the strategies of Acacia may depend on the current state of the specification automaton, as they are extracted from the resulting safety game. When comparing to the SMT-based Party tool, we again see a strict improvement in terms of strategy size, but not as significant as for Acacia.

We thus observe that the ability to universally quantify over the inputs and extract the transition system from the functional descriptions leads to advantages in terms of the size of the solution strategies.










§ CONCLUSION



We have revisited the bounded synthesis problem <cit.> and presented alternative encodings into boolean formulas (SAT), quantified boolean formulas (QBF), and dependency-quantified boolean formulas (DQBF).
Our evaluation shows that the QBF approach clearly dominates the SAT approach and the DQBF approach, and also previous approaches to bounded synthesis – both in terms of the number of instances solved and in the size of the solutions. 
This demonstrates that, while modern QBF-solvers effectively exploit the input-symbolic representation, current DQBF solvers cannot yet take similar advantage of the state-symbolic representation. The benchmarks obtained from the encodings of bounded synthesis problems should therefore be useful in improving current solvers, in particular for DQBF.




