Experimental data of TACAS 2026 Publication "Real-time Proof Checking for Distributed Incremental SAT Solving"

This repository features the software and experimental data surrounding our TACAS 2026 publication "Real-time Proof Checking for Distributed Incremental SAT Solving".Abstract: Distributed clause-sharing SAT solvers are powerful automated reasoning tools capable of rapidly solving many difficult instances. Users of SAT solving often rely on incremental SAT solving, i.e., interactive solve calls over an evolving formula. We present the first approach to distributed incremental SAT solving that grants full confidence in the obtained result. Specifically, we extend a recent distributed real-time proof checking approach with an incremental proof interface. Our approach offers great flexibility in that it supports dynamic re-scheduling of computational resources and allows to safely share clauses across tasks that operate on deviating assumptions and formula increments. We further add on-the-fly clause compression to checkers in order to reduce memory consumption. Experiments with the distributed solver MallobSat on up to 1216 cores show that our trusted solving approach checks incremental SAT tasks with small mean overhead (<33%) over unchecked solving.Note: This initial version of the artifact does not yet feature specific instructions to reproduce the experiments and plots from the paper. We aim to integrate them in a future version of the artifact as soon as possible.