Simultaneous SAT-Based Model Checking of Safety Properties. - Zurab Khasidashvili; Alexander Nadel; Amit Palti; Ziyad Hanna (Haifa Verification Conference, 2005)

A Clause-Based Heuristic for SAT Solvers. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2005)

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2006)

A Lazy and Layered SMT($ mathcal{BV}$) Solver for Hard Industrial Verification Problems. - Roberto Bruttomesso; Alessandro Cimatti; Anders Franzén; Alberto Griggio; Ziyad Hanna; Alexander Nadel; Amit Palti; Roberto Sebastiani (CAV, 2007)

Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver. - Nachum Dershowitz; Ziyad Hanna; Alexander Nadel (SAT, 2007)

Understanding and improving a modern SAT solver - Alexander Nadel (2009)

SAT-based semiformal verification of hardware. - Sabih Agbaria; Dan Carmi; Orly Cohen; Dmitry Korchemny; Michael Lifshits; Alexander Nadel (FMCAD, 2010)

Applying SMT in symbolic execution of microcode. - Anders Franzén; Alessandro Cimatti; Alexander Nadel; Roberto Sebastiani; Jonathan Shalev (FMCAD, 2010)

Boosting minimal unsatisfiable core extraction. - Alexander Nadel (FMCAD, 2010)

Assignment Stack Shrinking. - Alexander Nadel; Vadim Ryvchin (SAT, 2010)

Implicative Simultaneous Satisfiability and Applications. - Zurab Khasidashvili; Alexander Nadel (Haifa Verification Conference, 2011)

Generating Diverse Solutions in SAT. - Alexander Nadel (SAT, 2011)

From Total Assignment Enumeration to Modern SAT Solver - Nachum Dershowitz; Alexander Nadel (CoRR, 2011)

Efficient SAT Solving under Assumptions. - Alexander Nadel; Vadim Ryvchin (SAT, 2012)

Preprocessing in Incremental SAT. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (SAT, 2012)

Efficient MUS extraction with resolution. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (FMCAD, 2013)

Bit-Vector Rewriting with Automatic Rule Generation. - Alexander Nadel (CAV, 2014)

Ultimately Incremental SAT. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (SAT, 2014)

Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores. - Alexander Nadel; Vadim Ryvchin; Ofer Strichman (J. Satisf. Boolean Model. Comput., 2014)

Finding Bounded Path in Graph Using SMT for Automatic Clock Routing. - Amit Erez; Alexander Nadel (CAV (2), 2015)

Efficient generation of small interpolants in CNF. - Yakir Vizel; Alexander Nadel; Vadim Ryvchin (Formal Methods Syst. Des., 2015)

Routing under constraints. - Alexander Nadel (FMCAD, 2016)

Bit-Vector Optimization. - Alexander Nadel; Vadim Ryvchin (TACAS, 2016)

A Correct-by-Decision Solution for Simultaneous Place and Route. - Alexander Nadel (CAV (2), 2017)

Solving linear arithmetic with SAT-based model checking. - Yakir Vizel; Alexander Nadel; Sharad Malik (FMCAD, 2017)

Solving Constraints over Bit-Vectors with SAT-based Model Checking. - Yakir Vizel; Alexander Nadel; Sharad Malik (SMT, 2017)

Solving MaxSAT with Bit-Vector Optimization. - Alexander Nadel (SAT, 2018)

Chronological Backtracking. - Alexander Nadel; Vadim Ryvchin (SAT, 2018)

Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization. - Alexander Nadel (FMCAD, 2019)

Anytime Algorithms for MaxSAT and Beyond. - Alexander Nadel (FMCAD, 2020)

On Optimizing a Generic Function in SAT. - Alexander Nadel (FMCAD, 2020)

Polarity and Variable Selection Heuristics for SAT-Based Anytime MaxSAT. - Alexander Nadel (J. Satisf. Boolean Model. Comput., 2020)

Local Search with a SAT Oracle for Combinatorial Optimization. - Aviad Cohen 001; Alexander Nadel; Vadim Ryvchin (TACAS (2), 2021)

Introducing Intel(R) SAT Solver. - Alexander Nadel (SAT, 2022)

AllSAT for Combinational Circuits. - Dror Fried; Alexander Nadel; Yogev Shalmon (SAT, 2023)

Solving Huge Instances with Intel(R) SAT Solver. - Alexander Nadel (SAT, 2023)

Entailing Generalization Boosts Enumeration. - Dror Fried; Alexander Nadel; Roberto Sebastiani; Yogev Shalmon (SAT, 2024)

TT-Open-WBO-Inc: An Efficient Anytime MaxSAT Solver. - Alexander Nadel (J. Satisf. Boolean Model. Comput., 2024)

Enumerating All Boolean Matches. - Alexander Nadel; Yogev Shalmon (SAT, 2025)