The propositional satisfiability (SAT) solver Kissat supports a relatively narrow feature set in favor of bare-metal performance and targeted improvements to core solving techniques, which helped it dominate the International SAT Competition since 2024. However, many applications rely on advanced SAT solver features such as incremental interaction schemes, finding direct consequences of assumed literals, or expressive proof logging that allows for real-time checking. This system description reports on how we successfully adapted Kissat’s award-winning techniques to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition. The main challenge was to support efficient linear proof production with hints. We further extended CaDiCaL’s API to extract implied literals under assumptions and applied advanced deterministic scheduling of inprocessing based on the ticks metric for approximating cache line accesses. Experiments confirm the benefits of these efforts.

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 enables safely sharing 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.

Abstract The SAT solver CaDiCaL provides a rich feature set with a clean library interface. It has been adopted by many users, is well documented and easy to extend due to its effective testing and debugging infrastructure. In this tool paper we give a high-level introduction into the solver architecture and then go briefly over implemented techniques. We describe basic features and novel advanced usage scenarios. Experiments confirm that CaDiCaL despite this flexibility has state-of-the-art performance both in a stand-alone as well as incremental setting.

Certifying results by checking proofs and models is an essential feature of modern SAT solving. While incremental solving with assumptions and core extraction is crucial for many applications, support for incremental proof certificates remains lacking. We propose a proof format and corresponding checkers for incremental SAT solving. We further extend it to leverage resolution hints. Experiments on incremental SAT solving for Bounded Model Checking and Satisfiability Modulo Theories demonstrate the feasibility of our approach, further confirming that resolution hints substantially reduce checking time.

Modern SAT solvers are often integrated as sub-reasoning engines into more complex tools to address problems beyond the Boolean satisfiability problem. Consider, for example, solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration, and model counting. There, the SAT solver can often provide relevant information beyond the satisfiability answer and the domain knowledge of the embedding system, such as symmetry properties or theory axioms, may benefit the CDCL search. However, this knowledge can often not be efficiently represented in clausal form. This paper proposes a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. The aim is to capture the essential functionalities that simplify and improve use cases requiring a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, the state-of-the-art SAT solver CaDiCaL is extended with the proposed interface and evaluated on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.

Abstract We introduce a calculus for incremental pre-processing for SMT and instantiate it in the context of z3. It identifies when powerful formula simplifications can be retained when adding new constraints. Use cases that could not be solved in incremental mode can now be solved incrementally thanks to the availability of pre-processing. Our approach admits a class of transformations that preserve satisfiability, but not equivalence. We establish a taxonomy of pre-processing techniques that distinguishes cases where new constraints are modified or constraints previously added have to be replayed. We then justify the soundness of the proposed incremental pre-processing calculus.