TY - GEN

T1 - Reducing chaos in SAT-like search

T2 - 14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011

AU - Abío, Ignasi

AU - Deters, Morgan

AU - Nieuwenhuis, Robert

AU - Stuckey, Peter J.

PY - 2011/6/27

Y1 - 2011/6/27

N2 - 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., re-scheduling), 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.

AB - 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., re-scheduling), 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.

UR - http://www.scopus.com/inward/record.url?scp=79959392250&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-21581-0_22

DO - 10.1007/978-3-642-21581-0_22

M3 - Conference Paper

AN - SCOPUS:79959392250

SN - 9783642215803

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 273

EP - 286

BT - Theory and Application of Satisfiability Testing - 14th International Conference, SAT 2011, Proceedings

PB - Springer

Y2 - 19 June 2011 through 22 June 2011

ER -