Generation and prediction of difficult model counting instances

Loading...
Thumbnail Image
Date
2022-12-06
Authors
Escamocher, Guillaume
O'Sullivan, Barry
Journal Title
Journal ISSN
Volume Title
Publisher
Published Version
Research Projects
Organizational Units
Journal Issue
Abstract
We present a way to create small yet difficult model counting instances. Our generator is highly parameterizable: the number of variables of the instances it produces, as well as their number of clauses and the number of literals in each clause, can all be set to any value. Our instances have been tested on state of the art model counters, against other difficult model counting instances, in the Model Counting Competition. The smallest unsolved instances of the competition, both in terms of number of variables and number of clauses, were ours. We also observe a peak of difficulty when fixing the number of variables and varying the number of clauses, in both random instances and instances built by our generator. Using these results, we predict the parameter values for which the hardest to count instances will occur.
Description
Keywords
Artificial intelligence , AI , Model Counting Competition , Model counting instances
Citation
Escamocher, G. and O'Sullivan, B. (2022) 'Generation and Prediction of Difficult Model Counting Instances', CoRR abs/2212/.02893, https://arxiv.org/abs/2212.02893, doi: 10.48550/arXiv.2212.02893
Link to publisher’s version