| 2026 | AAAI | From Decision Trees to Boolean Logic: A Fast and Unified SHAP Algorithm. | Alexander Nadel, Ron Wettenstein |
| 2026 | SAT | Backtrackable Inprocessing. | Alexander Nadel |
| 2025 | SAT | Enumerating All Boolean Matches. | Alexander Nadel, Yogev Shalmon |
| 2024 | SAT | Entailing Generalization Boosts Enumeration. | Dror Fried, Alexander Nadel, Roberto Sebastiani, Yogev Shalmon |
| 2023 | SAT | AllSAT for Combinational Circuits. | Dror Fried, Alexander Nadel, Yogev Shalmon |
| 2023 | SAT | Solving Huge Instances with Intel(R) SAT Solver. | Alexander Nadel |
| 2022 | SAT | Introducing Intel(R) SAT Solver. | Alexander Nadel |
| 2021 | TACAS | Local Search with a SAT Oracle for Combinatorial Optimization. | Aviad Cohen, Alexander Nadel, Vadim Ryvchin |
| 2020 | FMCAD | Anytime Algorithms for MaxSAT and Beyond. | Alexander Nadel |
| 2020 | FMCAD | On Optimizing a Generic Function in SAT. | Alexander Nadel |
| 2019 | FMCAD | Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization. | Alexander Nadel |
| 2018 | SAT | Solving MaxSAT with Bit-Vector Optimization. | Alexander Nadel |
| 2018 | SAT | Chronological Backtracking. | Alexander Nadel, Vadim Ryvchin |
| 2017 | CAV | A Correct-by-Decision Solution for Simultaneous Place and Route. | Alexander Nadel |
| 2017 | FMCAD | Solving linear arithmetic with SAT-based model checking. | Yakir Vizel, Alexander Nadel, Sharad Malik |
| 2016 | FMCAD | Routing under constraints. | Alexander Nadel |
| 2016 | TACAS | Bit-Vector Optimization. | Alexander Nadel, Vadim Ryvchin |
| 2015 | CAV | Finding Bounded Path in Graph Using SMT for Automatic Clock Routing. | Amit Erez, Alexander Nadel |
| 2014 | CAV | Bit-Vector Rewriting with Automatic Rule Generation. | Alexander Nadel |
| 2014 | SAT | Ultimately Incremental SAT. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2013 | CAV | Efficient Generation of Small Interpolants in CNF. | Yakir Vizel, Vadim Ryvchin, Alexander Nadel |
| 2013 | FMCAD | Efficient MUS extraction with resolution. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2012 | SAT | Efficient SAT Solving under Assumptions. | Alexander Nadel, Vadim Ryvchin |
| 2012 | SAT | Preprocessing in Incremental SAT. | Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
| 2011 | SAT | Generating Diverse Solutions in SAT. | Alexander Nadel |
| 2010 | FMCAD | SAT-based semiformal verification of hardware. | Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel |
| 2010 | FMCAD | Applying SMT in symbolic execution of microcode. | Anders Franzn, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani, Jonathan Shalev |
| 2010 | FMCAD | Boosting minimal unsatisfiable core extraction. | Alexander Nadel |
| 2010 | SAT | Assignment Stack Shrinking. | Alexander Nadel, Vadim Ryvchin |
| 2007 | CAV | A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems. | Roberto Bruttomesso, Alessandro Cimatti, Anders Franzn, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani |
| 2007 | SAT | Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
| 2006 | SAT | A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
| 2005 | SAT | A Clause-Based Heuristic for SAT Solvers. | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |