Alexander Nadel's Page


I am a researcher and engineer developing state-of-the-art constraint solvers and applying them in the industry.

I have been at Intel, Haifa for 15 years. My professional interests include:

Contact Information

My email is alexander DOT nadel AT intel DOT com



[1]   Alexander Nadel, 2018, “Solving MaxSAT with Bit-Vector Optimization” [presentation]. SAT’18.

[2]   Alexander Nadel and Vadim Ryvchin, 2018, “Chronological Backtracking” [presentation]. SAT’18.

o   Maple_LCM_Dist_ChronoBT – our Maple_LCM_Dist-based SAT solver featuring chronological backtracking – won the main and the satisfiable tracks of SAT Competition 2018.

o   We also enabled chronological backtracking in the MaxSAT Evaluation 2017 winner in multiple categories OpenWBO. The updated OpenWBO version is available for download.

[3]   Saurabh Joshi, Prateek Kumar, Vasco Manquinho, Ruben Martins, Alexander Nadel and Sukrut Rao, 2018, “Open-WBO-Inc in MaxSAT Evaluation 2018

o    The solver won the “Weighted Incomplete 60s” track of MaxSAT Evaluation 2018


[4]   Yakir Vizel, Alexander Nadel and Sharad Malik, 2017, “Solving Linear Arithmetic with SAT-based Model Checking” [presentation]. FMCAD’17.

[5]   Alexander Nadel, 2017, “A Correct-by-Decision Solution for Simultaneous Place and Route” [presentation]. CAV’17.

[6]   Yakir Vizel, Alexander Nadel and Sharad Malik, 2017, “Solving Constraints over Bit-Vectors with SAT-based Model Checking” [presentation]. SMT’17.


[7]   Alexander Nadel, 2016, “Routing under Constraints” [presentation: pptx, pdf]. FMCAD’16.

[8]   Alexander Nadel and Vadim Ryvchin, 2016, “Bit-Vector Optimization” [presentation]. TACAS’16.


[9]   Amit Erez and Alexander Nadel, 2015, “Finding Bounded Path in Graph using SMT for Automatic Clock Routing” [presentation]. CAV’15.

[10]Nachum Dershowitz and Alexander Nadel, 2015, “Is Bit-Vector Reasoning as Hard as NExpTime in Practice?” [presentation]. SMT’15.

[11]Yakir Vizel, Vadim Ryvchin and Alexander Nadel, 2015, “Efficient Generation of Small Interpolants in CNF”. Formal Methods in System Design (2015), pages 1-24.


[12]Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2014, “Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores”. Journal on Satisfiability, Boolean Modeling and Computation (JSAT) 9 (2014), pages 27-51.

[13]Alexander Nadel, 2014, “Bit-Vector Rewriting with Automatic Rule Generation” [presentation]. CAV’14.

[14]Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2014, “Ultimately Incremental SAT” [presentation]. SAT’14.


[15]Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2013, “Efficient MUS Extraction with Resolution” [presentation]. FMCAD’13.

[16]Alexander Nadel, 2013, “Handling Bit-Propagating Operations in Bit-Vector Reasoning” [presentation]. SMT’13.

[17]Yakir Vizel, Vadim Ryvchin and Alexander Nadel, 2015, Efficient Generation of Small Interpolants in CNF” [CAV’13 presentation; Interpolation’13 presentation with additional details]. CAV’13.


[18]Alexander Nadel, and Vadim Ryvchin, 2012, “Efficient SAT Solving under Assumptions” [presentation]. SAT’12.

o   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.

[19]Alexander Nadel, Vadim Ryvchin, and Ofer Strichman, 2012, “Preprocessing in Incremental SAT” [presentation]. SAT’12.

o   A technical report containing a proof supplement is available.


[20]Zurab Khasidashvili, and Alexander Nadel, 2011, “Implicative Simultaneous Satisfiability and Applications” [presentation]. HVC’11.

[21]Alexander Nadel, June 2011, “Generating Diverse Solutions in SAT” [presentation]. SAT’11

o   An addendum to the paper is available.


[22]Alexander Nadel, October 2010, “Boosting Minimal Unsatisfiable Core Extraction” [presentation]. FMCAD’10.

o   An addendum to the paper containing complementary experimental results is available.

o   Benchmarks 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 site organizers for hosting them.

[23]Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits and Alexander Nadel, October 2010, “SAT-Based Semiformal Verification of Hardware”. FMCAD’10.

[24]Anders Franzén, Alessandro Cimatti, Alexander Nadel, Roberto Sebastiani and Jonathan Shalev, October 2010, “Applying SMT in Symbolic Execution of Microcode”. FMCAD’10. Received the FMCAD’10 best paper award.

[25]Alexander Nadel, Vadim Ryvchin, July 2010, “Assignment Stack Shrinking” [presentation]. SAT 2010: 375-381.

o   Detailed experimental results are available.

o   Minisat 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.

[26]Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, Alexander Nadel, February 2010, “An Experience of Complex Design Validation: How to Make Semiformal Verification Work” [presentation]. Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).

[27]Orly Cohen, Moran Gordon, Michael Lifshits, Alexander Nadel, Vadim Ryvchin, February 2010, “Designers Work Less with Quality Formal Equivalence Checking” [presentation]. Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).


[28]Alexander Nadel, August 2009, “Understanding and Improving a Modern SAT Solver”. PhD thesis, Tel Aviv University.


[29]Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Ziyad Hanna, Alexander Nadel, Amit Palti, Roberto Sebastiani, August 2007, "A Lazy and Layered SMT(BV) Solver for Hard Industrial Verification Problems". CAV 2007: 547-560.

[30]Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, June 2007, "Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver" [presentation]. SAT 2007: 287-293.


[31]Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, August 2006, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" [presentation]. SAT 2006: 36-41


[32]Zurab Khasidashvili, Alexander Nadel, Amit Palti, Ziyad Hanna, November 2005, "Simultaneous SAT-Based Model Checking of Safety Properties" [presentation]. Haifa Verification Conference 2005: 56-75

[33]Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, June 2005, "A Clause-Based Heuristic for SAT Solvers" [presentation]. SAT 2005: 46-60


[34]Alexander Nadel, November 2002, "Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew University.


2013  Alexander Nadel, Vadim Ryvchin and Yakir Vizel, “Generating Tiny Interpolants and Near-interpolants from a Resolution Refutation”, Interpolation’13 workshop.
2012 SAT Genealogy”, the Technion, Israel.
2011 SAT Technology at Intel”, Invited talk, POS’11 workshop.


Program Committee Membership and Other Professional Services

2019                                    DATE, FMCAD, IJCAI, SAT
2018                                    CAV, FMCAD, IJCAI-ECAI, SAT, SMT
2017                                    CAV, SMT
2016                                    SAT, SMT
2012-2015                         SAT
2011                                    SAT Competition: Judge
2010                                    SAT


Publicly Available Software

2018 Maple_LCM_Dist_ChronoBT‎ [2]: the winner of the main and satisfiable tracks of the SAT Competition 2018, created by implementing chronological backtracking ‎[2] in the SAT Competition 2017 winner Maple_LCM_Dist.
2018 OpenWBO with chronological backtracking ‎[2]: the MaxSAT solver OpenWBO (the version which won multiple categories at MaxSAT Evaluation 2017) enhanced by chronological backtracking ‎[2].
2001-2004 Jerusat SAT solver (ver. 1.3) ‎[33]: Jerusat won multiple medals at the international SAT competitions, including winning the Industrial, Satisfiable category at the SAT’04 competition.