Alexander Nadel's Page

General

I am a researcher and engineer developing high-performance constraint solving tools.

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

Contact Information

My email is alexander DOT nadel AT intel DOT com

Publications

2016

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

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

2015

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

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

[5]     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

[6]     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.

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

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

2013

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

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

[11] 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

[12]  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.

[13]  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

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

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

o   An addendum to the paper is available.

2010

[16]  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.

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

[18]  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.

[19]  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.

[20]  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).

[21]  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

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

2007

[23]  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.

[24]  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

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

2005

[26]  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

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

2002

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

Talks

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.

 

Professional Services

2017 PC member at CAV conference
2016 PC member at SMT workshop
2012-2016 PC member at SAT conference
2011 Judge at the SAT’11 Competition.
2010 PC member at SAT 2010

 

Publicly Available Software

2001-2004 Jerusat SAT solver (ver. 1.3) ‎[28]: Jerusat won multiple medals at the international SAT competitions, including winning the Industrial, Satisfiable category at the SAT’04 competition.