I am a research scientist and engineer. My expertise lays in developing state-of-the-art constraint solvers and applying them in the industry.
I have been at Intel, Haifa since 2003. My professional interests include:
My email: alexander DOT nadel AT cs DOT tau DOT ac DOT il
My ORCID ID: https://orcid.org/0000-0003-4679-892X
 Aviad Cohen, Alexander Nadel and Vadim Ryvchin, “Local Search with a SAT Oracle for Combinatorial Optimization” [presentation: pptx (with narration), pdf]. TACAS’21.
o The major algorithmic improvement as compared to the 2019 version of the solver is the Polosat algorithm, detailed in .
A detailed description of the 2019 version of
o The solver was created by implementing some of the ideas from  in Open-WBO-Inc.
A more thorough description is available in .
 Saurabh Joshi, Prateek Kumar, Vasco Manquinho, Ruben Martins, Alexander Nadel and Sukrut Rao, “Open-WBO-Inc in MaxSAT Evaluation 2018”
o The solver won the “Weighted Incomplete 60s” track of MaxSAT Evaluation 2018
Alexander Nadel and Sharad Malik, “Solving
Linear Arithmetic with SAT-based Model Checking” [presentation].
Alexander Nadel, “A
Correct-by-Decision Solution for Simultaneous Place and Route” [presentation].
Vizel, Alexander Nadel and Sharad Malik, “Solving
Constraints over Bit-Vectors with SAT-based Model Checking” [presentation].
Erez and Alexander Nadel, “Finding
Bounded Path in Graph using SMT for Automatic Clock Routing” [presentation].
Dershowitz and Alexander Nadel, “Is
Bit-Vector Reasoning as Hard as NExpTime in Practice?” [presentation].
 Yakir Vizel, Vadim Ryvchin and Alexander Nadel, “Efficient Generation of Small Interpolants in CNF”. Formal Methods in System Design (2015), pages 1-24.
Alexander Nadel, Vadim Ryvchin, and Ofer
Deletion-based Extraction of Minimal Unsatisfiable Cores”. Journal on
Satisfiability, Boolean Modeling and Computation (JSAT) 9 (2014), pages 27-51.
Rewriting with Automatic Rule Generation” [presentation].
 Alexander Nadel, “Handling
Bit-Propagating Operations in Bit-Vector Reasoning” [presentation].
 Yakir Vizel, Vadim Ryvchin and Alexander Nadel, “Efficient Generation of Small Interpolants in CNF” [CAV’13 presentation; Interpolation’13 presentation with additional details]. CAV’13.
We found two typos in the paper: the subscript
for the conjunction should be “j=1” instead of “j=i” at p.9, last paragraph and
p. 10, Alg.2, line 3.
o A technical report containing a proof supplement is available.
Khasidashvili, and Alexander Nadel, “Implicative
Simultaneous Satisfiability and Applications” [presentation].
o An addendum to the paper is available.
o An addendum to the paper containing complementary experimental results is available.
for high-level minimal unsatisfiable core extraction, which were generated
by Intel’s abstraction refinement flow and used in my paper, are available at
the above link. Thanks to satcompetition.org
site organizers for hosting them.
 Anders Franzén,
Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani and Jonathan Shalev, “Applying SMT in Symbolic Execution of Microcode”. FMCAD’10. Received the FMCAD’10 best paper award.
o Detailed experimental results are available.
2 with shrinking and advanced restart strategies is available. Vadim
Ryvchin implemented shrinking and the restart strategies on top of Minisat 2. UPDATE (December,
2010): Now the code matches exactly the Minisat version we had used for the
paper. Unfortunately, an incorrect version appeared before.
 Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry
Korchemny, Michael Lifshits, Alexander Nadel, “An Experience of Complex Design Validation: How to Make Semiformal
Verification Work” [presentation]. Proceedings of the Design and Verification Conference and Exhibition
 Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, Vadim Ryvchin, “Designers Work Less with Quality Formal Equivalence Checking” [presentation]. Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).
 Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna,
Alexander Nadel, Amit Palti, Roberto Sebastiani, "A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification
Problems". CAV 2007: 547-560.
 Alexander Nadel, November 2002, "Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew University.