Knowledge Representations for Efficient Boolean Functional Synthesis

Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is satisfied. More precisely, given a Boolean formula F (X, I), where X is a vector of outputs and I is a vector of inputs, the Boolean Skolem function synthesis problem (BFnS) asks to compute a Skolem function vector G(I) such that F (G(I), I) holds whenever ∃X F (X, I) holds. This problem has a wide variety of applications ranging from cryptanalysis to certified QBF solving to reactive synthesis. In general, this problem is known to be hard: indeed complexity-theoretic hardness results show polysized and polytime computable Skolem functions are unlikely to exist always. However, algorithms developed using different techniques seem to perform surprisingly well on a wide set of benchmarks. This motivates us to ask if there is structure in the input representation that allows for efficient computation of Skolem functions. This investigation leads us down a rabbithole of knowledge representations, which enable efficient (in size and time) synthesis of Skolem functions. First, it is easy to see that well-known normal forms like BDDs, DNNFs permit efficient synthesis. But we can go significantly beyond this and obtain a semantic (checkable with a SAT solver!) condition on the specification that also allows for efficient Skolem function synthesis. This results in a normal form that is exponentially more succinct than the previous ones and yet permits efficient Skolem function synthesis. Finally, we ask if we may precisely characterize polytime and polysized Skolem function synthesis. Surprisingly, the answer is yes! We develop a normal form that captures exactly this requirement and examine its many properties and possible implications. This work is based on papers presented in FMCAD’2019 and a very recent work accepted at LICS’2021. [LICS’2021] A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis. Long version available at ArXiv: https: //arxiv. org/abs/2104. 14098[FMCAD’2019] Knowledge Compilation for Boolean Functional Synthesis. Long version available at ArXiv: https: //arxiv. org/abs/1908. 06275[Coauthors: All this work is joint with Supratik Chakraborty of IIT Bombay. The LICS’21 paper is also with Preey Shah and Aman Bansal, while FMCAD’19 was jointly done with Jatin Arora, Divya Raghunathan, Shetal Shah and S. Krishna. All authors are from IIT Bombay or were at IIT Bombay when a bulk of the work was carried out. ]

Authors

• S. Akshay Indian Institute of Technology Bombay, Mumbai, India

Keywords

No keywords are indexed for this paper.