Alexander
Nadel's Page
General
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:
- Propositional Satisfiability (SAT)
- Satisfiability Modulo Theories (SMT)
- Model Checking
- Formal Methods for Physical Design
- Formal Verification of Hardware and Software
Contact Information
My email is alexander DOT nadel AT intel DOT com
Publications
2018
[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
2017
[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.
2016
[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.
2015
[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.
2014
[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.
2013
[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.
2012
[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.
2011
[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.
2010
[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 satcompetition.org 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).
2009
[28]Alexander Nadel, August 2009, �Understanding and Improving a Modern SAT Solver�. PhD thesis, Tel Aviv University.
2007
[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.
2006
[31]Nachum Dershowitz, Ziyad Hanna, Alexander Nadel, August 2006, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" [presentation]. SAT 2006: 36-41
2005
[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
2002
[34]Alexander Nadel, November 2002, "Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew University.