一句话：设计稀疏哈希函数，以更小概率选变量生成短 XOR 约束，提升近似 #SAT 模型计数的可扩展性。
本文关注 CNF 公式的近似模型计数（#SAT）问题。近年来，主流方法将 Stockmeyer 的强 2-universal 哈希函数与 SAT 求解结合：向公式中加入随机 XOR 约束，并反复调用 NP oracle（实践中为 CDCL SAT 求解器）来估计满足赋值数。然而，标准 2-universal 哈希以 1/2 概率选取每个变量，使 XOR 约束期望长度约为 n/2，而过大的 XOR 约束会显著拖慢现代 SAT 求解器在 CNF-XOR 公式上的运行。为此，论文提出设计稀疏哈希函数：以更小概率选取变量，从而生成更短、更稀疏的 XOR 约束，并用以替代强 2-universal 哈希，以提升近似模型计数的可扩展性。摘要未给出具体实验评估结果。
Given a CNF formula F on n variables, the problem of model counting, also referred to as #SAT, is to compute the number of models or satisfying assignments of F. Recent years have witnessed a surge of effort towards developing efficient algorithmic techniques that combine the classical strongly 2-universal hash functions (from [Stockmeyer 1983]) with the remarkable progress in SAT solving over the past decade. These techniques augment the CNF formula F with random XOR constraints and invoke an NP oracle repeatedly on the resultant CNF-XOR formulas. In practice, the NP oracle calls are replaced by calls to a SAT solver and it is observed that runtime performance of modern SAT solvers (based on conflict-driven clause learning) on CNF-XOR formulas is adversely affected by the size of XOR constraints. The standard construction of 2-universal hash functions chooses every variable with probability p = 1/2 leading to XOR constraints of size n/2 in expectation. Consequently, the main challenge is to design sparse hash functions, where variables can be chosen with smaller probability and lead to smaller sized XOR constraints, which can then replace strongly 2-universal hash functions.
DOI 原文 ·
@inproceedings{paperbot5544,
title = {Sparse Hashing for Scalable Approximate Model Counting},
author = {Kuldeep S. Meel and S. Akshay},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394809}
}