Demo Data from EDBT 2026 / reviewers in the wild / expert
Henri Morel
dblp:71/3479
· DBLP profile ↗
1ranked-venue papers
0as first author
0since 2021 · last 1995
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 1
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 · 30% Algorithms and data structures · 30% Mathematical optimization · 30% |
Topics — the 4 heaviest of 4, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Algorithms and data structures › analysis of algorithms
average-case analysis |
0.0 | 1 | 1995 | A Variational Method for Analysing Unit Clause Search · SIAM J. Comput. 1995 |
Automated reasoning and model checking › satisfiability
SAT solving |
0.0 | 1 | 1995 | A Variational Method for Analysing Unit Clause Search · SIAM J. Comput. 1995 |
Mathematical optimization
variational methods |
0.0 | 1 | 1995 | A Variational Method for Analysing Unit Clause Search · SIAM J. Comput. 1995 |
Computational complexity › complexity classes
exponential time |
0.0 | 1 | 1995 | A Variational Method for Analysing Unit Clause Search · SIAM J. Comput. 1995 |
Methods — techniques the papers use, named apart from their topics
variational method · 0.0probabilistic analysis · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 1995 | A Variational Method for Analysing Unit Clause SearchabstractWe expose a variational method for analysing algorithms, as applied to analyse the algorithm $\textbf{UC}$, which is the Davis-Putnam procedure for a set of clauses of three literals. The variable from a unit clause or, if there is none, the first remaining variable from a fixed list is chosen. The algorithm $\textbf{UC}$ finds all the solutions as a set of cylinders. Following the nomenclature of Purdom [J. Inform. Process., 13 (1990), pp. 449–455], we call this algorithm “unit clause backtracking with cylinders of solutions.” First we give an expression for the number of nodes of the calculation trees of all the inputs. Then we use a variational method to calculate the base $\beta $ of the principal exponential part of the average time of calculation T. This “exponential base” is the maximum of three elementary functions $f_{i}$ of four real variables, These functions are defined on the product of the half positive real line by the 3-dimensional unit real cube. We finally obtain the following short statement. Let v be the number of the variables. Let c be the number of the clauses. Let $\gamma = \frac{c}{v} > 1$. Let $\gamma $ be constant when v grows to infinity. The principal exponential part of the average time of $\textbf{UC}$ is $\beta^{v}$ where \[ \beta = \max\limits_{0 \leq \lambda \leq 1} 2^{\lambda} \left( 1 - \frac{3\lambda ^{2}}{8} + \frac{\lambda ^{3}}{4} \right)^{\gamma}. \] We mean that $\lim_{v \rightarrow \infty} T^{1/v} =\beta $. As a first consequence of our method we match $\textbf{UC}$, with the algorithm $\textbf{B}$ without rearrangement (i.e., with a fixed order for introducing the variables). This gives a proof to a conjecture of P W. Purdom [Artif. Intell., 21(1983), pp. 117–133]. Henri-M. Méjean, Henri Morel, Gerard Reynaud |
SIAM J. Comput. | 2 |