Towards Practical First-Order Model Counting Article Swipe
Ananth K. Kidambi
,
Gurpreet Singh
,
Paulius Dilkas
,
Kuldeep S. Meel
·
YOU?
·
· 2025
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2502.12278
YOU?
·
· 2025
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.2502.12278
First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to variants of FOMC, the design of scalable methods for FOMC has attracted attention from both theoreticians and practitioners over the past decade. Recently, a new approach based on first-order knowledge compilation was proposed. This approach, called Crane, instead of simply providing the final count, generates definitions of (possibly recursive) functions that can be evaluated with different arguments to compute the model count for any domain size. However, this approach is not fully automated, as it requires manual evaluation of the constructed functions. The primary contribution of this work is a fully automated compilation algorithm, called Crane2, which transforms the function definitions into C++ code equipped with arbitrary-precision arithmetic. These additions allow the new FOMC algorithm to scale to domain sizes over 500,000 times larger than the current state of the art, as demonstrated through experimental results.
Related Topics
Concepts
Metadata
- Type
- preprint
- Language
- en
- Landing Page
- http://arxiv.org/abs/2502.12278
- https://arxiv.org/pdf/2502.12278
- OA Status
- green
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W4407759218
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W4407759218Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.48550/arxiv.2502.12278Digital Object Identifier
- Title
-
Towards Practical First-Order Model CountingWork title
- Type
-
preprintOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2025Year of publication
- Publication date
-
2025-02-17Full publication date if available
- Authors
-
Ananth K. Kidambi, Gurpreet Singh, Paulius Dilkas, Kuldeep S. MeelList of authors in order
- Landing page
-
https://arxiv.org/abs/2502.12278Publisher landing page
- PDF URL
-
https://arxiv.org/pdf/2502.12278Direct link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
greenOpen access status per OpenAlex
- OA URL
-
https://arxiv.org/pdf/2502.12278Direct OA link when available
- Concepts
-
Order (exchange), Computer science, Economics, FinanceTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
0Total citation count in OpenAlex
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W4407759218 |
|---|---|
| doi | https://doi.org/10.48550/arxiv.2502.12278 |
| ids.doi | https://doi.org/10.48550/arxiv.2502.12278 |
| ids.openalex | https://openalex.org/W4407759218 |
| fwci | |
| type | preprint |
| title | Towards Practical First-Order Model Counting |
| biblio.issue | |
| biblio.volume | |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T12205 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9491000175476074 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1711 |
| topics[0].subfield.display_name | Signal Processing |
| topics[0].display_name | Time Series Analysis and Forecasting |
| topics[1].id | https://openalex.org/T10317 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9452999830245972 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1705 |
| topics[1].subfield.display_name | Computer Networks and Communications |
| topics[1].display_name | Advanced Database Systems and Queries |
| topics[2].id | https://openalex.org/T12761 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9060999751091003 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1702 |
| topics[2].subfield.display_name | Artificial Intelligence |
| topics[2].display_name | Data Stream Mining Techniques |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C182306322 |
| concepts[0].level | 2 |
| concepts[0].score | 0.6193937063217163 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q1779371 |
| concepts[0].display_name | Order (exchange) |
| concepts[1].id | https://openalex.org/C41008148 |
| concepts[1].level | 0 |
| concepts[1].score | 0.42605456709861755 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[1].display_name | Computer science |
| concepts[2].id | https://openalex.org/C162324750 |
| concepts[2].level | 0 |
| concepts[2].score | 0.22358229756355286 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q8134 |
| concepts[2].display_name | Economics |
| concepts[3].id | https://openalex.org/C10138342 |
| concepts[3].level | 1 |
| concepts[3].score | 0.0 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q43015 |
| concepts[3].display_name | Finance |
| keywords[0].id | https://openalex.org/keywords/order |
| keywords[0].score | 0.6193937063217163 |
| keywords[0].display_name | Order (exchange) |
| keywords[1].id | https://openalex.org/keywords/computer-science |
| keywords[1].score | 0.42605456709861755 |
| keywords[1].display_name | Computer science |
| keywords[2].id | https://openalex.org/keywords/economics |
| keywords[2].score | 0.22358229756355286 |
| keywords[2].display_name | Economics |
| language | en |
| locations[0].id | pmh:oai:arXiv.org:2502.12278 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4306400194 |
| locations[0].source.issn | |
| locations[0].source.type | repository |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | |
| locations[0].source.is_core | False |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | arXiv (Cornell University) |
| locations[0].source.host_organization | https://openalex.org/I205783295 |
| locations[0].source.host_organization_name | Cornell University |
| locations[0].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[0].license | |
| locations[0].pdf_url | https://arxiv.org/pdf/2502.12278 |
| locations[0].version | submittedVersion |
| locations[0].raw_type | text |
| locations[0].license_id | |
| locations[0].is_accepted | False |
| locations[0].is_published | False |
| locations[0].raw_source_name | |
| locations[0].landing_page_url | http://arxiv.org/abs/2502.12278 |
| locations[1].id | doi:10.48550/arxiv.2502.12278 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | |
| locations[1].version | |
| locations[1].raw_type | article |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | |
| locations[1].raw_source_name | |
| locations[1].landing_page_url | https://doi.org/10.48550/arxiv.2502.12278 |
| indexed_in | arxiv, datacite |
| authorships[0].author.id | https://openalex.org/A5116335640 |
| authorships[0].author.orcid | |
| authorships[0].author.display_name | Ananth K. Kidambi |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Kidambi, Ananth K. |
| authorships[0].is_corresponding | False |
| authorships[1].author.id | https://openalex.org/A5018302833 |
| authorships[1].author.orcid | https://orcid.org/0000-0003-3696-965X |
| authorships[1].author.display_name | Gurpreet Singh |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Singh, Guramrit |
| authorships[1].is_corresponding | False |
| authorships[2].author.id | https://openalex.org/A5082232901 |
| authorships[2].author.orcid | https://orcid.org/0000-0001-9185-7840 |
| authorships[2].author.display_name | Paulius Dilkas |
| authorships[2].author_position | middle |
| authorships[2].raw_author_name | Dilkas, Paulius |
| authorships[2].is_corresponding | False |
| authorships[3].author.id | https://openalex.org/A5116335641 |
| authorships[3].author.orcid | |
| authorships[3].author.display_name | Kuldeep S. Meel |
| authorships[3].author_position | last |
| authorships[3].raw_author_name | Meel, Kuldeep S. |
| authorships[3].is_corresponding | False |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://arxiv.org/pdf/2502.12278 |
| open_access.oa_status | green |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Towards Practical First-Order Model Counting |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T06:51:31.235846 |
| primary_topic.id | https://openalex.org/T12205 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9491000175476074 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1711 |
| primary_topic.subfield.display_name | Signal Processing |
| primary_topic.display_name | Time Series Analysis and Forecasting |
| related_works | https://openalex.org/W4391375266, https://openalex.org/W2899084033, https://openalex.org/W2748952813, https://openalex.org/W2390279801, https://openalex.org/W4391913857, https://openalex.org/W2358668433, https://openalex.org/W4396701345, https://openalex.org/W2376932109, https://openalex.org/W2001405890, https://openalex.org/W4396696052 |
| cited_by_count | 0 |
| locations_count | 2 |
| best_oa_location.id | pmh:oai:arXiv.org:2502.12278 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4306400194 |
| best_oa_location.source.issn | |
| best_oa_location.source.type | repository |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | |
| best_oa_location.source.is_core | False |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | arXiv (Cornell University) |
| best_oa_location.source.host_organization | https://openalex.org/I205783295 |
| best_oa_location.source.host_organization_name | Cornell University |
| best_oa_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| best_oa_location.license | |
| best_oa_location.pdf_url | https://arxiv.org/pdf/2502.12278 |
| best_oa_location.version | submittedVersion |
| best_oa_location.raw_type | text |
| best_oa_location.license_id | |
| best_oa_location.is_accepted | False |
| best_oa_location.is_published | False |
| best_oa_location.raw_source_name | |
| best_oa_location.landing_page_url | http://arxiv.org/abs/2502.12278 |
| primary_location.id | pmh:oai:arXiv.org:2502.12278 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4306400194 |
| primary_location.source.issn | |
| primary_location.source.type | repository |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | |
| primary_location.source.is_core | False |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | arXiv (Cornell University) |
| primary_location.source.host_organization | https://openalex.org/I205783295 |
| primary_location.source.host_organization_name | Cornell University |
| primary_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| primary_location.license | |
| primary_location.pdf_url | https://arxiv.org/pdf/2502.12278 |
| primary_location.version | submittedVersion |
| primary_location.raw_type | text |
| primary_location.license_id | |
| primary_location.is_accepted | False |
| primary_location.is_published | False |
| primary_location.raw_source_name | |
| primary_location.landing_page_url | http://arxiv.org/abs/2502.12278 |
| publication_date | 2025-02-17 |
| publication_year | 2025 |
| referenced_works_count | 0 |
| abstract_inverted_index.a | 14, 50, 116 |
| abstract_inverted_index.as | 100, 158 |
| abstract_inverted_index.be | 79 |
| abstract_inverted_index.in | 16 |
| abstract_inverted_index.is | 4, 96, 115 |
| abstract_inverted_index.it | 101 |
| abstract_inverted_index.of | 7, 11, 13, 28, 32, 65, 73, 105, 112, 155 |
| abstract_inverted_index.on | 24, 54 |
| abstract_inverted_index.to | 26, 84, 142, 144 |
| abstract_inverted_index.C++ | 129 |
| abstract_inverted_index.The | 109 |
| abstract_inverted_index.and | 43 |
| abstract_inverted_index.any | 90 |
| abstract_inverted_index.can | 78 |
| abstract_inverted_index.for | 35, 89 |
| abstract_inverted_index.has | 37 |
| abstract_inverted_index.new | 51, 139 |
| abstract_inverted_index.not | 97 |
| abstract_inverted_index.the | 5, 9, 30, 46, 68, 86, 106, 125, 138, 152, 156 |
| abstract_inverted_index.was | 58 |
| abstract_inverted_index.FOMC | 36, 140 |
| abstract_inverted_index.This | 60 |
| abstract_inverted_index.art, | 157 |
| abstract_inverted_index.both | 41 |
| abstract_inverted_index.code | 130 |
| abstract_inverted_index.from | 40 |
| abstract_inverted_index.into | 128 |
| abstract_inverted_index.over | 45, 147 |
| abstract_inverted_index.past | 47 |
| abstract_inverted_index.rely | 23 |
| abstract_inverted_index.than | 151 |
| abstract_inverted_index.that | 77 |
| abstract_inverted_index.this | 94, 113 |
| abstract_inverted_index.with | 81, 132 |
| abstract_inverted_index.work | 114 |
| abstract_inverted_index.FOMC, | 29 |
| abstract_inverted_index.Since | 19 |
| abstract_inverted_index.These | 135 |
| abstract_inverted_index.allow | 137 |
| abstract_inverted_index.based | 53 |
| abstract_inverted_index.count | 88 |
| abstract_inverted_index.final | 69 |
| abstract_inverted_index.fully | 98, 117 |
| abstract_inverted_index.model | 1, 87 |
| abstract_inverted_index.scale | 143 |
| abstract_inverted_index.size. | 92 |
| abstract_inverted_index.sizes | 146 |
| abstract_inverted_index.state | 154 |
| abstract_inverted_index.times | 149 |
| abstract_inverted_index.which | 123 |
| abstract_inverted_index.(FOMC) | 3 |
| abstract_inverted_index.Crane, | 63 |
| abstract_inverted_index.called | 62, 121 |
| abstract_inverted_index.count, | 70 |
| abstract_inverted_index.design | 31 |
| abstract_inverted_index.domain | 91, 145 |
| abstract_inverted_index.larger | 150 |
| abstract_inverted_index.lifted | 20 |
| abstract_inverted_index.logic. | 18 |
| abstract_inverted_index.manual | 103 |
| abstract_inverted_index.models | 12 |
| abstract_inverted_index.number | 10 |
| abstract_inverted_index.simply | 66 |
| abstract_inverted_index.500,000 | 148 |
| abstract_inverted_index.Crane2, | 122 |
| abstract_inverted_index.compute | 85 |
| abstract_inverted_index.current | 153 |
| abstract_inverted_index.decade. | 48 |
| abstract_inverted_index.instead | 64 |
| abstract_inverted_index.methods | 34 |
| abstract_inverted_index.primary | 110 |
| abstract_inverted_index.problem | 6 |
| abstract_inverted_index.through | 160 |
| abstract_inverted_index.However, | 93 |
| abstract_inverted_index.approach | 52, 95 |
| abstract_inverted_index.counting | 2, 8 |
| abstract_inverted_index.equipped | 131 |
| abstract_inverted_index.function | 126 |
| abstract_inverted_index.requires | 102 |
| abstract_inverted_index.results. | 162 |
| abstract_inverted_index.scalable | 33 |
| abstract_inverted_index.sentence | 15 |
| abstract_inverted_index.variants | 27 |
| abstract_inverted_index.(possibly | 74 |
| abstract_inverted_index.Recently, | 49 |
| abstract_inverted_index.additions | 136 |
| abstract_inverted_index.algorithm | 141 |
| abstract_inverted_index.approach, | 61 |
| abstract_inverted_index.arguments | 83 |
| abstract_inverted_index.attention | 39 |
| abstract_inverted_index.attracted | 38 |
| abstract_inverted_index.automated | 118 |
| abstract_inverted_index.different | 82 |
| abstract_inverted_index.evaluated | 80 |
| abstract_inverted_index.functions | 76 |
| abstract_inverted_index.generates | 71 |
| abstract_inverted_index.inference | 21 |
| abstract_inverted_index.knowledge | 56 |
| abstract_inverted_index.proposed. | 59 |
| abstract_inverted_index.providing | 67 |
| abstract_inverted_index.algorithm, | 120 |
| abstract_inverted_index.automated, | 99 |
| abstract_inverted_index.evaluation | 104 |
| abstract_inverted_index.functions. | 108 |
| abstract_inverted_index.recursive) | 75 |
| abstract_inverted_index.reductions | 25 |
| abstract_inverted_index.techniques | 22 |
| abstract_inverted_index.transforms | 124 |
| abstract_inverted_index.First-order | 0 |
| abstract_inverted_index.arithmetic. | 134 |
| abstract_inverted_index.compilation | 57, 119 |
| abstract_inverted_index.constructed | 107 |
| abstract_inverted_index.definitions | 72, 127 |
| abstract_inverted_index.first-order | 17, 55 |
| abstract_inverted_index.contribution | 111 |
| abstract_inverted_index.demonstrated | 159 |
| abstract_inverted_index.experimental | 161 |
| abstract_inverted_index.practitioners | 44 |
| abstract_inverted_index.theoreticians | 42 |
| abstract_inverted_index.arbitrary-precision | 133 |
| cited_by_percentile_year | |
| countries_distinct_count | 0 |
| institutions_distinct_count | 4 |
| citation_normalized_percentile |