arxiv: 2605.11796 · v1 · submitted 2026-05-12 · 💻 cs.LO

Recognition: 1 theorem link

· Lean Theorem

On Knowledge Compilation For Two-Variable First-Order Logic

Qiaolan Meng , Juhua Pu , Hongting Niu , Yuyi Wang , Yuanhong Wang , Ond\v{r}ej Ku\v{z}elka

Authors on Pith no claims yet

Pith reviewed 2026-05-13 04:43 UTC · model grok-4.3

classification 💻 cs.LO

keywords knowledge compilationtwo-variable first-order logicFO2DNNFsymmetrieslifted inferencepropositional grounding

0 comments

The pith

Groundings of some two-variable first-order logic sentences force DNNF circuits to grow exponentially with domain size, but a type-based compiler can still produce compact representations by exploiting symmetries.

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

The paper proves that knowledge compilation of FO2 groundings into DNNF is impossible in general: at least one FO2 sentence produces propositional theories whose smallest DNNF representation grows as 2 to the power of Omega of n. It then presents a two-stage procedure that compiles by branching over unary and binary types instead of individual ground atoms and caches subproblems that remain equivalent under future extensions. Experiments indicate that this yields smaller circuits and faster runtimes than direct grounding baselines for the sentences tested. A reader would care because the result marks a sharp boundary on tractable lifted reasoning while supplying a concrete method that respects that boundary in practice.

Core claim

There exists an FO2 sentence whose grounding over a domain of size n requires DNNF size 2 to the Omega of n. For many other FO2 sentences, however, a two-stage compiler that branches on types and caches residual equivalences constructs compact DNNF circuits whose size and construction time remain practical with respect to n.

What carries the argument

A two-stage compiler that branches on unary and binary types rather than ground atoms and caches residual subproblems equivalent with respect to future extensions.

If this is right

Knowledge compilation of FO2 groundings to DNNF cannot succeed for every sentence because some force exponential circuit size.
Branching over types instead of atoms reduces the decision space from n squared atoms to a constant number of types.
Caching of residual equivalences avoids repeating work on symmetric subproblems.
The resulting circuits are often smaller and compile faster than those obtained by grounding first then compiling.
The same symmetry exploitation may extend to other limited-variable fragments of first-order logic.

Where Pith is reading between the lines

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

Applying the same type branching and caching to OBDD or SDD targets could further enlarge the tractable fragment.
If residual detection remains efficient, the technique could directly support lifted probabilistic inference over relational models with growing domains.
Measuring the growth rate of detected residuals on sentences with increasing numbers of binary predicates would clarify the method's scalability limits.

Load-bearing premise

Symmetries and residual equivalences among FO2 groundings can be detected and cached in time polynomial in the domain size without the detection step itself incurring exponential cost.

What would settle it

Exhibit an FO2 sentence on which the type-branching compiler still produces a DNNF of size exponential in n, or show that residual-equivalence detection requires superpolynomial time on some family of inputs.

read the original abstract

Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO2, the two-variable fragment of first-order logic over finite domains. Given an FO2 sentence and a domain of size n, its grounding yields a propositional theory over ground atoms. We ask whether such theories admit compact representations in DNNF-based and related knowledge compilation languages, and whether these can be constructed efficiently, both with respect to the domain size n for a fixed sentence. We show first that compact compilation is impossible in general: there exists an FO2 sentence whose grounding over a domain of size n requires DNNF size $2^{\Omega(n)}$. On the positive side, we develop a two-stage compiler that exploits the symmetries inherent in the propositional groundings of FO2 sentences. It branches on unary and binary types rather than individual ground atoms, in a similar spirit to lifted inferences for probabilistic relational models. Moreover, it optimizes the compilation process by efficiently identifying and caching residual subproblems that are equivalent with respect to future extensions. Experiments show the practical efficiency of our approach, which often produces smaller circuits and compiles faster than straightforward grounding-based baselines.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

FO2 groundings can force exponential DNNF size, but the type-based compiler with residual caching gives a workable practical route.

read the letter

The paper shows that some FO2 sentences have groundings that require exponentially large DNNFs, and it gives a compiler using types and caching that often works better than basic grounding. The lower bound is the fresh result here. It is a classic-style hardness proof for the two-variable case, which fills a gap left by earlier work on propositional and other fragments. The compiler is the constructive part. It branches on unary and binary types rather than ground atoms and caches residuals that match with respect to later domain growth. This draws from lifted inference but applies it to deterministic NNF construction. Experiments are included and they indicate smaller circuits and quicker compilation times compared to baselines. That adds some practical weight. The soft spot is the runtime of the symmetry detection and caching step. If checking for equivalent residuals involves enumerating many type combinations for sentences with complex binary predicates, the cost could exceed polynomial in n before you even build the circuit. The abstract calls the identification efficient, and the experiments look good, so the paper probably has a polynomial method like type isomorphism checks. Still, it is the part that needs the closest look in the full text. This paper is for researchers in knowledge compilation, lifted probabilistic inference, and relational reasoning systems. Anyone thinking about the scalability of compiling first-order theories to circuits would find it relevant. It has enough new material and supporting evidence to deserve a serious referee.

Referee Report

1 major / 2 minor

Summary. The paper studies knowledge compilation for propositional groundings of FO2 sentences over finite domains of size n. It proves a lower bound establishing that there exists an FO2 sentence whose grounding requires DNNF size 2^Ω(n). On the positive side, it introduces a two-stage compiler that branches on unary and binary types rather than ground atoms and caches residual subproblems equivalent with respect to future domain extensions, claiming this exploits inherent symmetries efficiently; experiments are reported to show smaller circuits and faster compilation than direct grounding baselines.

Significance. The lower bound is a meaningful complexity result, as it demonstrates that even the restricted FO2 fragment can produce groundings whose DNNF representations are exponentially large in the domain size, limiting the applicability of standard knowledge compilation techniques. The algorithmic contribution, if the symmetry detection and caching steps are indeed polynomial-time, would provide a lifted-style method for compiling FO2 groundings that scales with n for fixed sentences, with potential relevance to relational probabilistic inference. The experimental support strengthens the practical case, though the overall significance hinges on rigorous verification of the runtime claims for the equivalence caching mechanism.

major comments (1)

[Section 4 (algorithmic construction)] The positive algorithmic result (two-stage compiler description): the assertion that residual subproblems are 'efficiently' identified and cached lacks an explicit complexity analysis of the equivalence test over unary/binary types. If this test involves enumerating combinations of domain extensions rather than reducing to polynomial-time type isomorphism checks, the overall runtime would not be polynomial in n, directly undermining the claim that the compiler scales with domain size for fixed FO2 sentences.

minor comments (2)

[Abstract] The abstract and introduction could more clearly distinguish the lower-bound construction from the compiler's scope (e.g., which FO2 sentences the positive result applies to).
[Experiments] Experimental section: include controls for the number of binary predicates and domain sizes tested to allow direct comparison with the lower-bound example.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough review and for highlighting the importance of a rigorous complexity analysis for the caching mechanism. We address the major comment below and will revise the manuscript to include the requested details.

read point-by-point responses

Referee: [Section 4 (algorithmic construction)] The positive algorithmic result (two-stage compiler description): the assertion that residual subproblems are 'efficiently' identified and cached lacks an explicit complexity analysis of the equivalence test over unary/binary types. If this test involves enumerating combinations of domain extensions rather than reducing to polynomial-time type isomorphism checks, the overall runtime would not be polynomial in n, directly undermining the claim that the compiler scales with domain size for fixed FO2 sentences.

Authors: We agree that an explicit complexity analysis is required. The equivalence test for residual subproblems does not enumerate domain extensions; instead, it reduces to checking isomorphism between the sets of unary and binary types realized in the current partial grounding. For a fixed FO2 sentence the vocabulary is fixed, so the total number of possible unary and binary types is a constant (independent of n). Type isomorphism can therefore be decided in time linear in the number of realized types, which is O(n) in the worst case but typically much smaller due to the type-based branching. The overall compilation thus remains polynomial in n for fixed sentences. We will add a dedicated paragraph in Section 4 (and a corresponding lemma) spelling out this analysis, including the precise polynomial bound. revision: yes

Circularity Check

0 steps flagged

No significant circularity; results are independent lower bound and algorithmic construction

full rationale

The paper establishes an exponential lower bound on DNNF size for a specific FO2 sentence via direct construction of a hard instance, independent of any fitted parameters or self-referential definitions. The positive result describes a two-stage symmetry-exploiting compiler with caching of equivalent residual subproblems, presented as efficient without any equation or claim reducing the runtime or circuit size back to the input by construction. No load-bearing self-citations, uniqueness theorems from prior author work, or ansatzes smuggled via citation appear in the derivation chain. The approach remains self-contained, with the lower bound and compilation method each having independent content not forced by the other.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claims rest on standard properties of DNNF circuits and FO2 syntax; no free parameters, ad-hoc axioms, or invented entities are introduced in the abstract.

axioms (2)

standard math DNNF is a standard knowledge-compilation language whose size lower bounds are well-defined for propositional formulas
Invoked when stating the 2^Ω(n) size requirement
domain assumption FO2 sentences over finite domains admit a well-defined propositional grounding
Background assumption of the problem setup

pith-pipeline@v0.9.0 · 5524 in / 1300 out tokens · 36057 ms · 2026-05-13T04:43:38.517285+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

two-stage compiler that branches on unary and binary types rather than individual ground atoms... efficiently identifying and caching residual subproblems that are equivalent with respect to future extensions

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

77 extracted references · 77 canonical work pages

[1]

Proceedings of the AAAI Conference on Artificial Intelligence , volume=

Symmetric component caching for model counting on combinatorial instances , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

work page
[2]

Proceedings of the AAAI Conference on Artificial Intelligence , volume=

Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

work page
[3]

IJCAI Proceedings-International Joint Conference on Artificial Intelligence , volume=

SDD: A new canonical representation of propositional knowledge bases , author=. IJCAI Proceedings-International Joint Conference on Artificial Intelligence , volume=

work page
[4]

Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering , pages=

SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications , author=. Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering , pages=

work page
[5]

Knuth , title =

Donald E. Knuth , title =. Commun. 1974 , doi =

work page 1974
[6]

Proceedings of the 26th International Conference on Artificial Intelligence and Statistics (AISTATS) , month = 4, year =

Ahmed, Kareem and Chang, Kai-Wei and Van den Broeck, Guy , title =. Proceedings of the 26th International Conference on Artificial Intelligence and Statistics (AISTATS) , month = 4, year =

work page
[7]

http://starai.cs.ucla.edu/papers/AhmedNeurIPS23.pdf

Ahmed, Kareem and Chang, Kai-Wei and Van den Broeck, Guy , title =. Advances in Neural Information Processing Systems 36 (NeurIPS) , url = "http://starai.cs.ucla.edu/papers/AhmedNeurIPS23.pdf", month = 12, year =

work page
[8]

, year = 2018, series =

Sharma, Shubham and Gupta, Rahul and Roy, Subhajit and Meel, Kuldeep S. , year = 2018, series =. Knowledge

work page 2018
[9]

Dijkstra , title =

Edsger W. Dijkstra , title =. Commun. 1968 , doi =

work page 1968
[10]

1993 , isbn =

Jim Gray and Andreas Reuter , title =. 1993 , isbn =

work page 1993
[11]

1975 , crossref =

On Time versus Space and Related Problems , booktitle =. 1975 , crossref =. doi:10.1109/SFCS.1975.23 , timestamp =

work page doi:10.1109/sfcs.1975.23 1975
[12]

1975 , timestamp =

16th Annual Symposium on Foundations of Computer Science, Berkeley, California, USA, October 13-15, 1975 , publisher =. 1975 , timestamp =

work page 1975
[13]

Structure and Interpretation of Computer Programs

Harold Abelson and Gerald Jay Sussman and Julie Sussman. Structure and Interpretation of Computer Programs. 1985

work page 1985
[14]

2010 , publisher=

Generating random permutations , author=. 2010 , publisher=

work page 2010
[15]

Visual Information Extraction with Lixto

Robert Baumgartner and Georg Gottlob and Sergio Flesca. Visual Information Extraction with Lixto. Proceedings of the 27th International Conference on Very Large Databases. 2001

work page 2001
[16]

Brachman and James G

Ronald J. Brachman and James G. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science. 1985

work page 1985
[17]

Complexity results for nonmonotonic logics

Georg Gottlob. Complexity results for nonmonotonic logics. Journal of Logic and Computation. 1992

work page 1992
[18]

Hypertree Decompositions and Tractable Queries

Georg Gottlob and Nicola Leone and Francesco Scarcello. Hypertree Decompositions and Tractable Queries. Journal of Computer and System Sciences. 2002

work page 2002
[19]

Levesque

Hector J. Levesque. Foundations of a functional approach to knowledge representation. Artificial Intelligence. 1984

work page 1984
[20]

Levesque

Hector J. Levesque. A logic of implicit and explicit belief. Proceedings of the Fourth National Conference on Artificial Intelligence. 1984

work page 1984
[21]

On the compilability and expressive power of propositional planning formalisms

Bernhard Nebel. On the compilability and expressive power of propositional planning formalisms. Journal of Artificial Intelligence Research. 2000

work page 2000
[22]

De Raedt, Luc and Kimmig, Angelika and Toivonen, Hannu , year = 2007, series =

work page 2007
[23]

Encyclopedia of Database Systems , pages=

Probabilistic databases , author=. Encyclopedia of Database Systems , pages=. 2016 , publisher=

work page 2016
[24]

Advances in Neural Information Processing Systems , volume=

Semantic probabilistic layers for neuro-symbolic learning , author=. Advances in Neural Information Processing Systems , volume=

work page
[25]

Journal of Applied Non-Classical Logics , volume =

Adnan Darwiche , title =. Journal of Applied Non-Classical Logics , volume =. 2001 , publisher =. doi:10.3166/jancl.11.11-34 , URL =

work page doi:10.3166/jancl.11.11-34 2001
[26]

Advances in neural information processing systems , volume=

Deepproblog: Neural probabilistic logic programming , author=. Advances in neural information processing systems , volume=

work page
[27]

Kolaitis and Moshe Y

Erich Grädel and Phokion G. Kolaitis and Moshe Y. Vardi , journal =. On the Decision Problem for Two-Variable First-Order Logic , urldate =

work page
[28]

Proceedings of the fourth annual ACM symposium on Theory of computing , pages=

Turing machines and the spectra of first-order formulas with equality , author=. Proceedings of the fourth annual ACM symposium on Theory of computing , pages=

work page
[29]

1991 , url =

Leslie Ann Goldberg , title =. 1991 , url =

work page 1991
[30]

Jan Ramon and Siegfried Nijssen , title =. J. Mach. Learn. Res. , volume =. 2009 , url =. doi:10.5555/1577069.1577102 , timestamp =

work page doi:10.5555/1577069.1577102 2009
[31]

A Circuit-Based Approach to Efficient Enumeration , booktitle =

Antoine Amarilli and Pierre Bourhis and Louis Jachiet and Stefan Mengel , editor =. A Circuit-Based Approach to Efficient Enumeration , booktitle =. 2017 , url =. doi:10.4230/LIPICS.ICALP.2017.111 , timestamp =

work page doi:10.4230/lipics.icalp.2017.111 2017
[32]

Makowsky , title =

Eldar Fischer and Johann A. Makowsky , title =. J. Symb. Log. , volume =. 2004 , url =. doi:10.2178/JSL/1096901758 , timestamp =

work page doi:10.2178/jsl/1096901758 2004
[33]

2007 , url =

Arnaud Durand and Etienne Grandjean , title =. 2007 , url =. doi:10.1145/1276920.1276923 , timestamp =

work page doi:10.1145/1276920.1276923 2007
[34]

Van Den Broeck, Guy and Taghipour, Nima and Meert, Wannes and Davis, Jesse and De Raedt, Luc , year = 2011, series =. Lifted. doi:10.5591/978-1-57735-516-8/IJCAI11-363 , isbn =. 1412.0315 , pages =

work page doi:10.5591/978-1-57735-516-8/ijcai11-363 2011
[35]

2004 , publisher=

Elements of finite model theory , author=. 2004 , publisher=

work page 2004
[36]

Journal of Applied Non-Classical Logics , volume=

On the tractable counting of theory models and its application to truth maintenance and belief revision , author=. Journal of Applied Non-Classical Logics , volume=. 2001 , publisher=

work page 2001
[37]

Artificial Intelligence , volume=

Lifted algorithms for symmetric weighted first-order model sampling , author=. Artificial Intelligence , volume=. 2024 , publisher=

work page 2024
[38]

On Exact Sampling in the Two-Variable Fragment of First-Order Logic , booktitle =

Wang, Yuanhong and Pu, Juhua and Wang, Yuyi and Ku. On Exact Sampling in the Two-Variable Fragment of First-Order Logic , booktitle =. 2023 , month = jun, series =. 2302.02730 , primaryclass =

work page arXiv 2023
[39]

Wang, Yuanhong and. Domain-. Proceedings of the. 2019 , month = oct, volume =

work page 2019
[40]

, biburl =

Scott, D. , biburl =. A decision method for validity of sentences in two variables , username =. Journal of Symbolic Logic , keywords =

work page
[41]

Decidability and the Finite Model Property , urldate =

Alasdair Urquhart , journal =. Decidability and the Finite Model Property , urldate =

work page
[42]

2012 , journal =

Conditioning in. 2012 , journal =. doi:10.1609/aaai.v26i1.8404 , isbn =

work page doi:10.1609/aaai.v26i1.8404 2012
[43]

2004 , publisher=

Combinatorial enumeration , author=. 2004 , publisher=

work page 2004
[44]

2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages=

Towards a more efficient approach for the satisfiability of two-variable logic , author=. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages=. 2021 , organization=

work page 2021
[45]

Mathematical Logic Quarterly , volume=

On languages with two variables , author=. Mathematical Logic Quarterly , volume=. 1975 , publisher=

work page 1975
[46]

International Joint Conference on Automated Reasoning , pages=

A resolution-based decision procedure for the two-variable fragment with equality , author=. International Joint Conference on Automated Reasoning , pages=. 2001 , organization=

work page 2001
[47]

Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems , pages=

Symmetric weighted first-order model counting , author=. Proceedings of the 34th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems , pages=

work page
[48]

Uncertainty in Artificial Intelligence , pages=

Faster lifting for two-variable logic using cell graphs , author=. Uncertainty in Artificial Intelligence , pages=. 2021 , organization=

work page 2021
[49]

arXiv preprint arXiv:1707.07763 , year=

Domain recursion for lifted inference with existential quantifiers , author=. arXiv preprint arXiv:1707.07763 , year=

work page arXiv
[50]

Journal of Artificial Intelligence Research , volume=

Weighted first-order model counting in the two-variable fragment with counting quantifiers , author=. Journal of Artificial Intelligence Research , volume=

work page
[51]

2014 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems , pages=

All-SAT using minimal blocking clauses , author=. 2014 27th International Conference on VLSI Design and 2014 13th International Conference on Embedded Systems , pages=. 2014 , organization=

work page 2014
[52]

Journal of Experimental Algorithmics (JEA) , volume=

Implementing efficient all solutions SAT solvers , author=. Journal of Experimental Algorithmics (JEA) , volume=. 2016 , publisher=

work page 2016
[53]

Journal of the ACM (JACM) , volume=

Solving SAT and SAT modulo theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL (T) , author=. Journal of the ACM (JACM) , volume=. 2006 , publisher=

work page 2006
[54]

Haifa Verification Conference , pages=

Cube and conquer: Guiding CDCL SAT solvers by lookaheads , author=. Haifa Verification Conference , pages=. 2011 , organization=

work page 2011
[55]

Journal of the ACM (JACM) , volume=

Testing first-order properties for subclasses of sparse graphs , author=. Journal of the ACM (JACM) , volume=. 2013 , publisher=

work page 2013
[56]

Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles of database systems , pages=

Enumeration of first-order queries on classes of structures with bounded expansion , author=. Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles of database systems , pages=

work page
[57]

Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems , pages=

Enumerating answers to first-order queries over databases of low degree , author=. Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems , pages=

work page
[58]

A hyperheuristic approach for dynamic enumeration strategy selection in constraint satisfaction , author=. New Challenges on Bioinspired Applications: 4th International Work-conference on the Interplay Between Natural and Artificial Computation, IWINAC 2011, La Palma, Canary Islands, Spain, May 30-June 3, 2011. Proceedings, Part II 4 , pages=. 2011 , orga...

work page 2011
[59]

Annual Symposium on Theoretical Aspects of Computer Science , pages=

Enumerating all solutions for constraint satisfaction problems , author=. Annual Symposium on Theoretical Aspects of Computer Science , pages=. 2007 , organization=

work page 2007
[60]

International Conference on Current Trends in Theory and Practice of Computer Science , pages=

Exhaustive search, combinatorial optimization and enumeration: Exploring the potential of raw computing power , author=. International Conference on Current Trends in Theory and Practice of Computer Science , pages=. 2000 , organization=

work page 2000
[61]

1997 , school=

Algorithmic techniques in verification by explicit state enumeration , author=. 1997 , school=

work page 1997
[62]

International Conference on Theory and Applications of Satisfiability Testing , pages=

A lower bound on DNNF encodings of pseudo-boolean constraints , author=. International Conference on Theory and Applications of Satisfiability Testing , pages=. 2020 , organization=

work page 2020
[63]

Journal of the ACM (JACM) , volume=

Decomposable negation normal form , author=. Journal of the ACM (JACM) , volume=. 2001 , publisher=

work page 2001
[64]

, author=

Knowledge Compilation Meets Communication Complexity. , author=. IJCAI , volume=

work page
[65]

arXiv: Computational Complexity , year=

A Strongly Exponential Separation of DNNFs from CNF Formulas , author=. arXiv: Computational Complexity , year=

work page
[66]

Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity , year=

Meng, Qiaolan and Pu, Juhua and Niu, Hongting and Wang, Yuyi and Wang, Yuanhong and Kuželka, Ondřej , booktitle=. Model Enumeration of Two-Variable Logic with Quadratic Delay Complexity , year=

work page
[67]

Journal of Artificial Intelligence Research , volume=

A knowledge compilation map , author=. Journal of Artificial Intelligence Research , volume=

work page
[68]

Proceedings of the AAAI Conference on Artificial Intelligence , volume=

A compiler for weak decomposable negation normal form , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

work page
[69]

, author=

An Improved Decision-DNNF Compiler. , author=. IJCAI , volume=

work page
[70]

New advances in compiling CNF to decomposable negation normal form , author=. Proc. of ECAI , pages=. 2004 , organization=

work page 2004
[71]

Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence , pages =

Pipatsrisawat, Knot and Darwiche, Adnan , title =. Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence , pages =. 2010 , publisher =

work page 2010
[72]

Proceedings of the 16th International Joint Conference on Artificial Intelligence - Volume 1 , pages =

Darwiche, Adnan , title =. Proceedings of the 16th International Joint Conference on Artificial Intelligence - Volume 1 , pages =. 1999 , publisher =

work page 1999
[73]

Proceedings of the 2010 Conference on ECAI 2010: 19th European Conference on Artificial Intelligence , pages =

Pipatsrisawat, Knot and Darwiche, Adnan , title =. Proceedings of the 2010 Conference on ECAI 2010: 19th European Conference on Artificial Intelligence , pages =. 2010 , isbn =

work page 2010
[74]

Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence , pages =

Faster lifting for two-variable logic using cell graphs , author =. Proceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence , pages =. 2021 , editor =

work page 2021
[75]

and Singh, Guramrit and Dilkas, Paulius and Meel, Kuldeep S

Kidambi, Ananth K. and Singh, Guramrit and Dilkas, Paulius and Meel, Kuldeep S. , title =. 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.SAT.2025.18 , annote =

work page doi:10.4230/lipics.sat.2025.18 2025
[76]

International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

WAPS: Weighted and Projected Sampling , author=. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2019 , organization=

work page 2019
[77]

arXiv preprint arXiv:2202.10025 , year=

CCDD: A tractable representation for model counting and uniform sampling , author=. arXiv preprint arXiv:2202.10025 , year=

work page arXiv