论文标题
可扩展的证据通过共享而不是复制条款，从而与gimsatul产生多线程SAT解决
Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
论文作者
论文摘要
我们首先说明了我们新的平行SAT求解器gimsatul。它的关键功能是在内存中进行物理共享子句，而不是复制它们，这是其他最先进的多线程SAT求解器的方法来逻辑地交换条款。我们的方法保留了有关求解线程的本地条款中观察哪些文字的信息，但在所有求解线程中在全球范围内分享了一项的实际不变文字。该设计提供了相当出色的并行可伸缩性，可以使积极的子句共享，同时保持记忆使用量较低并产生更紧凑的证明。
We give a first account of our new parallel SAT solver Gimsatul. Its key feature is to share clauses physically in memory instead of copying them, which is the method of other state-of-the-art multi-threaded SAT solvers to exchange clauses logically. Our approach keeps information about which literals are watched in a clause local to a solving thread but shares the actual immutable literals of a clause globally among all solving threads. This design gives quite remarkable parallel scalability, allows aggressive clause sharing while keeping memory usage low and produces more compact proofs.
