Author name cluster

Thach-Thao Duong

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

3 papers

2 author rows

IJCAI Conference 2013 Conference Paper

Weight-Enhanced Diversification in Stochastic Local Search for Satisfiability

Thach-Thao Duong
Duc Nghia Pham
Abdul Sattar
M. A. Hakim Newton

Intensification and diversification are the key factors that control the performance of stochastic local search in satisfiability (SAT). Recently, Novelty Walk has become a popular method for improving diversification of the search and so has been integrated in many well-known SAT solvers such as TNM and gNovelty+. In this paper, we introduce new heuristics to improve the effectiveness of Novelty Walk in terms of reducing search stagnation. In particular, we use weights (based on statistical information collected during the search) to focus the diversification phase onto specific areas of interest. With a given probability, we select the most frequently unsatisfied clause instead of a totally random one as Novelty Walk does. Amongst all the variables appearing in the selected clause, we then select the least flipped variable for the next move. Our experimental results show that the new weightenhanced diversification method significantly improves the performance of gNovelty+ and thus outperforms other local search SAT solvers on a wide range of structured and random satisfiability benchmarks.

PDF Details DOI

ECAI Conference 2012 Conference Paper

A Study of Local Minimum Avoidance Heuristics for SAT

Thach-Thao Duong
Duc Nghia Pham
Abdul Sattar 0001

Stochastic local search for satisfiability (SAT) has successfully been applied to solve a wide range of problems. However, it still suffers from a major shortcoming, i. e. being trapped in local minima. In this study, we explore different heuristics to avoid local minima. The main idea is to proactively avoid local minima rather than reactively escape from them. This is worthwhile because it is time consuming to successfully escape from a local minimum in a deep and wide valley. In addition, revisiting an encountered local minimum several times makes it worse. Our new trap avoidance heuristics that operate in two phases: (i) learning of pseudo-conflict information at each local minimum, and (ii) using this information to avoid revisiting the same local minimum. We present a detailed empirical study of different strategies to collect pseudo-conflict information (using either static or dynamic heuristics) as well as to forget the outdated information (using naive or time window smoothing). We select a bench-mark suite that includes all random and structured instances used in the 2011 SAT competition and three sets of hardware and software verification problems. Our results show that the new heuristics significantly outperform existing stochastic local search solvers (including Sparrow2011 - the best local search solver for random instances in the 2011 SAT competition) on all tested benchmarks.

Details

AAAI Conference 2012 Conference Paper

Trap Avoidance in Local Search Using Pseudo-Conflict Learning

Duc Pham
Thach-Thao Duong
Abdul Sattar

A key challenge in developing efficient local search solvers is to effectively minimise search stagnation (i. e. avoiding traps or local minima). A majority of the state-of-the-art local search solvers perform random and/or Novelty-based walks to overcome search stagnation. Although such strategies are effective in diversifying a search from its current local minimum, they do not actively prevent the search from visiting previously encountered local minima. In this paper, we propose a new preventative strategy to effectively minimise search stagnation using pseudo-conflict learning. We define a pseudo-conflict as a derived path from the search trajectory that leads to a local minimum. We then introduce a new variable selection scheme that penalises variables causing those pseudo-conflicts. Our experimental results show that the new preventative approach significantly improves the performance of local search solvers on a wide range of structured and random benchmarks.

PDF Details