Reducing chaos in SAT-like search: finding solutions close to a given one
Visualitza/Obre
reducting.pdf (234,6Kb) (Accés restringit)
Sol·licita una còpia a l'autor
Què és aquest botó?
Aquest botó permet demanar una còpia d'un document restringit a l'autor. Es mostra quan:
- Disposem del correu electrònic de l'autor
- El document té una mida inferior a 20 Mb
- Es tracta d'un document d'accés restringit per decisió de l'autor o d'un document d'accés restringit per política de l'editorial
10.1007/978-3-642-21581-0_22
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/14740
Tipus de documentText en actes de congrés
Data publicació2011
EditorSpringer Verlag
Condicions d'accésAccés restringit per política de l'editorial
Llevat que s'hi indiqui el contrari, els
continguts d'aquesta obra estan subjectes a la llicència de Creative Commons
:
Reconeixement-NoComercial-SenseObraDerivada 3.0 Espanya
Abstract
Motivated by our own industrial users, we attack the following
challenge that is crucial in many practical planning, scheduling
or timetabling applications. Assume that a solver has found a solution
for a given hard problem and, due to unforeseen circumstances (e.g., rescheduling),
or after an analysis by a committee, a few more constraints
have to be added and the solver has to be re-run. Then it is almost always
important that the new solution is “close” to the original one.
The activity-based variable selection heuristics used by SAT solvers
make search chaotic, i.e., extremely sensitive to the initial conditions.
Therefore, re-running with just one additional clause added at the end
of the input usually gives a completely different solution. We show that
naive approaches for finding close solutions do not work at all, and that
solving the Boolean optimization problem is far too inefficient: to find
a reasonably close solution, state-of-the-art tools typically require much
more time than was needed to solve the original problem.
Here we propose the first (to our knowledge) approach that obtains
close solutions quickly. In fact, it typically finds the optimal (i.e., closest)
solution in only 25% of the time the solver took in solving the original
problem. Our approach requires no deep theoretical or conceptual innovations.
Still, it is non-trivial to come up with and will certainly be
valuable for researchers and practitioners facing the same problem.
CitacióAbío, I. [et al.]. Reducing chaos in SAT-like search: finding solutions close to a given one. A: International Conference on Theory and Applications of Satisfiability Testing. "Theory and Applications of Satisfiability Testing - SAT 2011". Ann Arbor: Springer Verlag, 2011, p. 273-286.
ISBN978-3-642-21580-3
Versió de l'editorhttp://www.springerlink.com/content/0nl71mk67227m5u7/
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
reducting.pdf | 234,6Kb | Accés restringit |