Alexander Nadel's Page

General

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:

Contact and Other Information

My email: alexander DOT nadel AT cs DOT tau DOT ac DOT il

My ORCID ID: https://orcid.org/0000-0003-4679-892X

Publications

2021

[1]    Aviad Cohen, Alexander Nadel and Vadim Ryvchin, “Local Search with a SAT Oracle for Combinatorial Optimization” [presentation: pptx (with narration), pdf]. TACAS’21.

2020

[2]    Alexander Nadel, “On Optimizing a Generic Function in SAT” [presentation]. FMCAD’20.

[3]    Alexander Nadel, “TT-Open-WBO-Inc-20: an Anytime MaxSAT Solver Entering MSE’20

o   A description of my solver TT-Open-WBO-Inc-20, which won both of the Weighted, Incomplete categories at MaxSAT Evaluation 2020 and came in 2nd in both the Unweighted, Incomplete categories.

o   The major algorithmic improvement as compared to the 2019 version of the solver is the Polosat algorithm, detailed in ‎[2].

 

[4]    Alexander Nadel, “Polarity and Variable Selection Heuristics for SAT-based Anytime MaxSAT”, JSAT, 12:17-22, 2020.

o   A detailed description of the 2019 version of TT-Open-WBO-Inc.

2019

[5]    Alexander Nadel, “Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector Optimization” [presentation]. FMCAD’19.

[6]    Alexander Nadel, “TT-Open-WBO-Inc: Tuning Polarity and Variable Selection for Anytime SAT-based Optimization

o   A description of my anytime MaxSAT solver TT-Open-WBO-Inc, which won both of the Weighted, Incomplete categories at MaxSAT Evaluation 2019.

o   The solver was created by implementing some of the ideas from ‎[2]‎[5] in Open-WBO-Inc.

o   A more thorough description is available in ‎[4].

[7]    Alexander Nadel and Vadim Ryvchin, “Flipped Recording” [presentation]. POS’19.

2018

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

o   Supplementary material is available here.

[9]    Alexander Nadel and Vadim Ryvchin, “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.

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

2017

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

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

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

2016

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

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

2015

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

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

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

2014

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

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

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

2013

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

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

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

2012

[25]  Alexander Nadel, and Vadim Ryvchin, “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.

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

o   A technical report containing a proof supplement is available.

2011

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

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

o   An addendum to the paper is available.

2010

[29]  Alexander Nadel, “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.

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

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

[32]  Alexander Nadel, Vadim Ryvchin, “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.

[33]  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 (DVCon '10).

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

2009

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

2007

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

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

2006

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

2005

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

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

2002

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

Talks

2020 Alexander Nadel, “Anytime Algorithms for MaxSAT and Beyond”, [video], FMCAD’20 Tutorial.
2019 Alexander Nadel, “Correct-by-Decision Solving and Applications”, Deduction Beyond Satisfiability Dagstuhl Seminar (19371)
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

2021                                    SMT Workshop Co-chair; PC: AAAI, ATVA, IJCAI
2020                                    AAAI, FMCAD, IJCAI, SAT, VLSI-SoC
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

2020 TT-Open-WBO-Inc-20 ‎[2]‎[3]: the 2020 version of TT-Open-WBO-Inc, which won both of the weighted incomplete categories at MaxSAT Evaluation 2020 and came in 2nd in both of the unweighted incomplete categories.
2019 TT-Open-WBO-Inc ‎[5]‎[6]‎[4]: my anytime MaxSAT solver, which won both of the weighted incomplete categories at MaxSAT Evaluation 2019.
2018 Maple_LCM_Dist_ChronoBT [9]: our Maple_LCM_Dist-based SAT solver featuring chronological backtracking, which won the main and the satisfiable tracks of SAT Competition 2018.
2018 OpenWBO with chronological backtracking ‎[9]: the MaxSAT solver OpenWBO (the version which won multiple categories at MaxSAT Evaluation 2017) enhanced by chronological backtracking ‎[9].
2001-2004 Jerusat SAT solver (ver. 1.3) ‎[41]: Jerusat won multiple medals at the international SAT competitions, including winning the Industrial, Satisfiable category at the SAT’04 competition.