Conditional Autarkies and Globally Blocked Clauses

This page provides source code for our invited paper at ATVA'19:

Benjamin Kiesl , Marijn Heule, Armin Biere. Truth Assignments as Conditional Autarkies. To be published in Proc. 17th Intl. Symp. on Automated Technology for Verification and Analysis (ATVA'19), Lecture Notes in Computer Science (LNCS), 17 pages SPringer 2019.
[ preprint | bibtex | source ]

With release rel-1.2.0 of CaDiCaL we published code for eliminating globally blocked clauses on GitHub. It resides in condition.cpp and still needs to be enabled with the --condition flag.

[ cadical-1.2.0-18b56ab.tar.xz ]