Weighted model counting beyond two-variable logic

DOI10.1145/3209108.3209168MaRDI QIDQ5145338zbMATH OpenOpenAlexWikidataFDO

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)

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

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)

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.

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

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
• Automatic conjecturing of P-recursions using lifted inference
• Weighted first-order model counting in the two-variable fragment with counting quantifiers
• scientific article; zbMATH DE number 1066727 (Why is no real title available?)

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)