一句话：提出基于 backbone 的 all-SAT 求解器 BASolver，通过缩短阻塞子句加速全可满足赋值枚举。
All-SAT 问题要求找出命题公式的所有可满足赋值，广泛应用于模型检测、自动机构造和逻辑最小化。现有求解器通常迭代求解并添加阻塞子句，但子句较长会拖慢后续搜索。本文提出 BASolver：先识别 backbone 变量，并从部分赋值和阻塞子句中移除这些变量，从而生成更短的阻塞子句。作者将 BASolver 与 MBlocking、BC、BDD 和 NBC 四种已有 all-SAT 求解器进行比较。实验结果显示，尽管寻找全部 backbone 变量会带来额外计算时间，但由于阻塞子句更短且能利用 backbone 变量，BASolver 整体上仍比现有求解器更高效。
The All-SAT (All-SATisfiable) problem focuses on finding all satisfiable assignments of a given propositional formula, whose applications include model checking, automata construction, and logic minimization. A typical ALL-SAT solver is normally based on iteratively computing satisfiable assignments of the given formula. In this work, we introduce BASolver, a backbone-based All-SAT solver for propositional formulas. Compared to the existing approaches, BASolver generates shorter blocking clauses by removing backbone variables from the partial assignments and the blocking clauses. We compare BASolver with 4 existing ALL-SAT solvers, namely MBlocking, BC, BDD, and NBC. Experimental results indicate that although finding all the backbone variables consumes additional computing time, BASolver is still more efficient than the existing solvers because of the shorter blocking clauses and the backbone variables used in it.
DOI 原文 ·
@inproceedings{paperbot5975,
title = {Accelerating all-SAT computation with short blocking clauses},
author = {Yueling Zhang and Geguang Pu and Jun Sun},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3416569}
}