Over the years, a steadily improving series of local search solvers for propositional satisfiability (SAT) have been constructed. However, these solvers are often fragile, in that they have apparently minor details in their implementation that dramatically affect performance and confound understanding. In order to understand and predict the success of differing strategies, various local search metrics have been proposed. Many of these metrics summarize properties of the boolean assignments examined during the search. This has two consequences: first, they only capture one side of satisfiability, failing to characterize the behaviour with respect to constraints. Secondly, the boolean requirement limits the applicability of these metrics to more general constraint satisfaction problems (CSPs), which can have non-boolean domains. In response, we present dual metrics, derived from existing primal (boolean assignment) metrics, that are based on the states of constraints during the search. Experimental results show a strong relationship between the primal and dual versions of these metrics on a variety of random and structured problems. This dual perspective can be easily applied to both SAT and general CSPs, allowing for new insights into the workings of a broad class of local search methods.
展开▼
