Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses
Logic in Computer Science
2022-08-01 v2
Abstract
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.
Cite
@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}
}
Comments
Accepted at the Pragmatics of SAT workshop http://www.pragmaticsofsat.org/2022/