Weighted model counting beyond two-variable logic

DOI10.1145/3209108.3209168zbMATH Open1497.68227arXiv1804.10185OpenAlexW2963742388WikidataQ130838827 ScholiaQ130838827MaRDI QIDQ5145338FDOQ5145338

Authors: Antti Kuusisto, Carsten Lutz 

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: It was recently shown by van den Broeck at al. that the symmetric weighted first-order model counting problem (WFOMC) for sentences of two-variable logic FO2 is in polynomial time, while it is Sharp-P_1 complete for some FO3-sentences. We extend the result for FO2 in two independent directions: to sentences of the form "phi and forallexists^=1 psi" with phi and psi in FO2, and to sentences formulated in the uniform one-dimensional fragment of FO, a recently introduced extension of two-variable logic with the capacity to deal with relation symbols of all arities. Note that the former generalizes the extension of FO2 with a functional relation symbol. We also identify a complete classification of first-order prefix classes according to whether WFOMC is in polynomial time or Sharp-P_1 complete.

Full work available at URL: https://arxiv.org/abs/1804.10185

Recommendations

• Weighted first-order model counting in the two-variable fragment with counting quantifiers
• Complexity Results for First-Order Two-Variable Logic with Counting
• Logics with counting and equivalence
• Two-variable first order logic with counting quantifiers: complexity results
• The two-variable fragment with counting and equivalence

zbMATH Keywords

tractabilityenumerative combinatoricstwo-variable logicweighted model counting

Mathematics Subject Classification ID

Model theory of finite structures (03C13) Logic in computer science (03B70) Descriptive complexity and finite models (68Q19) Computational aspects of satisfiability (68R07)

Cited In (6)

• Lifted algorithms for symmetric weighted first-order model sampling
• Counting of Teams in First-Order Team Logics
• Lifted inference with tree axioms
• Weighted First-Order Model Counting in the Two-Variable Fragment With Counting Quantifiers
• Automatic conjecturing of P-recursions using lifted inference
• Title not available (Why is that?)

This page was built for publication: Weighted model counting beyond two-variable logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145338)