3 papers
cs.LO2026
Backtrackable Inprocessing
Alexander Nadel
We introduce Backtrackable Inprocessing (BI), a framework that enables applying inprocessing under the current trail at any decision level, at any point during incremental SAT solv…
cs.LO2011
From Total Assignment Enumeration to Modern SAT Solver
Nachum Dershowitz, Alexander Nadel
A new framework for presenting and analyzing the functionality of a modern DLL-based SAT solver is proposed. Our approach exploits the inherent relation between backtracking and re…
cs.LO2006
A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
Nachum Dershowitz, Ziyad Hanna, Alexander Nadel
We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. We provide experimental results on formal v…