| **Description:** | Given a relation f(X,Y) the Boolean functional synthesis problem is to synthesize a function F(X) that produces assignments to Y such that f(X,Y) is satisfied. For X for which there is no Y that satisfies the relation, the function F may provide any Y.
This submission is a QBF encoding of the functional synthesis problem, which states that for every X there is a Y such that f(X,Y). All formulas are thus in 2QBF and is only accurate for SAT results, which most of the formulas in this collection are. Certificates of formulas that are SAT are successfully synthesized functions and can be compared to the results in the paper. Formulas that are UNSAT may just indicate that there is no complete function. | |