Improving GSAT using 2SAT

Abstract

GSAT has been proven highly effective for solving certain classes of large SAT problems. It starts from a randomly generated truth assignment and tries to reduce the number of violated clauses by iteratively flipping some variables’ truth value. GSATs effectiveness arises from the speed of a single flip, since this allows a large space of possible solutions to be explored. It does not examine any inter-relationship between the clauses of the problem it attacks.2SAT problems are highly tractable (linear time solvable), and some SAT problems, such as graph colouring, contain a high proportion of 2SAT information. In this paper we show how we can alter GSAT to take into account the 2SAT clauses, so that it never investigates truth assignments that violate a binary clause. This reduces the search space considerably. We give experimental results illustrating the benefit of our new approach on hard 3SAT problems involving a substantial 2SAT component.