Gimsatul 通过共享而非复制子句实现可证明可扩展的多线程 SAT 求解
计算机科学中的逻辑
2022-08-01 v2
摘要
我们首次介绍我们的新型并行 SAT 求解器 Gimsatul。其关键特征是在内存中物理地共享子句而非复制它们，而其他最先进的多线程 SAT 求解器采用的是逻辑交换子句的方法。我们的方法将子句中受监视的文字信息保留在求解线程局部，但在所有求解线程间全局共享子句实际的不可变文字。该设计带来了相当显著的并行可扩展性，允许激进的子句共享同时保持低内存使用，并生成更紧凑的证明。
引用
@article{arxiv.2207.13577,
title = {Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses},
author = {Mathias Fleury and Armin Biere},
journal= {arXiv preprint arXiv:2207.13577},
year = {2022}
}
备注
Accepted at the Pragmatics of SAT workshop http://www.pragmaticsofsat.org/2022/