Abstract
Given a Boolean relational specification \varphi(X, Y) over input variables X and output variables Y, the Boolean functional synthesis problem asks us to synthesize Y as a function F(X) such that for every X, the formula (\exists Y \varphi(X, Y)) holds iff \varphi(X, F(X)) holds. The function F(X) is also called the Skolem function for Y. Boolean functional synthesis has several applications, including in certified QBF solving, program and circuit repair, integer factorization, reactive controller synthesis and the like. In recent years, several tools have been developed that solve several large benchmark instances, including those with hundreds to thousands of X and Y variables. Despite the sophistication of these tools, however, there are several relational specifications, including those that don't involve very large numbers of variables, that have defied efficient synthesis by any tool. This motivates us to ask if the synthesis problem can be eased by compiling a given specification into a suitable normal form. In this talk, we describe one such normal form, called SynNNF, and discuss its properties. We show how a Boolean relational specification in SynNNF admits a quadratic time synthesis algorithm. SynNNF subsumes DNNF, which is widely used in AI applications. In fact, SynNNF can be shown to be exponentially more succinct than DNNF. We also discuss additional succinctness results that are premised on long-standing complexity-theoretic conjectures. Finally, we discuss an algorithm for top-down compilation of a CNF formula to SynNNF, and present some experimental results using a suite of benchmarks.
This is joint work with S. Akshay, Jatin Arora, S. Krishna, Divya Raghunathan and Shetal Shah.