Trap escape for local search by backtracking and conflict reverse
View/ Open
Author(s)
Huu-Phuoc, Duong
Thach-Thao, Duong
Duc, Nghia Pham
Sattar, Abdul
Anh, Duc Duong
Griffith University Author(s)
Year published
2013
Metadata
Show full item recordAbstract
This paper presents an efficient trap escape strategy in stochastic local search for Satisfiability. The proposed method aims to enhance local search by pro- viding an alternative local minima escaping strategy. Our variable selection scheme provides a novel local minima escaping mechanism to explore new solution areas. Conflict variables are hypothesized as variables recently selected near local min- ima. Hence, a list of backtracked conflict variables is retrieved from local min- ima. The new strategy selects variables in the backtracked variable list based on the clause-weight scoring function and stagnation weights ...
View more >This paper presents an efficient trap escape strategy in stochastic local search for Satisfiability. The proposed method aims to enhance local search by pro- viding an alternative local minima escaping strategy. Our variable selection scheme provides a novel local minima escaping mechanism to explore new solution areas. Conflict variables are hypothesized as variables recently selected near local min- ima. Hence, a list of backtracked conflict variables is retrieved from local min- ima. The new strategy selects variables in the backtracked variable list based on the clause-weight scoring function and stagnation weights and variable weights as tiebreak criteria. This method is an alternative to the conventional method of se- lecting variables in a randomized unsatisfied clause. The proposed tiebreak method favors high stagnation weights and low variable weights during trap escape phases. The new strategies are examined on verification benchmark and SAT Competi- tion 2011 and 2012 application and crafted instances. Our experiments show that proposed strategy has comparable performance with state-of-the-art local search solvers for SAT.
View less >
View more >This paper presents an efficient trap escape strategy in stochastic local search for Satisfiability. The proposed method aims to enhance local search by pro- viding an alternative local minima escaping strategy. Our variable selection scheme provides a novel local minima escaping mechanism to explore new solution areas. Conflict variables are hypothesized as variables recently selected near local min- ima. Hence, a list of backtracked conflict variables is retrieved from local min- ima. The new strategy selects variables in the backtracked variable list based on the clause-weight scoring function and stagnation weights and variable weights as tiebreak criteria. This method is an alternative to the conventional method of se- lecting variables in a randomized unsatisfied clause. The proposed tiebreak method favors high stagnation weights and low variable weights during trap escape phases. The new strategies are examined on verification benchmark and SAT Competi- tion 2011 and 2012 application and crafted instances. Our experiments show that proposed strategy has comparable performance with state-of-the-art local search solvers for SAT.
View less >
Conference Title
TWELFTH SCANDINAVIAN CONFERENCE ON ARTIFICIAL INTELLIGENCE (SCAI 2013)
Volume
257
Publisher URI
Copyright Statement
© 2013 IOS Press. This is the author-manuscript version of this paper. Reproduced in accordance with the copyright policy of the publisher. Please refer to the publisher website for access to the definitive, published version.
Subject
Artificial intelligence not elsewhere classified