13:00
14:00

Given a relational specification \varphi(X, Y_1, ... Y_n), Boolean functional synthesis concerns the construction of Boolean functions F_1(X), ... F_n(X) such that \varphi(X, F_1, ... F_n) is semantically equivalent to \exists Y_1, ... Y_n \varphi(X, Y_1, ... Y_n). Such functions are also called Skolem functions, and their algorithmic synthesis has many applications, including in program synthesis, QBF-SAT certificate generation, circuit repair, reactive synthesis, planning and the like. The synthesis problem is intractable unless long-standing complexity-theoretic conjectures are falsified. Fortunately, polynomial-time synthesis algorithms can be designed if \varphi is represented in special normal forms. In this talk, we present some such normal forms, including those that were originally studied in AI and formal verification, and others like Synthesis Negation Normal Form (SynNNF) and Subset And-Unrealizable Normal Form (SAUNF) that have arisen from our study of synthesis. We discuss properties of such forms and relations between them, and show that every universal representation that admits polynomial-time synthesis is polynomially reducible to SAUNF. We also sketch the idea behind compilation algorithms that convert a Boolean specification given as a circuit to SynNNF or SAUNF. We conclude with empirical evidence that shows that such compilation algorithms hold promise in practice.

LaBRI, 178