Encodings of Bounded Synthesis

TL;DR

This paper explores different encoding strategies for bounded synthesis in reactive systems, finding that QBF-based encodings outperform SAT and DQBF in efficiency through systematic evaluation.

Contribution

It introduces and compares SAT, QBF, and DQBF encodings for bounded synthesis, highlighting the superior performance of QBF in practical benchmarks.

Findings

QBF encoding dominates SAT and DQBF in efficiency

Systematic evaluation on SYNTCOMP benchmarks

Trade-offs between encoding conciseness and efficiency

Abstract

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.