C documents and settings administrateur mes documents travail

Sujets

• motivation
• Employabilité, métiers et formations

Informations

• Publié par: englue
• Nombre de lectures: 296
• Langue: English

Extrait

Constraint Programming Letters 4 (2008) 313

Submitted 6/2008; Published 12/2008

Local Restarts in SAT

Vadim Ryvchin [e-mail] Information Systems Engineering, IE, Technion, Haifa, Israel, and Design Technology Solutions Group, Intel Corporation, Haifa, Israel. Ofer Strichman [e-mail] Information Systems Engineering, IE, Technion, Haifa, Israel.

Editors:Youssef Hamadi, Eric Monfroy and Frederic Saubion

Abstract Most or even all competitive DPLLbased SAT solvers have a “restart” policy, by which the solver is forced to backtrack to decision level 0 according to some criterion. Although not a sophisticated technique, there is mounting evidence that this technique has crucial impact on performance. The common explanation is that restarts help the solver avoid spending too much time in branches in which there is neither an easytofind satisfying assignment nor opportunities for fast learning of strong clauses. All existing techniques rely on a global criterion such as the number of conflicts learned as of the previous restart, and differ in the method of calculating the threshold after which the solver is forced to restart. This approach disregards, in some sense, the original motivation of avoiding ‘bad’ branches. It is possible that a restart is activated right after going into a good branch, or that it spends all of its time in a single bad branch. We suggest instead tolocalizerestarts, i.e., apply restarts according to measures local to each branch. This adds a dimension to the restart policy, namely the decision level in which the solver is currently in. Our experiments with bothMinisat 2007andEurekashow that with certain parameters this improves the run time by 15%  30% on average (when applied to the 100 test benchmarks of SATrace’06), and reduces the number of timeouts. We begin the paper by considering various possible explanations for the effectiveness of restarts. Keywords:SAT solving, Restarts.

1. Introduction:

Why Do Restarts Work ?

Most or even all competitive DPLL SAT solvers have a “restart” policy, a strategy initially proposed by Gomes et al. (1998). Most modern DPLL solvers restart after a certain number of conflict clauses have been learned. The search changes from one restart to the next either due to randomness in the search algorithm, due to the change in the input formula as a result of learning new clauses, or both. The argument given by Gomes et al. (1998) for the success of restarts was in fact only relevant for solvers with a certain level of randomness. They observed empirically that the distribution of running time, when solving the same formula many times with a solver that has a certain element of randomness (assuming each run is initiated with a different seed), is ‘heavytailed’. One may interpret this phenomenon as follows. Every random seed defines a deterministic solver. The heavy tail phenomenon means that at any given time along the time axes, there are still some deterministic solvers that require exponential more time to

c 2008 Vadim Ryvchin and Ofer Strichman.