Nathan Bruning, Tim Koopman, Siem Kok, Joris Scharpff, Jip-Man Vuong. Applying Extended Resolution and Forced Patterns on Random 3-SAT instances. Technical Report Delft University of Technology, 02 2009.
In this study we aim to improve the runtime of the state-of-the-art March SAT solver. We apply a technique known as extended resolution on uniform random 3- SAT formulae; we add additional clauses, derived from the original formula, trying to guide the solver into the direction of a viable solution. Depending on a heuris- tic which we introduce, we add certain patterns to the formula to aid the solver. This method will be tested both unforced and forced: the unforced method lets the solver choose whether to include the additional clauses or not, in forced solving the patterns are used anyway. The latter might turn a satisfiable problem into an unsatisfiable one, however results still are very promising: a speed up of about 18% on the average. Also, at the end of this document some valuable insights into new studies can be found, which may lead to even more substantial improvements.