DROPS

Document

DOI: 10.4230/LIPIcs.SAT.2026.26

On Knowledge Compilation for Two-Variable First-Order Logic

Authors: Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang, and Ondřej Kuželka

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract

Knowledge compilation transforms logical theories into circuit representations that support efficient reasoning. We study this problem for propositional groundings of FO², the two-variable fragment of first-order logic over finite domains. Given an FO² 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 FO² sentence whose grounding over a domain of size n requires DNNF size 2^Ω(n). On the positive side, we develop a two-stage compiler that exploits the symmetries inherent in the propositional groundings of FO² 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.

Cite as

Qiaolan Meng, Juhua Pu, Hongting Niu, Yuyi Wang, Yuanhong Wang, and Ondřej Kuželka. On Knowledge Compilation for Two-Variable First-Order Logic. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{meng_et_al:LIPIcs.SAT.2026.26,
  author =	{Meng, Qiaolan and Pu, Juhua and Niu, Hongting and Wang, Yuyi and Wang, Yuanhong and Ku\v{z}elka, Ond\v{r}ej},
  title =	{{On Knowledge Compilation for Two-Variable First-Order Logic}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{26:1--26:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.26},
  URN =		{urn:nbn:de:0030-drops-263322},
  doi =		{10.4230/LIPIcs.SAT.2026.26},
  annote =	{Keywords: Knowledge Compilation, First-order Logic, SAT}
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.7

Bridging Weighted First Order Model Counting and Graph Polynomials

Authors: Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. It can be solved in time polynomial in the domain size for sentences from the two-variable fragment with counting quantifiers, known as C^2. This polynomial-time complexity is known to be retained when extending C^2 by one of the following axioms: linear order axiom, tree axiom, forest axiom, directed acyclic graph axiom or connectedness axiom. An interesting question remains as to which other axioms can be added to the first-order sentences in this way. We provide a new perspective on this problem by associating WFOMC with graph polynomials. Using WFOMC, we define Weak Connectedness Polynomial and Strong Connectedness Polynomials for first-order logic sentences. It turns out that these polynomials have the following interesting properties. First, they can be computed in polynomial time in the domain size for sentences from C^2. Second, we can use them to solve WFOMC with all of the existing axioms known to be tractable as well as with new ones such as bipartiteness, strong connectedness, having k connected components, etc. Third, the well-known Tutte polynomial can be recovered as a special case of the Weak Connectedness Polynomial, and the Strict and Non-Strict Directed Chromatic Polynomials can be recovered from the Strong Connectedness Polynomials.

Cite as

Qipeng Kuang, Ondřej Kuželka, Yuanhong Wang, and Yuyi Wang. Bridging Weighted First Order Model Counting and Graph Polynomials. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 7:1-7:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuang_et_al:LIPIcs.CSL.2026.7,
  author =	{Kuang, Qipeng and Ku\v{z}elka, Ond\v{r}ej and Wang, Yuanhong and Wang, Yuyi},
  title =	{{Bridging Weighted First Order Model Counting and Graph Polynomials}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{7:1--7:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.7},
  URN =		{urn:nbn:de:0030-drops-254316},
  doi =		{10.4230/LIPIcs.CSL.2026.7},
  annote =	{Keywords: Weighted First-Order Model Counting, Axiom, Enumerative Combinatorics, Tutte Polynomial}
}

Search Results

Documents authored by Kuželka, Ondřej

On Knowledge Compilation for Two-Variable First-Order Logic

Abstract

Cite as

Bridging Weighted First Order Model Counting and Graph Polynomials

Abstract

Cite as

Thanks for your feedback!

Could not send message