  Existing approaches to synthesize reactive systems from declarative
specifications mostly rely on Binary Decision Diagrams (BDDs), inheriting their
scalability issues. We present novel algorithms for safety specifications that
use decision procedures for propositional formulas (SAT solvers), Quantified
Boolean Formulas (QBF solvers), or Effectively Propositional Logic (EPR). Our
algorithms are based on query learning, templates, reduction to EPR, QBF
certification, and interpolation. A parallelization combines multiple
algorithms. Our optimizations expand quantifiers and utilize unreachable states
and variable independencies. Our approach outperforms a simple BDD-based tool
and is competitive with a highly optimized one. It won two medals in the
SyntComp competition.
