Skip to content
Log in
Sponsored Design Multi-Agent AI Systems Using MCP and A2A: Engineer your own Pyt Design Multi-Agent AI Systems Using MCP and A2A: Engineer your own Pyt

CaDiCaL 3.0

Florian Pollitt Mathias Fleury Katalin Fazekas Nils Froleyks André Schidler Dominik Schreiber Armin Biere
· 0 citations · 57 references

TL;DR

This system description reports on how Kissat’s award-winning techniques were adapted to the full-featured incremental SAT solver CaDiCaL, including clausal congruence closure, clausal equivalence sweeping, and bounded variable addition, to support efficient linear proof production with hints.

Semantic Scholar
View source

Similar papers

2026

Factoring Learned Clauses

This paper revisits previous work on ER, which factors out repeated parts of learned clauses during conflict analysis, and explores how their original strategy benefits from 15 years of improvements in the state-of-the-art solver CaDiCaL, and proposes a new, less intrusive inprocessing approach based on factoring XOR and ITE gates from learned clauses globally.

Florian Pollitt, Zachary Battleman, Mathias Fleury et al. · 1 citation
Preprint Jul 2026

A Modern View on MCSat

This paper revisits the theory-independent MCSat framework as a proof system to provide a modern perspective that refines the original formulation of MCSat, and presents a general, theory-agnostic rule scheme for MCSat and instantiate it for several theories, including propositional logic, non-linear real arithmetic, and uninterpreted functions.

T. Hader, Theo Jauschneg, Daniela Kaufmann et al. · 0 citations
2026

Conditional Autarkies: Hard Formulas Made Easy

It is shown that adding conditional autarkies (as set-blocked clauses) on top of resolution allows efficient refutations of a number of natural combinatorial principles that may occur in SAT benchmarks.

Ilario Bonacina, Maria Luisa Bonet, A. Kolokolova et al. · 0 citations

WhyUnsat: A Practical Explanation Tool

Here it is explained how and why the WhyUnsat approach is now also directly applicable, at no implementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).

R. Nieuwenhuis, Albert Oliveras, Enric Rodríguez-carbonell · 0 citations
Review Open access Jul 2026

Lazy clause generation in retrospect

This review considers how LCG has been refined and expanded over the years since its invention, and how it is used in all most performant CP solvers.

O. Ohrimenko, Peter James Stuckey, M. Codish · 0 citations
2026

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

PalRUP is introduced – an LRUP -based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components.

Ruben Götz, Michael Dörr, Dominik Schreiber · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.