Demo Data from EDBT 2026 / reviewers in the wild / expert
Vadim Ryvchin
dblp:72/2793
· DBLP profile ↗
14ranked-venue papers
2as first author
1since 2021 · last 2021
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 12 · 2 first-authorArtificial intelligence and machine learning · 9 · 2 first-authorSoftware engineering, systems software and programming languages · 4 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Theoretical computer science
1 paper |
Automated reasoning and model checking · 100% |
Topics — the 1 heaviest of 1, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Automated reasoning and model checking › automated reasoning
interpolation |
0.2 | 1 | 2013 | Efficient Generation of Small Interpolants in CNF · CAV 2013 |
Methods — techniques the papers use, named apart from their topics
interpolant generation · 0.2CNF representation · 0.2
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2021 | Local Search with a SAT Oracle for Combinatorial OptimizationabstractAbstract NP-hard combinatorial optimization problems are pivotal in science and business. There exists a variety of approaches for solving such problems, but for problems with complex constraints and objective functions, local search algorithms scale the best. Such algorithms usually assume that finding a non-optimal solution with no other requirements is easy. However, what if it is NP-hard? In such case, a SAT solver can be used for finding the initial solution, but how can one continue solving the optimization problem? We offer a generic methodology, called Local Search with SAT Oracle (), to solve such problems. facilitates implementation of advanced local search methods, such as variable neighbourhood search, hill climbing and iterated local search, while using a SAT solver as an oracle. We have successfully applied our approach to solve a critical industrial problem of cell placement and productized our solution at Intel. Aviad Cohen 0001, Alexander Nadel, Vadim Ryvchin |
TACAS (2) | 3 |
| 2018 | Chronological Backtracking
Alexander Nadel, Vadim Ryvchin |
SAT | 2 |
| 2016 | Bit-Vector Optimization
Alexander Nadel, Vadim Ryvchin |
TACAS | 2 |
| 2015 | Mining Backbone Literals in Incremental SAT - A New Kind of Incremental Data
Alexander Ivrii, Vadim Ryvchin, Ofer Strichman |
SAT | 2 |
| 2015 | Hints Revealed
Jonathan Kalechstain, Vadim Ryvchin, Nachum Dershowitz |
SAT | 2 |
| 2015 | Efficient generation of small interpolants in CNF
Yakir Vizel, Alexander Nadel, Vadim Ryvchin |
Formal Methods Syst. Des. | 3 |
| 2014 | Ultimately Incremental SAT
Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
SAT | 2 |
| 2013 | Efficient Generation of Small Interpolants in CNF
Yakir Vizel, Vadim Ryvchin, Alexander Nadel |
CAV | 2 |
| 2013 | Efficient MUS extraction with resolution
Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
FMCAD | 2 |
| 2012 | Efficient SAT Solving under Assumptions
Alexander Nadel, Vadim Ryvchin |
SAT | 2 |
| 2012 | Preprocessing in Incremental SAT
Alexander Nadel, Vadim Ryvchin, Ofer Strichman |
SAT | 2 |
| 2011 | Faster Extraction of High-Level Minimal Unsatisfiable Cores
Vadim Ryvchin, Ofer Strichman |
SAT | 1 |
| 2010 | Assignment Stack Shrinking
Alexander Nadel, Vadim Ryvchin |
SAT | 2 |
| 2008 | Local Restarts
Vadim Ryvchin, Ofer Strichman |
SAT | 1 |