Knowledge Compilation for Boolean Functional Synthesis

Autor:	Akshay, S., Arora, Jatin, Chakraborty, Supratik, Krishna, S., Raghunathan, Divya, Shah, Shetal
Rok vydání:	2019
Předmět:	Computer Science - Logic in Computer Science
Druh dokumentu:	Working Paper
Popis:	Given a Boolean formula F(X,Y), where X is a vector of outputs and Y is a vector of inputs, the Boolean functional synthesis problem requires us to compute a Skolem function vector G(Y)for X such that F(G(Y),Y) holds whenever \exists X F(X,Y) holds. In this paper, we investigate the relation between the representation of the specification F(X,Y) and the complexity of synthesis. We introduce a new normal form for Boolean formulas, called SynNNF, that guarantees polynomial-time synthesis and also polynomial-time existential quantification for some order of quantification of variables. We show that several normal forms studied in the knowledge compilation literature are subsumed by SynNNF, although SynNNFcan be super-polynomially more succinct than them. Motivated by these results, we propose an algorithm to convert a specification in CNF to SynNNF, with the intent of solving the Boolean functional synthesis problem. Experiments with a prototype implementation show that this approach solves several benchmarks beyond the reach of state-of-the-art tools. Comment: Full version of conference paper accepted at FMCAD 2019
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1908.06275 Zobrazit plný text záznamu View this record from Arxiv