Modal CEGAR-tableaux with RECAR and resolution-based SAT-shortcuts

[Submitted on 30 Jun 2026]

Authors:Rajeev Goré (Faculty of Information Technology, Monash University, Australia), Cormac Kikkert (Cormac Kikkert Research)

View PDF

Abstract:We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that:
(1) CEGARBox++ with RECAR SAT-shortcuts is not competitive
(2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP,
particularly on large satisfiable problems.
As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.

Submission history

From: EPTCS [view email] [via EPTCS proxy]
[v1] Tue, 30 Jun 2026 15:58:08 UTC (1,021 KB)