Pith. sign in

REVIEW 4 major objections 5 minor 39 references

Knowledge Compilation for Boolean Functional Synthesis

T0 review · 4 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 1908.06275 v1 pith:YUXNRIXH submitted 2019-08-17 cs.LO

S. Akshay , Jatin Arora , Supratik Chakraborty , S. Krishna , Divya Raghunathan , Shetal Shah This is my paper · ORCID
classification cs.LO MSC 03B0568Q2568T27
keywords BooleanfunctionalsynthesisSkolemfunctionsknowledgecompilationnegationnormalformSynNNFexistentialquantificationCNFrefinement
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

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.

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 (4)
  1. [Section IV, proof of Theorem 8] 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.
  2. [Section V / Appendix D, proof of Theorem 9] 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.
  3. [Section V, description of FIND FD before Algorithm 1] 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.
  4. [Appendix B, proof of Theorem 3(i), reverse direction] 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.
minor comments (5)
  1. [Appendix D, proof of Theorem 9] 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).
  2. [References] References [7] and [8] are the same FMCAD 2018 paper (“Functional synthesis via input-output separation”); one of the duplicates should be removed.
  3. [Section V, Algorithm 2, line 25] The definition of S3 ends with a stray semicolon: “S3 := {Ci ∈ S′ | ∀ Cj ∈ Pos ∪ Neg (Ci ≈S′ Cj);”. The semicolon should be removed.
  4. [Section III, proof of Theorem 1(ii)] 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.
  5. [Section VI, verification paragraph] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No circularity found; the paper's central theorems are proved from SynNNF's definition rather than assumed, and self-citations to prior work are not load-bearing.

full rationale

The central derivation is self-contained. SynNNF is defined via the independent ∧i-unrealizability condition on monotone reducts, and Theorem 1 is proved from that condition using positive unateness and the α10/α01 case split; Theorem 3(i) is then an iff, not a restatement of the definition. The GACKS construction comes from the authors' earlier paper [1], but it is re-derived in Theorem 1(ii), and Theorem 3(ii) characterizes its correctness using the independent error-formula criterion of [14]. The succinctness claims of Theorem 2 cite classical external results and the authors' prior hardness theorem; this is ordinary citation, not circularity. The C2Syn development has two real caveats that I flag but do not count as circular: (i) Section V explicitly assumes that FIND FD's clause patterns are sound ("Assuming all patterns used by FIND FD to determine functional dependencies are sound"), and (ii) the proof of Theorem 9 argues termination and refinement but does not explicitly discharge the SynNNF-output property. Neither caveat is an instance of a fitted parameter renamed as a prediction, nor of a theorem equivalent to its input by construction. The empirical verification of 183 of 185 outputs is external checking, not an input to the derivation. Overall, no step in the claimed derivation reduces to its own input.

Assumptions & free parameters 0 free parameters · 4 assumptions · 2 invented entities

This ledger is empty of fitted parameters, because the paper makes no measurement-based claims. The axioms are the standard logical background and the quoted assumptions that the pattern-matching and SAT/2QBF solvers are sound. The only newly introduced formal objects, SynNNF and refinement, are definitions with proven properties and checkable conditions, so they are not ad hoc postulates.

assumptions (4)
  • standard math Standard Boolean NNF and DAG semantics, including the positive form F-hat and constant propagation.
    Used throughout Section II and III; no independent justification needed beyond standard propositional logic.
  • domain assumption Complexity-theoretic conjectures: P != NP, P != VNP, and non-collapse of the polynomial hierarchy.
    Stated as hypotheses for the succinctness separations in Theorem 2(ii) and (iii); they are not needed for the central poly-time synthesis result but underpin the 'more succinct than' claims.
  • ad hoc to paper Soundness of FIND FD clause-pattern matching.
    The text says 'Assuming all patterns used by FIND FD to determine functional dependencies are sound'; this is an unproven implementation assumption needed for Theorem 9 and the C2Syn refinement guarantee.
  • domain assumption SAT and 2QBF solvers used by C2Syn and the verifier return correct results.
    C2Syn line 16 tests unsat of the error formula with a SAT solver, and the verification of Definition 4 requires 2QBF; incorrect solver answers would break the claimed refinement and the experimental verification.
invented entities (2)
  • SynNNF normal form independent evidence
    purpose: A structurally defined subclass of NNF that guarantees polynomial-time Boolean functional synthesis and existential quantification for a chosen output order.
    Definition 3 gives a semantic condition, (w_hat)i-unrealizability, that can be checked or certified; the paper proves theorems about it and C2Syn outputs are checked against it, so it is a falsifiable formal object, not an unobservable postulate.
  • Refinement w.r.t. synthesis independent evidence
    purpose: A relation ~F <syn F that lets a simpler specification replace the original when computing Skolem functions.
    Definition 4 states two semantic conditions checkable by SAT and 2QBF; the paper uses it as the correctness criterion for compilation and gives Proposition 5 and Lemmas 6 and 7 for deriving refinements.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Knowledge Compilation for Boolean Functional Synthesis." pith.science (2026). https://pith.science/paper/YUXNRIXH

@misc{pith2026190806275,
  author       = {Pith},
  title        = {Pith review of: Knowledge Compilation for Boolean Functional Synthesis},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YUXNRIXH}},
  note         = {Machine review of arXiv:1908.06275}
}
read the original abstract

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.

Figures

Figures reproduced from arXiv: 1908.06275 by the authors.

Figure 1
Figure 1. compares the run-times of C2Syn and BDDBFSS : for most QBFEVAL benchmarks that were solved by both, C2Syn took less time, while for FA.QD, C2Syn took more time. There were 130 QBFEVAL benchmarks that C2Syn solved by BDDBFSS couldn’t, whereas 98 were solved by BDDBFSS but not C2Syn. This indicates that the two ap￾proaches to SynNNF compilation have orthogonal strengths. We next compare C2Syn with CADET and BFSS. CADE… view at source ↗
Figure 2
Figure 2. Time comparisons: C2Syn vs CADET (left) and BFSS (right) [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. An edge A → B means that A is a proper subset of B. A blue edge from A to B means B is exponentially more succinct than A, while a red edge from A to B means that unless P = VNP, B is super-polynomially more succinct than A. The green edge from A to B means that unless P = NP, B is super-polynomially more succinct than A. The black edge is the exponential succinctness of DNNF w.r.t FBDD[9]. APPENDIX We present the m… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

39 extracted references · 38 canonical work pages

  1. [8]

    Tabajara, an d Moshe Y

    Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, an d Moshe Y . V ardi. Functional synthesis via input-output separation. In 2018 F ormal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, US A, October 30 - November 2, 2018 , pages 1–9, 2018

    work page 2018

  2. [1]

    Akshay, Supratik Chakraborty, Shubham Goel, Sumith K ulal, and Shetal Shah

    S. Akshay, Supratik Chakraborty, Shubham Goel, Sumith K ulal, and Shetal Shah. What’s Hard About Boolean Functional Synthesi s? In Computer Aided V erification - 30th International Conferenc e, CA V 2018, Held as Part of the Federated Logic Conference, FloC 2018, Ox ford, UK, July 14-17, 2018, Proceedings, Part I , pages 251–269, 2018

    work page 2018

  3. [2]

    Akshay, Supratik Chakraborty, Ajith K

    S. Akshay, Supratik Chakraborty, Ajith K. John, and Shet al Shah. Towards Parallel Boolean Functional Synthesis. In TACAS 2017 Pro- ceedings, Part I , pages 337–353, 2017

    work page 2017

  4. [3]

    G. Boole. The Mathematical Analysis of Logic . Philosophical Library, 1847

    work page

  5. [4]

    R. E. Bryant. Graph-based algorithms for boolean functi on manipula- tion. IEEE Trans. Comput. , 35(8):677–691, August 1986

    work page 1986

  6. [5]

    Randal E. Bryant. On the complexity of VLSI implementati ons and graph representations of boolean functions with applicati on to integer multiplication. IEEE Trans. Computers , 40(2):205–213, 1991

    work page 1991

  7. [6]

    Marco Cadoli and Francesco M. Donini. A survey on knowled ge compilation. AI Commun. , 10(3-4):137–150, 1997

    work page 1997

  8. [9]

    Decomposable negation normal form

    Adnan Darwiche. Decomposable negation normal form. J. ACM , 48(4):608–647, 2001

    work page 2001

Show all 39 references
  1. [10]

    A knowledge compila tion map

    Adnan Darwiche and Pierre Marquis. A knowledge compila tion map. CoRR, abs/1106.1819, 2011

    2011 arXiv

  2. [11]

    Tabajara, and Moshe Y

    Dror Fried, Lucas M. Tabajara, and Moshe Y . V ardi. BDD-b ased boolean functional synthesis. In Computer Aided V erification - 28th International Conference, CA V 2016, Toronto, ON, Canada, J uly 17-23, 2016, Proceedings, Part II , pages 402–421, 2016

    2016

  3. [12]

    J.-H. R. Jiang. Quantifier elimination via functional c omposition. In Proc. of CA V, pages 383–397. Springer, 2009

    2009

  4. [13]

    J.-H. R. Jiang and V Balabanov. Resolution proofs and Sk olem functions in QBF evaluation and applications. In Proc. of CA V, pages 149–164. Springer, 2011

    2011

  5. [14]

    A. John, S. Shah, S. Chakraborty, A. Trivedi, and S. Aksh ay. Skolem functions for factored formulas. In FMCAD, pages 73–80, 2015

    2015

  6. [15]

    Kuncak, M

    V . Kuncak, M. Mayer, R. Piskac, and P . Suter. Complete fu nctional synthesis. SIGPLAN Not. , 45(6):316–329, June 2010

    2010

  7. [16]

    P ropositional independence - formula-variable independence and forgett ing

    J´ erˆ ome Lang, Paolo Liberatore, and Pierre Marquis. P ropositional independence - formula-variable independence and forgett ing. CoRR, abs/1106.4578, 2011

    2011 arXiv

  8. [17]

    Lowenheim

    L. Lowenheim. ¨Uber die Aufl¨ osung von Gleichungen in Logischen Gebietkalkul. Math. Ann. , 68:169–207, 1910

    1910

  9. [18]

    Efficient Ex traction of Skolem Functions from QRA T Proofs

    Martina Seidl Marijn Heule and Armin Biere. Efficient Ex traction of Skolem Functions from QRA T Proofs. In F ormal Methods in Computer- Aided Design, FMCAD 2014, Lausanne, Switzerland, October 2 1-24, 2014, pages 107–114, 2014

    2014

  10. [19]

    Moskewicz, Conor F

    Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lint ao Zhang, and Sharad Malik. Chaff: Engineering an efficient sat solver . In Proceedings of the 38th Annual Design Automation Conferenc e, DAC ’01, pages 530–535, New Y ork, NY , USA, 2001. ACM

    2001

  11. [20]

    McIlraith, J

    Christian Muise, Sheila A. McIlraith, J. Christopher B eck, and Eric Hsu. DSHARP: Fast d-DNNF Compilation with sharpSA T . In AAAI-16 W orkshop on Beyond NP , 2016

    2016

  12. [21]

    QBFEval 2018

    QBFLib. QBFEval 2018. http://www.qbflib.org/qbfeval 18.php

    2018

  13. [22]

    M. N. Rabe and S. A. Seshia. Incremental determinizatio n. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th I nternational Conference, Bordeaux, France, July 5-8, 2016, Proceedings , pages 375– 392, 2016

    2016

  14. [23]

    M. N. Rabe and L. Tentrup. CAQE: A certifying QBF solver. In F ormal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texa s, USA, September 27-30, 2015. , pages 136–143, 2015

    2015

  15. [24]

    Rabe, Leander Tentrup, Cameron Rasmussen, an d Sanjit A

    Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, an d Sanjit A. Seshia. Understanding and extending incremental determin ization for 2qbf. In Computer Aided V erification - 30th International Conferenc e, CA V 2018, Held as Part of the Federated Logic Conference, Flo C 2018,...

    2018

  16. [25]

    Tabajara and Moshe Y

    Lucas M. Tabajara and Moshe Y . V ardi. Factored boolean f unctional synthesis. In 2017 F ormal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, October 2-6, 2017 , pages 124–131, 2017

    2017

  17. [26]

    G. S. Tseitin. On the complexity of derivation in propos itional calculus. Structures in Constructive Mathematics and Mathematical L ogic, Part II, Seminars in Mathematics , pages 115–125, 1968

    1968

  18. [27]

    L. G. V aliant. Completeness classes in algebra. In Proceedings of the Eleventh Annual ACM Symposium on Theory of Computing , STOC ’79, pages 249–261, New Y ork, NY , USA, 1979. ACM. OBDD/FBDD dDNNF DNNF wDNNF SynNNF Fig. 3: An edge A → B means that A is a proper subset of B. ...

    1979

  19. [28]

    If op′ 1 = · · · = op′ n = ∨, then g is in SynNNF

  20. [29]

    If op′ 1 = · · · = op′ n = ⊕, then g is in SynNNF. Proof. 1) Let g be any function in the family with all the op′ i = ∨. It is easy to see that g is in SynNNF, using the sufficient condition in Section III. That is, in [ˆg]1, there is no x1, so we never have a x1 and x1 meeting...

  21. [30]

    Note that in this case, we cannot use the sufficient conditio n as above, clearly,x1, x1 meet at a ∧ in [ˆg]1

    Let g be any function in the family with all the op′ i = ⊕. Note that in this case, we cannot use the sufficient conditio n as above, clearly,x1, x1 meet at a ∧ in [ˆg]1. Neverthelessg is in SynNNF, if we consider [ˆg]i for 1 ≤i ≤n, and consider the root node with children α1 =...

  22. [31]

    If ⋀ yj ∈Y ( F |yj=0 ⇔F |yj=1 ) and π |=F (X, Y), then form(π↓X) ≼ syn F

  23. [32]

    If ⋀ xi∈X (F |xi=0 ⇔F |xi=1), then 1 ≼ syn F

  24. [33]

    negative) unate in xi ∈ X, then xi ∧F |xi=1 (resp

    If F is positive (resp. negative) unate in xi ∈ X, then xi ∧F |xi=1 (resp. ¬xi ∧F |xi=0) ≼ syn F

  25. [34]

    b) (~F1 ∧ ~ F2) ≼ syn (F1 ∧F2) if the output supports of F1 and F2, and similarly of ~ F1 and ~ F2, are disjoint

    If ~ F1 ≼ syn F1 and ~ F2 ≼ syn F2, then a) (~F1 ∨ ~ F2) ≼ syn (F1 ∨F2). b) (~F1 ∧ ~ F2) ≼ syn (F1 ∧F2) if the output supports of F1 and F2, and similarly of ~ F1 and ~ F2, are disjoint. Proof. 1) The reflexivity of ≼ syn follows trivially from Definition 4. To see why ≼ syn is ...

  26. [35]

    Then F is semantically independent of Y and ∀YF (π ↓ X, Y) = 1 holds

    Suppose ⋀ yj ∈Y ( F |yj=0 ⇔F |yj=1 ) and π |= F (X, Y). Then F is semantically independent of Y and ∀YF (π ↓ X, Y) = 1 holds. Therefore, ∀Y∃XF (X, Y) = 1 . Since ∀Y∃Xform(π↓X) = 1 trivially, it follows that ∀Y (∃XF (X, Y) ⇒ ∃X′form(pi↓X)). Therefore condition (a) of Definition ...

  27. [36]

    Then F is semantically independent of X

    Suppose ⋀ xi∈X (F |xi=0 ⇔F |xi=1). Then F is semantically independent of X. Substituting 1 for ~F in condition (a) of Definition 4, we get a tautology. Similarly, substitut ing 1 for ~F in condition (b) of Definition 4, we get ∀Y∀X′ (∃XF (X, Y) ⇒F (X′, Y)). Since F is semantical...

  28. [37]

    It follows that F ⇔ (¬xi∧F |xi=0)∨(x∧F |xi =1) ⇒F |xi=1

    If F is positive unate inxi, thenF |xi=0 ⇒F |xi=1. It follows that F ⇔ (¬xi∧F |xi=0)∨(x∧F |xi =1) ⇒F |xi=1. Therefore, ∀Y ( ∃XF (X, Y) ⇒ ∃X′(x′ i ∧F (X′, Y)|x′ i=1) ) . This proves condition (a) of Definition 4. To show that condi tion (b) of the definition also holds, note that...

  29. [38]

    a) Since ∃X (F1(X, Y) ∨F2(X, Y)) ⇔ (∃XF1(X, Y) ∨ ∃XF2(X, Y)) and ∃X ( ~F1(X, Y) ∨ ~F2(X, Y) ) ⇔( ∃X~F1(X, Y) ∨ ∃X~F2(X, Y) ) , condition (a) of Definition 4 follows immediately

    Suppose ~F1 ≼ syn F1 and ~ F2 ≼ syn F2. a) Since ∃X (F1(X, Y) ∨F2(X, Y)) ⇔ (∃XF1(X, Y) ∨ ∃XF2(X, Y)) and ∃X ( ~F1(X, Y) ∨ ~F2(X, Y) ) ⇔( ∃X~F1(X, Y) ∨ ∃X~F2(X, Y) ) , condition (a) of Definition 4 follows immediately. To see wh y condition (b) of the def- inition holds, notice ...

  30. [39]

    If X = T, then FunT ≼ syn F

  31. [40]

    Similarly, if θF,T,xi,1 is a tautology, then (¬xi ∧F |xi=0) ≼ syn F

    If X \ T ⁄= ∅, then for every xi ∈ X \ T, we have: IfθF,T,xi,0 is a tautology, then (xi ∧F |xi=1) ≼ syn F . Similarly, if θF,T,xi,1 is a tautology, then (¬xi ∧F |xi=0) ≼ syn F . Proof. To prove part (1), notice that F ⇒ FunT. Hence, whenever F (X, Y) is satisfied, each of the f...

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.