Pith. sign in

REVIEW 3 major objections 4 minor 99 references

A Boolean formula can be compiled into a d-DNNF circuit that exists across a cluster—each worker keeps its own fragments—and the same distributed circuit answers counting, sampling, and direct-access queries without ever being assembled in

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review

2026-08-02 04:35 UTC pith:W3VDEKXK

load-bearing objection The distributed compilation half is a solid, reproducible advance; the querying half is not actually tested in the regime that matters, so the abstract oversells. the 3 major comments →

arxiv 2607.13642 v1 pith:W3VDEKXK submitted 2026-07-15 cs.DC

A Distributed Framework for Compiling and Reasoning with d-DNNF

Zhenghang Xu , Minghao Yin , jianan Wang , Jean-Marie Lagniez This is my paper
classification cs.DC
keywords knowledge compilationd-DNNFdistributed reasoningCube-and-Conquermodel countinguniform samplingdirect accessconditioning
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

Knowledge compilation turns a propositional formula into a circuit that supports fast counting and sampling, but building that circuit is expensive and often demands more memory than one machine has. The paper argues that a Cube-and-Conquer split—dividing the formula into disjoint subproblems—lets the compilation run across a cluster while each worker keeps its circuit pieces local. The global circuit is then an implicit deterministic OR over those pieces, and a companion reasoner answers satisfiability, model counting, direct access, and uniform sampling queries on it, even after conditioning on partial assignments. On the 2025 Model Counting Competition benchmarks, the distributed setup with 127 workers solves 113 instances, whereas a strong sequential compiler solves 76.

Core claim

The paper's central claim is that the communication overhead that has kept knowledge compilation single-node can be avoided by never moving circuit fragments. Each worker compiles its assigned cubes into d-DNNF fragments and persists them in a locally ordered list; the global circuit exists virtually as a deterministic OR gate over all those lists (Eq. 3). Because the cubes are pairwise inconsistent and cover the entire solution space, the reconstruction is correct, and because fragments remain local, the circuit can exceed the memory of any single node. The companion reasoner answers counting, direct access, and uniform sampling by broadcasting scalar questions, aggregating scalar answers,

What carries the argument

The key mechanism is the virtual circuit Δ = ∨_j ∨_{Σ∈L_j} Σ, a deterministic OR gate over ordered lists of local d-DNNF fragments. The Cube-and-Conquer decomposition of the formula into disjoint, exhaustive cubes is what makes this OR deterministic and correctness-preserving: every model belongs to exactly one fragment. This decomposition turns distributed compilation into a set of independent sequential compilations and reduces global reasoning to sums (counting), disjunctions (satisfiability), and index routing (direct access and uniform sampling) over the local lists.

Load-bearing premise

Uniform sampling relies on each worker's fragments covering a contiguous interval of the global model ordering; with dynamic dispatch, workers can receive non-contiguous cubes, so the routing step may not yield a uniform sample.

What would settle it

Compile a small formula with a known model set, deliberately dispatch cubes so one worker receives two non-adjacent cubes, then request a large batch of samples and compare the empirical distribution to the true uniform distribution; a significant mismatch would show the sampling guarantee fails.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

Share X Bluesky LinkedIn Reddit HN

If this is right

  • Knowledge compilation can be scaled beyond the memory of any single machine by persisting fragments locally and never gathering the full circuit.
  • The same distributed circuit supports the four standard queries—satisfiability, model counting, direct access, uniform sampling—in polynomial time, including under arbitrary conditioning.
  • With as few as two active workers, the distributed compiler overtakes the sequential baseline on the MC 2025 benchmark set, and with 127 workers it solves 113 instances versus 76.
  • Query overhead dominates for lightweight, sub-second queries; the distributed reasoner is most beneficial when the compiled circuit is too large for one machine.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The uniform-sampling router assumes the models of each worker form a contiguous interval in the global order; making this assumption explicit and enforcing contiguity at cube-assignment time would turn a heuristic into a provable guarantee.
  • The same virtual-circuit design—a deterministic root OR over locally stored fragments—should transplant to other compilation targets that support deterministic disjunction, such as BDDs or SDDs, giving them distributed query engines too.
  • The direct-access price of one broadcast count per variable suggests a speculative prefetching protocol could cut the round-trip count; the paper lists this as future work, but a concrete bound on the resulting speedup is a natural next test.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. dkc is presented as the first distributed d-DNNF compiler. It uses Cube-and-Conquer to partition the input CNF into disjoint cubes; each worker compiles its assigned cube with d4, stores the fragment locally in an ordered list, and never ships the circuit to the Master. The global circuit is virtualized as a deterministic OR of the local fragments (Eq. 3). dreasoner then supports satisfiability, model counting, direct access, and uniform sampling, with or without conditioning, by broadcasting queries and aggregating scalar results; sampling routes a random global index to a worker via per-worker counts. Experiments on MC 2025 show that dkc with 127 workers solves 113 instances versus 76 for sequential d4. Query experiments on a subset of 200 tractable instances compare the 128-core reasoner with d4 and show mixed results, with communication overhead dominating small queries.

Significance. If the correctness and scope issues below are addressed, this is a valuable contribution. Extending Cube-and-Conquer from transient #SAT to persistent compilation avoids the circuit-fragment communication bottleneck, and the distributed query algorithms (especially counting and routing-based sampling) are natural and potentially impactful. The reported compilation scalability is substantial, and the release of code and logs is a concrete reproducibility strength. The main scientific claim about querying formulas beyond sequential reach, however, is not yet supported by the experiments as designed.

major comments (3)
  1. [§3.2, Eq. (3)] The equivalence ∆≡Ψ is asserted but not established for the fragment representation as described. If a worker compiles the §2.1-style conditioned formula, the literals of cube τ are replaced/simplified away, and the fragment does not entail τ. Then the OR of local fragments is generally not equivalent to Ψ over Var(Ψ). Example: Ψ=(a∨d)∧(¬b∨c), cubes {a} and {¬a}; the residual fragments are (¬b∨c) and d∧(¬b∨c), whose OR is (¬b∨c), which is not Ψ. To validate Eq. (3), each stored fragment must be compiled from the un-simplified conjunction Ψ∧τ over all variables, or each fragment must be paired/conjoined with its cube. The reasoner must also handle variables that are absent from a fragment but appear in a conditioning set γ. This issue is load-bearing for §4.
  2. [§5.3, Figure 4] The query evaluation is restricted to instances 'tractable for compilation' and to those solved by both d4 and dkc; 116 of 200 compile in under one second. No query timings or memory data are given for the MC 2025 instances that dkc_128 solves but d4_seq does not (37 instances). The abstract's claim that the architecture enables 'compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers' is therefore supported only for compilation. Add query experiments on at least a few dkc-only instances, with per-worker circuit sizes and peak memory, or narrow the claim.
  3. [§5.2, Figures 1–3] No memory measurements are reported. The motivation for the distributed representation is overcoming the single-node memory wall, yet the paper gives no per-worker fragment sizes, no aggregate virtual-circuit size, and no instance where d4_seq hits the 32 GiB limit while dkc completes. Without these, the 'beyond the reach' narrative rests on solve counts alone. Report memory data for the solved instances, particularly the dkc-only ones.
minor comments (4)
  1. [§4.2 / Algorithm 2] The uniform-sampling routing is correct without assuming global lexicographic contiguity of a worker's models; a uniform global index s mapped to a local index in any fixed local enumeration is uniform because each model occurs exactly once in the union of local enumerations. Please state this argument and remove the misleading emphasis on 'owns' the s-th solution and on strict order being 'crucial' for direct access.
  2. [§5.3] The random selection of 200 instances needs a seed and a precise procedure for reproducibility.
  3. [Algorithm 2, line 25] #SAT(∆∧γ) is defined as a scalar in Eq. (5); the sampling path also needs per-worker partial counts {c_j}. Specify that workers return these counts.
  4. [Abstract, passim] Formatting artifacts such as 'proposedkc' and 'introducedreasoner' should be fixed.

Circularity Check

0 steps flagged

No significant circularity: core correctness argument is self-contained; self-citations provide prior tools, not load-bearing premises.

full rationale

The derivation chain is not circular. Equation (3) constructs the virtual d-DNNF as the deterministic disjunction of independently compiled local fragments, and its correctness is justified directly from the Cube-and-Conquer properties of coverage and pairwise disjointness; no quantity is fitted from query data. The reasoning algorithms (Eqs. 4-5 and Algorithm 2) are standard reductions to local d-DNNF operations, and uniform sampling uses prefix sums as a fixed index-to-model bijection, so uniformity is preserved by construction. Self-citations such as DisCount, d4, and the JELIA 2025 query benchmark supply implementation scaffolding, a worker compiler, and a workload; they are not used as unverified uniqueness theorems or as smuggled ansatz. The main weakness, namely that query evaluation is only measured on instances tractable for both solvers and does not test the memory-exceeding regime, is an empirical scoping limitation, not a circular reduction.

Axiom & Free-Parameter Ledger

1 free parameters · 3 axioms · 0 invented entities

The framework's correctness rests on the standard cube-and-conquer disjoint-cover property and on d4's correctness. The only ad hoc assumption is the implicit contiguity of per-worker model sets needed for the sampling router. No new theoretical entities are introduced.

free parameters (1)
  • nbCubes
    Granularity factor controlling number of cubes (nbCubes × |W|); value is not reported. Affects load balance and communication overhead, but not the core correctness claim.
axioms (3)
  • domain assumption Cube-and-Conquer partition: cubes τ are pairwise disjoint and cover the solution space (Ψ ≡ ∨_τ (Ψ∧τ)).
    Used in Eq. (1) and correctness of virtual circuit Eq. (3); inherited from DisCount and standard in cube-and-conquer solvers.
  • domain assumption d-DNNF fragments produced by d4 are correct and support conditioning and counting in linear time.
    Workers rely on d4 producing valid decision-DNNFs for each cube (Section 3.2/5.1).
  • ad hoc to paper Global lexicographic order of models can be recovered from per-worker counts and local indices.
    Uniform sampling and direct-access routing in Section 4.2 require that each worker's model set is a contiguous interval in the global order; this is not stated or derived.

reviewed 2026-08-02 · how reviews work

0 comments
Cite this review

Pith. "Pith review of A Distributed Framework for Compiling and Reasoning with d-DNNF." pith.science (2026). https://pith.science/paper/W3VDEKXK

@misc{pith2026260713642,
  author       = {Pith},
  title        = {Pith review of: A Distributed Framework for Compiling and Reasoning with d-DNNF},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/W3VDEKXK}},
  note         = {Machine review of arXiv:2607.13642}
}
Share X Bluesky LinkedIn Reddit HN
read the original abstract

Knowledge Compilation (KC) is a powerful paradigm that enables efficient reasoning by transforming propositional formulas into tractable target languages, such as Deterministic, Decomposable Negation Normal Form (d-DNNF). However, as real-world problem instances grow in complexity, the offline compilation phase becomes a significant computational bottleneck, often exceeding the memory and temporal limits of single-node systems. While distributed computing has been successfully applied to model counting ($\#\mathsf{SAT}$), extending these techniques to knowledge compilation remains a challenge due to the difficulty of sharing partial circuit fragments across distributed nodes. In this paper, we propose dkc, the first distributed knowledge compiler designed for large-scale Decision-DNNF generation. Leveraging a Cube-and-Conquer strategy, dkc effectively partitions the search space into independent subproblems, mitigating the communication overhead typically associated with work-stealing architectures in circuit-based tasks. Recognizing that the utility of compilation lies in subsequent querying, we further introduce dreasoner, a distributed reasoning engine. dreasoner is capable of performing core inference tasks (including model counting, direct access, and uniform sampling) across a distributed d-DNNF structure, even under variable conditioning. Our experimental evaluation on benchmarks demonstrates that our distributed architecture scales effectively, enabling the compilation and querying of complex formulas that remain beyond the reach of state-of-the-art sequential compilers.

Figures

Figures reproduced from arXiv: 2607.13642 by Jean-Marie Lagniez, Jianan Wang, Minghao Yin, Zhenghang Xu.

Figure 1
Figure 1. Figure 1: Performance comparison of the model counters [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Distribution of speedups achieved by dkc across varying core counts, normalized against the minimal distributed configura￾tion (1 Master + 1 Worker). a conservative lower bound on the actual speedup for any instance that times out in the baseline configuration. The results demonstrate robust scalability. We observe a consistent upward trend in the median speedup (orange line) as the core count increases, c… view at source ↗
Figure 4
Figure 4. Figure 4: Scatter plot comparing the 4 different queries times of [PITH_FULL_IMAGE:figures/full_fig_p009_4.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

99 extracted references · 23 canonical work pages · 2 internal anchors

  1. [1]

    Cook , editor =

    Stephen A. Cook , editor =. The Complexity of Theorem-Proving Procedures , booktitle =. 1971 , url =. doi:10.1145/800157.805047 , timestamp =

    arXiv 1971

  2. [2]

    The Thirteenth International Conference on Learning Representations,

    Jaron Maene and Vincent Derkinderen and Pedro Zuidberg Dos Martires , title =. The Thirteenth International Conference on Learning Representations,. 2025 , url =

    2025

  3. [3]

    Quentin Plazar and Mathieu Acher and Gilles Perrouin and Xavier Devroey and Maxime Cordy , title =. 12th. 2019 , url =. doi:10.1109/ICST.2019.00032 , timestamp =

    arXiv 2019

  4. [4]

    Binary Decision Diagram Algorithms to Perform Hard Analysis Operations on Variability Models , booktitle =

    Ruben Heradio and Hector Perez. Binary Decision Diagram Algorithms to Perform Hard Analysis Operations on Variability Models , booktitle =. 2016 , url =. doi:10.3233/978-1-61499-674-3-139 , timestamp =

    work page doi:10.3233/978-1-61499-674-3-139 2016

  5. [5]

    CaDiCaL 2.0 , booktitle =

    Armin Biere and Tobias Faller and Katalin Fazekas and Mathias Fleury and Nils Froleyks and Florian Pollitt , editor =. CaDiCaL 2.0 , booktitle =

  6. [6]

    Michael Hamann and Ben Strasser , title =

  7. [7]

    Definability for model counting , journal =

    Jean. Definability for model counting , journal =

  8. [8]

    On Preprocessing Techniques and Their Impact on Propositional Model Counting , journal =

    Jean. On Preprocessing Techniques and Their Impact on Propositional Model Counting , journal =

  9. [9]

    Evaluating State-of-the-Art

    Chico Sundermann and Tobias He. Evaluating State-of-the-Art. Software Engineering 2024, Fachtagung des GI-Fachbereichs Softwaretechnik, Linz, Austria, February 26 - March 1, 2024 , series =. 2024 , url =. doi:10.18420/SW2024\_18 , timestamp =

    work page doi:10.18420/sw2024 2024

  10. [10]

    Model Counting in Product Configuration , booktitle =

    Andreas K. Model Counting in Product Configuration , booktitle =. 2010 , url =. doi:10.4204/EPTCS.29.5 , timestamp =

    work page doi:10.4204/eptcs.29.5 2010

  11. [11]

    An Improved

    Anicet Bart and Fr. An Improved. 2016 , url =. doi:10.3233/978-1-61499-672-9-613 , timestamp =

    work page doi:10.3233/978-1-61499-672-9-613 2016

  12. [12]

    Mark Chavira and Adnan Darwiche , title =. Artif. Intell. , volume =. 2008 , url =. doi:10.1016/J.ARTINT.2007.11.002 , timestamp =

    doi:10.1016/j.artint.2007.11.002 2008

  13. [13]

    Batory , editor =

    Jeho Oh and Paul Gazzillo and Don S. Batory , editor =. Proceedings of the 23rd International Systems and Software Product Line Conference,. 2019 , url =. doi:10.1145/3336294.3342359 , timestamp =

    arXiv 2019

  14. [14]

    Meel and Prateek Saxena , title =

    Teodora Baluta and Zheng Leong Chua and Kuldeep S. Meel and Prateek Saxena , title =. 43rd. 2021 , url =. doi:10.1109/ICSE43902.2021.00039 , timestamp =

    arXiv 2021

  15. [15]

    Alistair Sinclair and Mark Jerrum , title =. Inf. Comput. , volume =. 1989 , url =. doi:10.1016/0890-5401(89)90067-9 , timestamp =

    doi:10.1016/0890-5401(89)90067-9 1989

  16. [16]

    Computing the jth solution of a first-order query , journal =

    Guillaume Bagan and Arnaud Durand and Etienne Grandjean and Fr. Computing the jth solution of a first-order query , journal =. 2008 , url =. doi:10.1051/ITA:2007046 , timestamp =

    doi:10.1051/ita:2007046 2008

  17. [17]

    2025 , url =

    Karl Bringmann and Nofar Carmeli and Stefan Mengel , title =. 2025 , url =. doi:10.1145/3707448 , timestamp =

    doi:10.1145/3707448 2025

  18. [18]

    On Tractable

    Gilles Audemard and Fr. On Tractable. Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning,. 2020 , url =. doi:10.24963/KR.2020/86 , timestamp =

    work page doi:10.24963/kr.2020/86 2020

  19. [19]

    Database Theory in Action: Making Provenance and Probabilistic Database Theory Work in Practice (Invited Talk) , booktitle =

    Silviu Maniu and Pierre Senellart , editor =. Database Theory in Action: Making Provenance and Probabilistic Database Theory Work in Practice (Invited Talk) , booktitle =. 2025 , url =. doi:10.4230/LIPICS.ICDT.2025.33 , timestamp =

    work page doi:10.4230/lipics.icdt.2025.33 2025

  20. [20]

    Pierre Senellart and Louis Jachiet and Silviu Maniu and Yann Ramusat , title =. Proc. 2018 , url =. doi:10.14778/3229863.3236253 , timestamp =

    arXiv 2018

  21. [21]

    Green and Gregory Karvounarakis and Val Tannen , editor =

    Todd J. Green and Gregory Karvounarakis and Val Tannen , editor =. Provenance semirings , booktitle =. 2007 , url =. doi:10.1145/1265530.1265535 , timestamp =

    arXiv 2007

  22. [22]

    Reasoning on Feature Models: Compilation-Based vs. Direct Approaches

    Pierre Bourhis and Laurence Duchien and J. Reasoning on Feature Models: Compilation-Based vs. Direct Approaches , journal =. 2023 , url =. doi:10.48550/ARXIV.2302.06867 , eprinttype =. 2302.06867 , timestamp =

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2302.06867 2023

  23. [23]

    Efficient Slicing of Feature Models via Projected d-

    Chico Sundermann and Jacob Loth and Thomas Th. Efficient Slicing of Feature Models via Projected d-. Proceedings of the 39th. 2024 , url =. doi:10.1145/3691620.3695594 , timestamp =

    arXiv 2024

  24. [24]

    Reusing d-

    Chico Sundermann and Heiko Raab and Tobias He. Reusing d-. 2024 , url =. doi:10.1145/3680465 , timestamp =

    doi:10.1145/3680465 2024

  25. [25]

    DeepProbLog: Neural Probabilistic Logic Programming , booktitle =

    Robin Manhaeve and Sebastijan Dumancic and Angelika Kimmig and Thomas Demeester and Luc De Raedt , editor =. DeepProbLog: Neural Probabilistic Logic Programming , booktitle =. 2018 , url =

    2018

  26. [26]

    Constraint-based Vehicle Configuration:

    Jean. Constraint-based Vehicle Configuration:. 22nd. 2010 , url =. doi:10.1109/ICTAI.2010.19 , timestamp =

    work page doi:10.1109/ictai.2010.19 2010

  27. [27]

    New Advances in Compiling

    Adnan Darwiche , editor =. New Advances in Compiling. Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI'2004, including Prestigious Applicants of Intelligent Systems,. 2004 , timestamp =

    2004

  28. [28]

    1997 , url =

    Eric Lehman and Yosinori Watanabe and Joel Grodstein and Heather Harkness , title =. 1997 , url =. doi:10.1109/43.644605 , timestamp =

    work page doi:10.1109/43.644605 1997

  29. [29]

    Ganai , title =

    Andreas Kuehlmann and Viresh Paruthi and Florian Krohm and Malay K. Ganai , title =

  30. [30]

    Enhancing Query Efficiency for

    Jean. Enhancing Query Efficiency for. Logics in Artificial Intelligence - 19th European Conference,. 2025 , url =. doi:10.1007/978-3-032-04590-4\_9 , timestamp =

    work page doi:10.1007/978-3-032-04590-4 2025

  31. [31]

    Chandra and Mark N

    Manuel Blum and Ashok K. Chandra and Mark N. Wegman , title =. Inf. Process. Lett. , volume =

  32. [32]

    Testing Equivalence Probabilistically , author =

  33. [33]

    Vincent Derkinderen , title =. 36th. 2024 , url =. doi:10.1109/ICTAI62512.2024.00099 , timestamp =

    arXiv 2024

  34. [34]

    2005 , url =

    FRAIGs: A Unifying Representation for Logic Synthesis and Verification , author =. 2005 , url =

    2005

  35. [35]

    Bounded Model Checking , booktitle =

    Armin Biere , editor =. Bounded Model Checking , booktitle =. 2021 , url =. doi:10.3233/FAIA201002 , timestamp =

    doi:10.3233/faia201002 2021

  36. [36]

    2012 , isbn =

    Reinhard Diestel , title =. 2012 , isbn =

    2012

  37. [37]

    Goldberg and Mukul R

    Evguenii I. Goldberg and Mukul R. Prasad and Robert K. Brayton , editor =. Using. Proceedings of the Conference on Design, Automation and Test in Europe,. 2001 , url =. doi:10.1109/DATE.2001.915010 , timestamp =

    arXiv 2001

  38. [38]

    Learning a Propagation Complete Formula , booktitle =

    Ku. Learning a Propagation Complete Formula , booktitle =. 2022 , publisher =

    2022

  39. [39]

    Parameterized Compilation Lower Bounds for Restricted

    Stefan Mengel , year =. Parameterized Compilation Lower Bounds for Restricted. 1604.06715 , archiveprefix =

    Pith/arXiv arXiv

  40. [40]

    , title =

    Schaefer, Thomas J. , title =. 1978 , isbn =. doi:10.1145/800133.804350 , booktitle =

    arXiv 1978

  41. [41]

    Shannon , title =

    Claude E. Shannon , title =. Bell Syst. Tech. J. , volume =. 1949 , url =. doi:10.1002/J.1538-7305.1949.TB03624.X , timestamp =

    arXiv 1949

  42. [42]

    Knowledge Compilation for Model Counting: Affine Decision Trees , booktitle =

    Fr. Knowledge Compilation for Model Counting: Affine Decision Trees , booktitle =. 2013 , url =

    2013

  43. [43]

    On Compiling

    Umut Oztok and Adnan Darwiche , editor =. On Compiling. Principles and Practice of Constraint Programming - 20th International Conference,. 2014 , url =. doi:10.1007/978-3-319-10428-7\_7 , timestamp =

    work page doi:10.1007/978-3-319-10428-7 2014

  44. [44]

    CV-width:

    Umut Oztok and Adnan Darwiche , editor =. CV-width:. 2014 , url =. doi:10.3233/978-1-61499-419-0-675 , timestamp =

    work page doi:10.3233/978-1-61499-419-0-675 2014

  45. [45]

    Cliquewidth and Knowledge Compilation , booktitle =

    Igor Razgon and Justyna Petke , editor =. Cliquewidth and Knowledge Compilation , booktitle =. 2013 , url =. doi:10.1007/978-3-642-39071-5\_25 , timestamp =

    doi:10.1007/978-3-642-39071-5 2013

  46. [46]

    Adnan Darwiche , title =. J. Appl. Non Class. Logics , volume =. 2001 , url =. doi:10.3166/JANCL.11.11-34 , timestamp =

    doi:10.3166/jancl.11.11-34 2001

  47. [47]

    Plaisted , editor =

    David A. Plaisted , editor =. History and Prospects for First-Order Automated Deduction , booktitle =. 2015 , url =. doi:10.1007/978-3-319-21401-6\_1 , timestamp =

    doi:10.1007/978-3-319-21401-6 2015

  48. [48]

    Knowledge Compilation Meets Communication Complexity , booktitle =

    Simone Bova and Florent Capelli and Stefan Mengel and Friedrich Slivovsky , editor =. Knowledge Compilation Meets Communication Complexity , booktitle =. 2016 , url =

    2016

  49. [49]

    2017 , url =

    Paul Beame and Jerry Li and Sudeepa Roy and Dan Suciu , title =. 2017 , url =. doi:10.1145/2984632 , timestamp =

    work page doi:10.1145/2984632 2017

  50. [50]

    32nd Annual

    Florent Capelli , title =. 32nd Annual. 2017 , url =. doi:10.1109/LICS.2017.8005121 , timestamp =

    arXiv 2017

  51. [51]

    On Compiling

    Simone Bova and Florent Capelli and Stefan Mengel and Friedrich Slivovsky , editor =. On Compiling. Theory and Applications of Satisfiability Testing -. 2015 , url =. doi:10.1007/978-3-319-24318-4\_15 , timestamp =

    doi:10.1007/978-3-319-24318-4 2015

  52. [52]

    Tractable

    Florent Capelli and Stefan Mengel , editor =. Tractable. 36th International Symposium on Theoretical Aspects of Computer Science,. 2019 , url =. doi:10.4230/LIPICS.STACS.2019.18 , timestamp =

    work page doi:10.4230/lipics.stacs.2019.18 2019

  53. [53]

    Giuseppe Marra and Sebastijan Dumancic and Robin Manhaeve and Luc De Raedt , title =. Artif. Intell. , volume =. 2024 , url =. doi:10.1016/J.ARTINT.2023.104062 , timestamp =

    arXiv 2024

  54. [54]

    38th Annual

    Adnan Darwiche , title =. 38th Annual. 2023 , url =. doi:10.1109/LICS56636.2023.10175757 , timestamp =

    arXiv 2023

  55. [55]

    CoRR , volume =

    Simone Bova and Florent Capelli and Stefan Mengel and Friedrich Slivovsky , title =. CoRR , volume =. 2014 , url =. 1411.1995 , timestamp =

    Pith/arXiv arXiv 2014

  56. [56]

    Cooper and Nicholas Asher and Jo

    Xuanxiang Huang and Yacine Izza and Alexey Ignatiev and Martin C. Cooper and Nicholas Asher and Jo. Efficient Explanations for Knowledge Compilation Languages , journal =. 2021 , url =. 2107.01654 , timestamp =

    Pith/arXiv arXiv 2021

  57. [57]

    Semantic Loss Functions for Neuro-Symbolic Structured Prediction , booktitle =

    Kareem Ahmed and Stefano Teso and Paolo Morettin and Luca Di Liello and Pierfrancesco Ardino and Jacopo Gobbi and Yitao Liang and Eric Wang and Kai. Semantic Loss Functions for Neuro-Symbolic Structured Prediction , booktitle =. 2023 , url =. doi:10.3233/FAIA230154 , timestamp =

    work page doi:10.3233/faia230154 2023

  58. [58]

    Solving PP\(

    Umut Oztok and Arthur Choi and Adnan Darwiche , editor =. Solving PP\(. Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference,. 2016 , url =

    2016

  59. [59]

    Adnan Darwiche , title =. Commun. 2010 , url =. doi:10.1145/1859204.1859227 , timestamp =

    arXiv 2010

  60. [60]

    Valiant , title =

    Leslie G. Valiant , title =. Theor. Comput. Sci. , volume =. 1979 , url =. doi:10.1016/0304-3975(79)90044-6 , timestamp =

    doi:10.1016/0304-3975(79)90044-6 1979

  61. [61]

    Knowledge Compilation Languages as Proof Systems , booktitle =

    Florent Capelli , editor =. Knowledge Compilation Languages as Proof Systems , booktitle =. 2019 , url =. doi:10.1007/978-3-030-24258-9\_6 , timestamp =

    doi:10.1007/978-3-030-24258-9 2019

  62. [62]

    Certifying Top-Down Decision-

    Florent Capelli and Jean. Certifying Top-Down Decision-. Thirty-Fifth. 2021 , url =. doi:10.1609/AAAI.V35I7.16776 , timestamp =

    work page doi:10.1609/aaai.v35i7.16776 2021

  63. [63]

    Certified Knowledge Compilation with Application to Formally Verified Model Counting

    Randal E. Bryant and Wojciech Nawrocki and Jeremy Avigad and Marijn J. H. Heule , title =. CoRR , volume =. 2025 , url =. doi:10.48550/ARXIV.2501.12906 , eprinttype =. 2501.12906 , timestamp =

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2501.12906 2025

  64. [64]

    A Circuit

    Feng Lu and Li. A Circuit. 2003 Design, Automation and Test in Europe Conference and Exposition. 2003 , url =. doi:10.1109/DATE.2003.10018 , timestamp =

    Pith/arXiv arXiv 2003

  65. [65]

    1991 , url =

    Seinosuke Toda , title =. 1991 , url =. doi:10.1137/0220053 , timestamp =

    doi:10.1137/0220053 1991

  66. [66]

    2004 International Conference on Computer-Aided Design,

    Andreas Kuehlmann , title =. 2004 International Conference on Computer-Aided Design,. 2004 , url =. doi:10.1109/ICCAD.2004.1382542 , timestamp =

    Pith/arXiv arXiv 2004

  67. [67]

    Muise and Sheila A

    Christian J. Muise and Sheila A. McIlraith and J. Christopher Beck and Eric I. Hsu , editor =. Dsharp: Fast. Advances in Artificial Intelligence - 25th Canadian Conference on Artificial Intelligence, Canadian. 2012 , url =. doi:10.1007/978-3-642-30353-1\_36 , timestamp =

    work page doi:10.1007/978-3-642-30353-1 2012

  68. [68]

    Knowledge Compilation and More with

    Rafael Kiesel and Thomas Eiter , editor =. Knowledge Compilation and More with. Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning,. 2023 , url =. doi:10.24963/KR.2023/40 , timestamp =

    work page doi:10.24963/kr.2023/40 2023

  69. [69]

    A Billion

    Neha Rungta , editor =. A Billion. Computer Aided Verification - 34th International Conference,. 2022 , url =. doi:10.1007/978-3-031-13185-1\_1 , timestamp =

    doi:10.1007/978-3-031-13185-1 2022

  70. [70]

    2013 , eprint =

    Lower Bounds for Exact Model Counting and Applications in Probabilistic Databases , author =. 2013 , eprint =

    2013

  71. [71]

    1997 , issn =

    Natural Proofs , journal =. 1997 , issn =. doi:https://doi.org/10.1006/jcss.1997.1494 , url =

    arXiv 1997

  72. [72]

    2021 , eprint =

    Learning with distributional inverters , author =. 2021 , eprint =

    2021

  73. [73]

    Carmosino and Russell Impagliazzo and Valentine Kabanets and Antonina Kolokolova , editor =

    Marco L. Carmosino and Russell Impagliazzo and Valentine Kabanets and Antonina Kolokolova , editor =. Learning Algorithms from Natural Proofs , booktitle =. 2016 , url =. doi:10.4230/LIPICS.CCC.2016.10 , timestamp =

    work page doi:10.4230/lipics.ccc.2016.10 2016

  74. [74]

    Oliveira , editor =

    Rahul Ilango and Bruno Loff and Igor C. Oliveira , editor =. NP-Hardness of Circuit Minimization for Multi-Output Functions , booktitle =. 2020 , url =. doi:10.4230/LIPICS.CCC.2020.22 , timestamp =

    doi:10.4230/lipics.ccc.2020.22 2020

  75. [75]

    Rahul Ilango , title =. 64th. 2023 , url =. doi:10.1109/FOCS57990.2023.00048 , timestamp =

    arXiv 2023

  76. [76]

    Universal search problems , year =

    Leonid Anatolevich Levin , journal =. Universal search problems , year =

  77. [77]

    Scott , journal =

    Norman R. Scott , journal =. A new approach to the design of switching circuits , year =

  78. [78]

    Ashenhurst , journal =

    Robert L. Ashenhurst , journal =. The decomposition of switching functions , year =

  79. [79]

    On the Use of Partially Ordered Decision Graphs in Knowledge Compilation and Quantified Boolean Formulae , booktitle =

    H. On the Use of Partially Ordered Decision Graphs in Knowledge Compilation and Quantified Boolean Formulae , booktitle =. 2006 , url =

    2006

  80. [80]

    Improvements to Satisfiability-Based Boolean Function Bi-Decomposition , booktitle =

    Huan Chen and Jo. Improvements to Satisfiability-Based Boolean Function Bi-Decomposition , booktitle =. 2011 , url =. doi:10.1007/978-3-642-32770-4\_4 , timestamp =

    work page doi:10.1007/978-3-642-32770-4 2011

Showing first 80 references.

This paper was first reviewed by deepseek-v4-flash on August 2, 2026.