A previously developed quantum search algorithm for solving 1-SAT problems in a single step is generalized to apply to a range of highly constrained k-SAT problems. We identify a bound on the number of clauses in satisfiability problems for which the generalized algorithm can find a solution in a constant number of steps as the number of variables increases. This performance contrasts with the linear growth in the number of steps required by the best classical algorithms, and the exponential number required by classical and quantum methods that ignore the problem structure. In some cases, the algorithm can also guarantee that insoluble problems in fact have no solutions, unlike previously proposed quantum search algorithms.
We present a quantum computer heuristic search algorithm for graph coloring. This algorithm uses a new quantum operator, appropriate for nonbinary-valued constraint satisfaction problems, and information available in partial colorings. We evaluate the algorithm empirically with small graphs near a phase transition in search performance. It improves on two prior quantum algorithms: unstructured search and a heuristic applied to the satisfiability (SAT) encoding of graph coloring. An approximate asymptotic analysis suggests polynomial-time cost for hard graph coloring problems, on average.
From a computational perspective, there is a close connection between various probabilistic reasoning tasks and the problem of counting or sampling satisfying assignments of a propositional theory. We consider the question of whether state-of-the-art satisfiability procedures, based on random walk strategies, can be used to sample uniformly or nearuniformly from the space of satisfying assignments. We first show that random walk SAT procedures often do reach the full set of solutions of complex logical theories. Moreover, by interleaving random walk steps with Metropolis transitions, we also show how the sampling becomes near-uniform.
Backtrack search algorithms for Propositional Satisfiability (SAT) have seen significant improvements in recent years (Bayardo Jr. & Schrag 1997; Zhang 1997; Gomes, Selman, & Kautz 1998; Marques-Silva & Sakallah 1999; Prestwich 2000; Moskewicz et al. 2001). These improvements result from new search pruning techniques as well as new strategies for how to organize the search. Effective search pruning techniques include, among others, clause recording and non-chronological backtracking (Bayardo Jr. & Schrag 1997; Marques-Silva & Sakallah 1999; Moskewicz et al. 2001), whereas recent effective strategies include restarts (Gomes, Selman, & Kautz 1998) and (very recently) randomized backtracking (Prestwich 2000). Intrinsic to several of these improvements is randomization. Randomization has found application in different SAT algorithms, that include local search and backtrack search algorithms (McAllester, Selman, Kautz 1997; Bayardo Jr. & Schrag 1997). In backtrack search, current state-of-the-art SAT solvers extensively resort to randomization, most often for selecting variable assignments but (and as a result) also within search restart strategies. Search restarts are a well-known Copyright 2001, American Association for Artificial Intelligence (www.aaai.org).