Name
Abstract | ||
|---|---|---|
Experimentation of new algorithms is the usual companion section of papers dealing with SAT. However, the behavior of those algorithms is so unpredictable that even strong experiments (hundreds of benchmarks, dozen of solvers) can be still misleading. We present here a set of experiments of very small changes of a canonical Conflict Driven Clause Learning (CDCL) solver and show that even very close versions can lead to very different behaviors. In some cases, the best of them could perfectly have been used to convince the reader of the efficiency of a new method for SAT. This observation can be explained by the lack of real experimental studies of CDCL solvers. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-85958-1_55 | CP |
Keywords | Field | DocType |
conflict-driven clause,cdcl solvers,new algorithm,small change,usual companion section,real experimental study,small changes,different behavior,canonical conflict driven clause,close version,strong experiment,new method,learning algorithms | Conflict-Driven Clause Learning,Mathematical optimization,Computer science,Algorithm,Theoretical computer science,Solver | Conference |
Volume | ISSN | Citations |
5202 | 0302-9743 | 1 |
PageRank | References | Authors |
0.39 | 8 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Audemard | 1 | 640 | 37.66 |
| Laurent Simon | 2 | 746 | 43.15 |