Scalable Proof Producing Multi-Threaded SAT Solving with Gimsatul through Sharing instead of Copying Clauses

2022/07/27 by Mathias Fleury, Armin Biere, Fleury, Mathias +1 · 2 citations
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques

paper · pdf · doi:10.48550/arxiv.2207.13577

openalex publication_date 2022/07/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Parallelizable Exact Synthesis of Quantum Circuits via Semi-Tensor Product
• RustSAT: A Library For SAT Solving in Rust

Related

• Learned Clause Minimization in Parallel SAT Solvers
• GpuShareSat: a SAT solver using the GPU for clause sharing
• Proof-Stitch: Proof Combination for Divide and Conquer SAT Solvers
• Clause Vivification by Unit Propagation in CDCL SAT Solvers
• HordeSat: A Massively Parallel Portfolio SAT Solver