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 and joined the Technion’s
Faculty of Data and Decision Sciences as a part-time research fellow in
2023.
My
professional interests include:
- Propositional Satisfiability
(SAT)
- Satisfiability Modulo Theories
(SMT)
- MaxSAT and Optimization in SAT
and SMT
- Model Checking
- Formal Methods for Physical
Design
- Formal Verification of Hardware
and Software
Contact and Other Information
My email: alexander DOT
nadel AT intel DOT com
My ORCID
ID: https://orcid.org/0000-0003-4679-892X
Publications
2023
[1]
Dror Fried, Alexander Nadel and Yogev Shalmon,
“AllSAT for Combinational Circuits”, [SAT’23 Presentation]. SAT’23.
[2]
Alexander Nadel, “Solving Huge Instances with Intel® SAT Solver” [SAT’23 Presentation with Narration]. SAT’23.
2022
[3]
Alexander Nadel, “Introducing Intel® SAT Solver” [repository, SAT’22 presentation, long presentation (presented at MIAO Seminar on Feb. 28, 2023), MIAO Seminar
video]. SAT’22.
2021
[4]
Aviad Cohen, Alexander Nadel and Vadim Ryvchin,
“Local
Search with a SAT Oracle for Combinatorial Optimization” [presentation: pptx
(with narration), pdf].
TACAS’21.
[5]
Alexander Nadel, “TT-Open-WBO-Inc-21: an Anytime MaxSAT Solver Entering MSE’21”
o
A description of my solver TT-Open-WBO-Inc-21,
which came in 2nd in both the Weighted, Incomplete categories and
the 60-sec. Unweighted, Incomplete and 3d in the 300-sec. Unweighted, Incomplete
category at MaxSAT Evaluation
2021.
2020
[6]
Alexander Nadel, “On Optimizing a Generic Function in SAT” [presentation]. FMCAD’20.
[7]
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 [6].
o
TT-Open-WBO-Inc-20
was also part of the 2021 version of the solver SATLike-c which won 3 out of 4 Incomplete
categories at MaxSAT
Evaluation 2021.
[8]
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
[9]
Alexander Nadel, “Anytime Weighted MaxSAT with
Improved Polarity Selection and Bit-Vector Optimization” [presentation]. FMCAD’19.
[10]
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 [6][9] in Open-WBO-Inc.
o
A more thorough description is available in [8].
[11]
Alexander Nadel and Vadim Ryvchin, “Flipped
Recording” [presentation].
POS’19.
2018
[12] Alexander
Nadel, “Solving MaxSAT with Bit-Vector Optimization” [presentation]. SAT’18.
o
Supplementary
material is available here.
[13] 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.
[14]
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
[15]
Yakir
Vizel, Alexander Nadel and Sharad Malik, “Solving
Linear Arithmetic with SAT-based Model Checking” [presentation].
FMCAD’17.
[16]
Alexander Nadel, “A
Correct-by-Decision Solution for Simultaneous Place and Route” [presentation].
CAV’17.
[17]
Yakir
Vizel, Alexander Nadel and Sharad Malik, “Solving
Constraints over Bit-Vectors with SAT-based Model Checking” [presentation].
SMT’17.
2016
[18]
Alexander Nadel, “Routing
under Constraints” [presentation: pptx,
pdf].
FMCAD’16.
[19]
Alexander Nadel and Vadim Ryvchin, “Bit-Vector
Optimization” [presentation].
TACAS’16.
2015
[20]
Amit
Erez and Alexander Nadel, “Finding
Bounded Path in Graph using SMT for Automatic Clock Routing” [presentation].
CAV’15.
[21]
Nachum
Dershowitz and Alexander Nadel, “Is
Bit-Vector Reasoning as Hard as NExpTime in Practice?” [presentation].
SMT’15.
[22]
Yakir Vizel,
Vadim Ryvchin and Alexander Nadel, “Efficient
Generation of Small Interpolants in CNF”. Formal Methods in System Design
(2015), pages 1-24.
2014
[23]
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.
[24]
Alexander Nadel, “Bit-Vector
Rewriting with Automatic Rule Generation” [presentation].
CAV’14.
[25] Alexander Nadel, Vadim Ryvchin, and Ofer
Strichman, “Ultimately
Incremental SAT” [presentation].
SAT’14.
2013
[26] Alexander Nadel, Vadim Ryvchin, and Ofer
Strichman, “Efficient
MUS Extraction with Resolution” [presentation].
FMCAD’13.
[27] Alexander Nadel, “Handling
Bit-Propagating Operations in Bit-Vector Reasoning” [presentation].
SMT’13.
[28] 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
[29]
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.
[30]
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
[31]
Zurab
Khasidashvili, and Alexander Nadel, “Implicative
Simultaneous Satisfiability and Applications” [presentation].
HVC’11.
[32]
Alexander Nadel, “Generating
Diverse Solutions in SAT” [presentation].
SAT’11
o
An
addendum to the paper is available.
2010
[33] 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.
[34] Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry
Korchemny, Michael Lifshits and Alexander Nadel, “SAT-Based Semiformal Verification of Hardware”. FMCAD’10.
[35] 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.
[36] 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.
[37] 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).
[38] 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
[39] Alexander Nadel, August 2009, “Understanding and Improving a Modern SAT Solver”. PhD thesis, Tel Aviv University.
2007
[40] 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.
[41] 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
[42] Nachum Dershowitz, Ziyad Hanna, Alexander
Nadel, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction" [presentation]. SAT 2006: 36-41
2005
[43] Zurab Khasidashvili, Alexander Nadel, Amit
Palti, Ziyad Hanna, "Simultaneous SAT-Based Model Checking of Safety Properties" [presentation]. Haifa Verification Conference 2005: 56-75
[44] Nachum Dershowitz, Ziyad Hanna, Alexander
Nadel, "A Clause-Based Heuristic for SAT Solvers" [presentation]. SAT 2005: 46-60
2002
[45] Alexander Nadel, November 2002, "Backtrack Search Algorithms for
Propositional Logic Satisfiability : Review and Innovations". Master Thesis, the Hebrew
University.