论文标题
困难的模型计数实例的产生和预测
Generation and Prediction of Difficult Model Counting Instances
论文作者
论文摘要
我们提出了一种创建小而困难的模型计数实例的方法。我们的发电机是高度参数化的：它产生的实例的变量数量以及其子句的数量以及每个子句中的文字数量都可以将所有值设置为任何值。在模型计数竞争中，我们的实例已在最先进的模型计数器上对其他困难的模型计数实例进行了测试。竞争的最小未解决的实例，无论是变量数量还是条款数量，都是我们的。在固定变量的数量并改变子句的数量时，在我们的发电机构建的随机实例和实例中，我们还会观察到难度的峰值。使用这些结果，我们预测了最难计数实例的参数值。
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.
