Alexander Nadel's Page

General

I completed my Ph.D. in Computer Science at the Tel-Aviv University under the supervision of Prof. Nachum Dershowitz at 2009.

I am currently at Intel, Haifa. My research interests include:

Contact Information

My email is alexander DOT nadel AT intel DOT com

Publications

2011

[1]     Alexander Nadel, June 2011, “Generating Diverse Solutions in SAT”. SAT’11. The original publication will be available at www.springerlink.com.

o   An addendum to the paper is available.

o   Benchmarks used in the paper are available by e-mail.

2010

[2]     Alexander Nadel, October 2010, “Boosting Minimal Unsatisfiable Core Extraction”. 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.

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

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

[5]     Alexander Nadel, Vadim Ryvchin, July 2010, “Assignment Stack Shrinking”. 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.

[6]     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”. Proceedings of the Design and Verification Conference and Exhibition (DVCon '10).

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

2009

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

2007

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

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

2006

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

2005

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

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

2002

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

Main Research Directions

·         Efficient DPLL-based SAT Solving

-          Assignment stack shrinking ‎[5]

-          A clause-based decision heuristic [‎13,8]

-          Local conflict clause recording [‎10‎,8]

-          Simultaneous solving of a number of properties in a single invocation of a SAT solver [‎12]

·         Unsatisfiable Core Extraction

-          Efficient high-level and clause-level minimal unsatisfiable core extraction [11,8,‎2]

o   High-level minimal unsatisfiable core extraction is unsatisfiable core extraction in terms of “interesting” propositional constraints provided by the user application.

·         Generating Diverse Solutions in SAT

-          Efficient diverse solution generation for hard industrial instances [‎3,1]

·         Applying SMT to Embedded Software Validation [9,4]

·         Applying SAT to Industrial Problems [‎12,7,6,3]

·         Understanding SAT Solving

-          Understanding the SAT solver as a resolution-based engine generating parent resolutions; comparing the performance of various techniques and designing new ones in the light of this observation [‎8]

Software

Eureka SAT solver:

·         Eureka is Intel’s SAT solver. A short description of Eureka’s 2006 version is available. Eureka’s algorithms are described in [‎13,‎12,‎11,‎10,‎8,‎5,‎3,‎2,1].

·         Eureka solved the most instances in Industrial, Unsatisfiable category at the international SAT'05 competition. Eureka finished second at SAT'06 race solving the most unsatisfiable instances and the most instances from the formal verification domain of all participating solvers.

·         The previous version of Eureka’s minimal unsatisfiable core extraction algorithm [‎11,8] was found to be the most efficient for reducing the size of the core by the Mathsat team, who evaluated Eureka’s algorithm vs. Amuse, Genetic, MiniUnsat, Trimmer, ZChaff, and PicoSAT in the context of UNSAT core extraction for SMT. A paper containing the details of the comparison is under submission. A preliminary technical report is available from Alberto Griggio’s site.

Jerusat SAT solver:

·         Jerusat was developed during my Master studies at the Hebrew University [‎14].

·         Jerusat won the Industrial, Satisfiable category at SAT’04 competition.

·         The code of Jerusat1.3 is available.

Other: I am involved in the development of Intel’s SAT-based model checker and SMT solver.