SmArT solving

Abstract

The satisfiability problem (Sat) lies at the core of the complexity theory. This is a decision problem: Not the solution itself, but whether or not a solution exists given a specified set of requirements is the central question. Over the years, the satisfiability problem has taken center stage as a means of effective representation to tackle problems with different characteristics: Many problems can first be translated into Sat and then solved by means of software dedicated to the Sat problem. Due to the increasing power of these Sat solvers, the number of applications climbs every year. Examples of this kind of translatable problems are scheduling problems, verification of software and hardware, bounded model checking and a wide variety of mathematical puzzles. Sat solvers come in two flavors: Complete and incomplete. Complete solvers systematically go over the whole search space and are able to determine with certainty whether a solution exists. Incomplete Sat solvers look for a solution at a venture. They dont follow a system, yet they might hit a solution. Most complete Sat solvers are based on the ConflictDriven architecture. At a dead end, they analyze what went wrong and where in the search space it happened. Then they resume the search from there. Conflict-driven solvers make relatively cheap decisions (in terms of computational costs), which enables them to search the space swiftly. Only a few complete Sat solvers are based on an architecture that chooses its battles, so to speak. The LookAhead architecture peers further into the search space before making the next move. Look-ahead solvers make expensive decisions in order to keep the search space as small as possible. Incomplete Sat solvers have a dominant and a rare type of architecture as well. The commonly used WalkSat makes cheap decisions, while UnitWalk a bit off the wall makes more costly moves. This thesis deals with a number of contributions to the development of Sat solvers both complete and incomplete. With the adagium poundwise, Pennyfoolish in mind, its focus is primarily set on both rare, more expensive approaches. On one hand, expensive procedures are implemented efficiently to reduce their relative costs, while they maintain their impact on the search space. On the other hand, building up reasoning power further limits the search space. The growing attention for Sat solvers generates a growing group of users. More and more of them will not be familiar with the specific ins and outs of their application, which makes it difficult to tune the Sat solvers. Here, adaptive heuristics may be of use. Given a specific problem, these heuristics set the parameters in such a way that the solver performs (almost) optimally. This thesis presents some elegant adaptive heuristics for a technique that looks even further ahead into the search area to learn even more: The DoubleLook procedure. Thanks to these adaptive heuristics that keep on fine-tuning the parameters on the fly this binocular-technique can be helpful to solve more problems. The raison dÊtre of incomplete Sat solvers is the assumption that on many problems, they find a solution faster than complete solvers. Yet they are only superior within a certain niche; they work well on big (random) problems. To extend the span of incomplete Sat solvers, this thesis presents a Sat solver with the more rarely used UnitWalk architecture. Several expensive calculations are run simultaneously on a single processor which keeps costs relatively low. In addition, the solver features some communicative skills: Whenever a solution is found for part of the problem, all further calculations will run more efficiently. Despite these enhancements and its good results, this solver is not (yet) competitive on structured problems; an field dominated by complete Sat solvers. However, our complete Sat solver march, based on the LookAhead architecture, has won many awards in the prestigious Sat competitions, among which the gold medal for random problems without solutions (2007); a traditional stronghold of LookAhead solvers. More intriguing is the gold medal for crafted problems with solutions (2007). This is a field which is dominated besides march by conflict-driven solvers. In conclusion, the new techniques presented in this thesis have enhanced the LookAhead architecture to such an extend, that this type of solvers can compete on more problems while sustaining dominance on random instances.