Improving GSAT using 2SAT

Peter J. Stuckey, Lei Zheng

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)


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.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming- CP 2002 - 8th International Conference, CP 2002, Proceedings
EditorsPascal Van Hentenryck
Number of pages5
ISBN (Print)3540441204, 9783540441205
Publication statusPublished - 1 Jan 2002
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2002 - Ithaca, United States of America
Duration: 9 Sept 200213 Sept 2002
Conference number: 8th

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceInternational Conference on Principles and Practice of Constraint Programming 2002
Abbreviated titleCP 2002
Country/TerritoryUnited States of America

Cite this