{"id":"fb1fa6d7-909b-4ff9-a46f-2fe9db1ca564","arxiv_id":"1908.06275","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new normal form, SynNNF, guarantees polynomial-time Skolem function synthesis and existential quantification, subsumes wDNNF/DNNF/ROBDD, and supports a CNF-to-SynNNF compiler that solves benchmarks beyond current tools.","lead":"Boolean functional synthesis asks for output functions that satisfy a relational specification. This paper introduces a new normal form, SynNNF, that guarantees polynomial-time synthesis and quantifier elimination, and shows it subsumes earlier normal forms and enables a practical compiler.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"C2Syn's correctness relies on an unproven soundness assumption for FIND FD patterns, which Theorem 9 does not discharge; the SynNNF output property is also asserted without proof.","rationale":"The reader's weakest assumption and my independent analysis converge on the same point: the soundness of FIND FD pattern matching. This is the hinge between the theoretical SynNNF framework and the claimed practical compiler. Theorem 1 is self-contained and appears correct; the issues in Theorem 8's proof are typographical and do not affect the main synthesis algorithm. However, Theorem 9's guarantee that C2Syn outputs a SynNNF refinement is what lets a user take a CNF specification, compile it, and invoke Theorem 1 to get correct Skolem functions. The proof of Theorem 9 silently skips the SynNNF preservation and delegates the f-def construction to an assumed-sound subroutine. Because the paper itself flags this assumption, it is not a hidden flaw but an acknowledged gap; the conditional verdict is exactly right. The proposed test, a finite audit of all FIND FD patterns, would either discharge the assumption or produce a counterexample, thus settling the concern. I therefore recommend keeping the conditional acceptance.","tokens_in":27694,"tokens_out":19378,"duration_ms":178480,"concrete_test":"Extract the finite set of clause patterns hard-coded in FIND FD from the implementation and, for each pattern, use a SAT solver to verify that the pattern's clauses logically imply the claimed functional definition (e.g., for the AND pattern, check that (¬α∨β1)∧(¬α∨β2)∧(¬β1∨¬β2∨α) is equivalent to α↔(β1∧β2) on all 8 assignments of the placeholders, and similarly for OR/NAND/NOR/XOR/XNOR/NOT/identity). If all patterns pass, the assumption in Theorem 9 is discharged; if any fail, C2Syn's refinement guarantee is unsound.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central practical claim is Theorem 9, which states that C2Syn always terminates and returns a SynNNF specification F~ with F~ <syn φS. The proof in Appendix D only argues termination and refinement; it never shows that the constructed DAG is in SynNNF. More importantly, the refinement argument depends on Lemma 6(1), whose hypothesis is that (T,FunT) is an acyclic system of f-defs in the current formula. This hypothesis is discharged by FIND FD only under the explicit caveat in Section V: 'Assuming all patterns used by FIND FD to determine functional dependencies are sound.' No proof or exhaustive check of this assumption is given. If some pattern matches a clause set that does not semantically entail the claimed functional definition, then FunT built by FDR EFINE need not be implied by φS, so Lemma 6 can return a non-refinement; the Skolem functions extracted from F~ would then not satisfy the original specification. This is not a mere notation issue like the Theorem 8 tautology: it is a missing correctness condition on the algorithm that implements the main contribution. The empirical verifier checked only 185 outputs (183 verified, 1 timeout, 1 OOM), so the unconditional Theorem 9 is not established by experiment either.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies Boolean functional synthesis (Skolem function synthesis) for relational specifications F(X,Y). It introduces SynNNF, a subclass of NNF defined by the condition that each ith-reduct of the positive form of the specification is “∧i-unrealizable.” The authors prove that SynNNF admits polynomial-time synthesis and polynomial-time existential quantification for the output variables (Theorem 1), that SynNNF subsumes ROBDD/FBDD, dDNNF, DNNF, and wDNNF and can be super-polynomially more succinct than them (Theorem 2), and that SynNNF exactly characterizes when the GACKS functions give the correct existential quantification, with a related criterion for correctness of GACKS Skolem vectors (Theorem 3). They introduce a refinement relation with respect to synthesis (Section IV), propose a CNF-to-SynNNF compiler C2Syn (Section V), and report experiments on QBFEVAL 2018 and factorization benchmarks, including an independent verifier for the compiler’s outputs. The main practical and theoretical claim is Theorem 9, which states that C2Syn always terminates and returns a SynNNF refinement of the input CNF specification.","tokens_in":27701,"tokens_out":13678,"duration_ms":129656,"significance":"If the main theorems are correct, SynNNF is a genuinely useful normal form for Boolean functional synthesis and for some-order existential quantification. The paper gives a clean sufficient condition for polynomial-time synthesis, explains the previously unexplained empirical success of GACKS functions outside wDNNF, and provides a practical compilation approach with a prototype and an independent output verifier. The succinctness results relative to standard knowledge-compilation targets are interesting, and the refinement notion is a principled way to formalize the algorithm’s preprocessing. The paper also honestly reports that its verifier checked 183 of 185 successfully compiled instances, with one timeout and one out-of-memory. The main theoretical results are substantial and the empirical comparison is suggestive, although the proof of Theorem 9 is incomplete and the proof of Theorem 8 contains a typographical error that invalidates the argument as printed.","major_comments":[{"comment":"In the forward direction of Theorem 8, the displayed construction of ~F is ⋀_i ((x_i ∧ ψ_i(Y)) ∨ (¬x_i ∨ ¬ψ_i(Y))). The second disjunct should almost certainly be (¬x_i ∧ ¬ψ_i(Y)); as printed, each conjunct is a tautology, so ~F is equivalent to 1. The constant-true formula does not in general refine F, and it certainly does not encode the intended equivalence x_i ↔ ψ_i(Y). This is an easy typographical fix, but because Theorem 8 is one of the central equivalences of the paper, the proof as printed is invalid.","section":"Section IV, proof of Theorem 8"},{"comment":"The proof of Theorem 9 in Appendix D establishes termination and argues that each return statement of Algorithm 2 yields a refinement of φ_S, but it never proves that the returned DAG is in SynNNF. The missing case is line 30: the recursive calls return SynNNF sub-DAGs t1, t2, t3, but the paper does not show that t3 ∧ ((x ∧ t2) ∨ (¬x ∧ t1)) again satisfies the SynNNF condition for every output variable with respect to the original output ordering. In particular, when the same connected component contributes clauses to both S1 and S2, the sub-specifications t1 and t2 share output variables other than x, and paths from such a variable and its negation through different branches can meet at the root ∧-node; the proof must rule this out explicitly. The theorem also does not state what output order is used by the recursive calls and how that order is preserved. This is a load-bearing gap in the main practical theorem.","section":"Section V / Appendix D, proof of Theorem 9"},{"comment":"The text explicitly says “Assuming all patterns used by FIND FD to determine functional dependencies are sound,” but no proof or exhaustive validation of this assumption is given. The soundness of these patterns is load-bearing: Lemma 6 and the refinement guarantees of FDR EFINE require that (T′, FunT′) is a system of acyclic f-defs implied by the current clause set. Since Theorem 9 is stated unconditionally, the authors must either prove soundness of the pattern library or restate the theorem and the correctness claims as conditional on that assumption. This is not a stylistic issue; an unsound pattern can cause the output of C2Syn to fail to refine φ_S.","section":"Section V, description of FIND FD before Algorithm 1"},{"comment":"The reverse direction of Theorem 3(i) fixes an arbitrary realizable input valuation Y and then claims “As a result, we have α11 = 1” and “α01 = 0” and “α10 = 0.” These equalities hold only for the specific Y (together with a specific assignment to X^n_{i+1}) that satisfies the formula ζ witnessing non-∧i-unrealizability. An arbitrary realizable Y does not guarantee them. The proof should choose a satisfying assignment of ζ and use its Y-coordinate as the counterexample; this Y is realizable because α11 = 1 yields a full model of F. As written, the reverse direction of the iff is not established.","section":"Appendix B, proof of Theorem 3(i), reverse direction"}],"minor_comments":[{"comment":"The sentence “The correctness of lines 6 and 8 use Propositions 5(2) and 5(2)” should read “Propositions 5(2) and 5(3)”, since line 8 uses Proposition 5(3).","section":"Appendix D, proof of Theorem 9"},{"comment":"References [7] and [8] are the same FMCAD 2018 paper (“Functional synthesis via input-output separation”); one of the duplicates should be removed.","section":"References"},{"comment":"The definition of S3 ends with a stray semicolon: “S3 := {Ci ∈ S′ | ∀ Cj ∈ Pos ∪ Neg (Ci ≈S′ Cj);”. The semicolon should be removed.","section":"Section V, Algorithm 2, line 25"},{"comment":"The sentence “the root of ψj connects to a leaf of every ψi” is unclear; presumably the DAG of ψj is substituted into the input leaves of earlier ψi’s. The intended sharing of sub-DAGs should be described more precisely.","section":"Section III, proof of Theorem 1(ii)"},{"comment":"The paper reports that the verifier checked 183 of 185 successful outputs and timed out / ran out of memory on the other two. This is honest reporting, but the two unverified instances should be mentioned in Table I or the surrounding text so that the reader can see exactly which benchmark classes are affected.","section":"Section VI, verification paragraph"}],"recommendation":"major_revision","confidential_remarks":"The main concern is proof completeness rather than novelty. The SynNNF concept and the refinement framework are interesting, and the empirical comparison is useful. I would support acceptance if the authors provide a real proof that the C2Syn composition in Algorithm 2 line 30 preserves SynNNF, prove or explicitly conditionalize the soundness of the FIND FD pattern library, and fix the typo in the proof of Theorem 8. The gap in the proof of Theorem 3(i) is easy to repair but should be corrected."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Rough take: SynNNF is real. The paper identifies a new NNF subclass that guarantees polynomial-time Skolem synthesis and is provably more succinct than ROBDD, FBDD, dDNNF, DNNF, and wDNNF. The main theoretical machinery — the ∧i-unrealizability condition and the refinement relation ≼syn — is coherent, and the proof of Theorem 1 is direct. This is a genuine extension of the earlier wDNNF result, not a repackaging.\n\nWhat's good: the normal form is clean, the subsumption/succinctness arguments are standard conditional lower bounds and they hold up. The refinement relation is a useful formalization. The C2Syn idea — compile CNF to SynNNF with refinement — is interesting, and the experiments are honestly reported: 185/402 QBFEVAL instances plus all six factorization instances, with an independent check on 183 outcomes. That is real evidence the approach has traction.\n\nWhere it's soft: Theorem 8's proof contains a formula that is a tautology as printed — the conjunction over i of ((xi ∧ ψi) ∨ (¬xi ∨ ¬ψi)) is always true. The intended equivalence (xi ↔ ψi) is obvious, so this is a typo-level defect, but the proof as written does not establish the claimed characterization and must be fixed.\n\nThe more substantial issue is Theorem 9. It asserts that C2Syn always terminates and returns a SynNNF refinement. The appendix proves termination and argues refinement, but never shows that the constructed DAG is in SynNNF, and the refinement argument leans on Lemma 6(1) whose hypothesis is discharged only by FIND FD pattern matching under an explicit \"assuming all patterns are sound\" caveat. No proof of pattern soundness is given. That is not cosmetic — it is the correctness condition for the main practical contribution. The empirical verifier mitigates it but does not establish the unconditional theorem.\n\nMinor: references [7] and [8] are the same paper listed twice.\n\nBottom line: the theory is solid, the compiler is promising but overclaimed. A serious referee should engage with this; after the Theorem 8 typo is fixed and the FIND FD soundness is either proved or explicitly folded into the theorem statement, this is a strong paper. I would send it to peer review.","headline":"Solid new normal form with a real theorem behind it, but the compiler's correctness (Theorem 9) rests on an unproven pattern-soundness assumption and the Theorem 8 proof has a tautology-level typo that must be fixed.","tokens_in":28506,"tokens_out":2319,"would_cite":true,"duration_ms":24735,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B05","68Q25","68T27"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper introduces SynNNF, a normal form for Boolean specifications in which Skolem functions can always be synthesized in quadratic time, and gives a compiler that refines CNF specifications into this form.","keywords":["Boolean functional synthesis","Skolem functions","knowledge compilation","negation normal form","SynNNF","existential quantification","CNF compilation","refinement"],"falsifier":"Brute-force falsification: enumerate all SynNNF formulas over, say, two outputs and two inputs and compare, by truth table, $\\exists x_1,x_2\\,F(X,Y)$ against $[\\hat{F}]_3[\\bar{X}_2 \\mapsto \\neg X_2]$; any mismatch falsifies Theorem 1. For the compiler, a smaller test is to instantiate one of FIND FD's patterns with variables where the asserted functional equivalence is not entailed and check whether C2Syn's output still satisfies both conditions of Definition 4.","tokens_in":27265,"feed_emoji":"🧮","tokens_out":8819,"duration_ms":81198,"temperature":0.7,"pith_summary":"This paper tries to establish that the representation of a Boolean relational specification can be the deciding factor for Boolean functional synthesis. It introduces SynNNF, a subclass of negation normal form with the property that every specification in SynNNF admits polynomial-time synthesis and polynomial-time existential quantification for a chosen order of output variables. The authors further show that SynNNF is more succinct than earlier normal forms used in knowledge compilation, and they propose an algorithm that refines an input CNF specification into an equivalent-for-synthesis SynNNF form. If the claims hold, any specification that can be brought into SynNNF—or already is in it—can be solved without the exponential blow-up that afflicts general synthesis, and the paper reports that a prototype solves benchmarks beyond existing tools.","feed_headline":"New normal form makes Boolean functional synthesis polynomial-time","feed_subtitle":"A CNF-to-SynNNF compiler brings hundreds of benchmarks within reach, including cases beyond existing solvers.","key_machinery":"The load-bearing object is the SynNNF condition on the $i$-th reduct of the positive form. In plain terms, after fixing earlier outputs to 1 and substituting $\\neg x_j$ for each later output $x_j$, the paper asks whether the remaining formula can behave like the contradictory conjunction $x_i \\wedge \\bar{x}_i$; if for every $i$ no assignment makes it do so, the formula is SynNNF. This condition supplies exactly the missing converse of a monotonicity argument: positive unateness gives one inclusion, and $\\wedge_i$-unrealizability gives the reverse inclusion that turns the cheap GACKS candidate into an exact Skolem function. The refinement relation $\\tilde{F} \\preceq_{\\mathrm{syn}} F$ carries the compilation side, allowing a specification to be replaced by a simpler one whose Skolem functions still satisfy the original; C2Syn combines functional-dependency detection, pivoting on outputs, and decomposed recursion while preserving this relation.","core_discovery":"SynNNF is defined through the positive form $\\hat{F}(X,\\bar{X},Y)$, where negated outputs are replaced by fresh variables. For each output $x_i$, the $i$-th reduct $[\\hat{F}]_i$ sets earlier outputs and their negations to 1 and later outputs to their negated counterparts; the formula is in SynNNF exactly when this reduct is never equivalent to $x_i \\wedge \\bar{x}_i$ (a condition the paper calls $\\wedge_i$-unrealizable). The central theorem is that for a SynNNF specification, existential quantification of the first $i$ outputs is exactly the reduct $[\\hat{F}]_{i+1}$ with later outputs negated, and the GACKS functions—the candidates $[\\hat{F}]_i[x_i \\mapsto 1, \\bar{x}_i \\mapsto 0]$—form a correct Skolem function vector in $O(n^2|F|)$ time and $O(n|F|)$ space. A second characterization theorem shows that a slight relaxation of SynNNF, in which later outputs are replaced by the GACKS candidates, is both necessary and sufficient for GACKS functions to be correct, which explains earlier empirical observations. The paper also proves that a specification has a polynomial-sized Skolem function vector if and only if it has a polynomial-sized refinement in SynNNF, and presents a terminating compiler C2Syn that produces such a refinement for every CNF input.","pith_inferences":["Because Theorem 3(ii) lets correctness of the GACKS vector be checked by one unsatisfiability test, a practical anytime strategy would run that test first and branch only when it fails, potentially eliminating recursion on many instances; the paper does this inside C2Syn but not as a standalone mode.","The MCC decomposition with respect to shared output variables suggests a compositional scheme in which disconnected output groups are compiled in parallel and combined by conjunction; the paper's line 30 already uses this principle for the third component, but it could be pushed to the top level.","The clause-pattern matcher in FDR EFINE currently recognizes eight Boolean functions (and, or, nand, nor, xor, xnor, not, identity); replacing this fixed list with a SAT-based functional-dependency checker would remove the soundness assumption and may find more f-defs, likely improving refinement.","Theorem 8 transfers hardness from synthesis to compilation: whenever Skolem functions are inherently exponential, any SynNNF refinement must also blow up, so C2Syn's practical success on factor-multiplication benchmarks should not be expected to scale to all CNF formulas unless the polynomial hierarchy collapses."],"forward_implications":["Any specification already in SynNNF, or linearly compilable to it (ROBDD/FBDD, DNNF, dDNNF, wDNNF), synthesizes Skolem functions in $O(n^2|F|)$ time using $O(n|F|)$ space.","Existential quantification of a chosen prefix of outputs is linear for SynNNF, so the form is directly usable for image computation and QBF-certificate generation without requiring a full decomposable DNNF.","SynNNF is exponentially more succinct than FBDD and, under standard complexity conjectures, super-polynomially more succinct than dDNNF, DNNF, and wDNNF, so compilation to SynNNF can be much smaller than compilation to these classical targets.","Every specification with a polynomial-sized Skolem function vector has a polynomial-sized refinement in SynNNF, so SynNNF-compilation is complete for tractable synthesis in this sense.","C2Syn always terminates and returns a SynNNF refinement of its input CNF; experimentally it compiles 283 of 402 QBFEVAL benchmarks into SynNNF and can synthesize cases beyond the reach of prior tools."],"supporting_citations":[{"why":"Supplies the GACKS functions and the wDNNF synthesis algorithm whose key step SynNNF makes exact, plus the hardness results used in Theorem 2(iii).","marker":"[1]"},{"why":"Gives the error-formula characterization of Skolem-function correctness used in Theorem 3 and in C2Syn's branch decision.","marker":"[14]"},{"why":"Defines DNNF and gives the linear FBDD-to-DNNF translation that underlies the subsumption argument in Theorem 2(i).","marker":"[9]"},{"why":"Provides dDNNF and DNNF definitions and the polynomial-time model-counting property used to prove SynNNF's succinctness separations.","marker":"[10]"},{"why":"Tseitin encoding is the source of the functionally defined output variables that FDR EFINE detects.","marker":"[26]"},{"why":"Gives lower bounds for FBDD representation of integer multiplication, used to show SynNNF is exponentially more succinct than FBDD.","marker":"[5]"},{"why":"Defines the algebraic class VNP used in the conditional dDNNF succinctness lower bound.","marker":"[27]"},{"why":"Supplies the BDD restriction argument used in the FBDD succinctness proof.","marker":"[4]"}],"fun_headline_variants":["SynNNF: a new normal form for polynomial-time Boolean synthesis","Polynomial-time Boolean synthesis via SynNNF normal form","CNF-to-SynNNF conversion: polynomial-time Boolean synthesis","SynNNF: a normal form that guarantees polynomial-time synthesis","Boolean functional synthesis becomes polynomial with SynNNF"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing assumption is that every clause pattern matched by FDR EFINE really does imply the functional definition it assigns; if one pattern ever recognizes a 'definition' the specification does not entail, the compiled formula could fail to refine the original specification, and the Skolem functions produced from it would no longer be guaranteed correct.","fun_headline_variants_meta":{"raw":{"variants":["SynNNF: a new normal form for polynomial-time Boolean synthesis","Polynomial-time Boolean synthesis via SynNNF normal form","CNF-to-SynNNF conversion: polynomial-time Boolean synthesis","SynNNF: a normal form that guarantees polynomial-time synthesis","Boolean functional synthesis becomes polynomial with SynNNF"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000786,"raw_usage":{"total_tokens":3508,"prompt_tokens":1023,"completion_tokens":2485,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":639,"completion_tokens_details":{"reasoning_tokens":2401}},"tokens_in":639,"tokens_out":2485,"duration_ms":16772,"temperature":1.0,"reasoning_tokens":2401,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T12:52:10.196160+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Brute-force falsification: enumerate all SynNNF formulas over, say, two outputs and two inputs and compare, by truth table, $\\exists x_1,x_2\\,F(X,Y)$ against $[\\hat{F}]_3[\\bar{X}_2 \\mapsto \\neg X_2]$; any mismatch falsifies Theorem 1. For the compiler, a smaller test is to instantiate one of FIND FD's patterns with variables where the asserted functional equivalence is not entailed and check whether C2Syn's output still satisfies both conditions of Definition 4.","supporting_citations":[{"cited_title":"Akshay, Supratik Chakraborty, Shubham Goel, Sumith K ulal, and Shetal Shah","cited_arxiv_id":null,"evidence_quote":"Supplies the GACKS functions and the wDNNF synthesis algorithm whose key step SynNNF makes exact, plus the hardness results used in Theorem 2(iii)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the error-formula characterization of Skolem-function correctness used in Theorem 3 and in C2Syn's branch decision."},{"cited_title":"Decomposable negation normal form","cited_arxiv_id":null,"evidence_quote":"Defines DNNF and gives the linear FBDD-to-DNNF translation that underlies the subsumption argument in Theorem 2(i)."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Tseitin encoding is the source of the functionally defined output variables that FDR EFINE detects."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives lower bounds for FBDD representation of integer multiplication, used to show SynNNF is exponentially more succinct than FBDD."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the algebraic class VNP used in the conditional dDNNF succinctness lower bound."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the BDD restriction argument used in the FBDD succinctness proof."}],"review_version":1}