Thao Duong

The increasing availability of MRI brain data opens up a research direction for abnormality detection which is necessary to on-time detection of impairment and performing early diagnosis. The paper proposes scores based on z-score transformation and kernel density estimation (KDE) which are respectively Gaussian-based assumption and nonparametric modeling to detect the abnormality in MRI brain images. The methodologies are applied on gray-matter-based score of Voxel-base Morphometry (VBM) and sparse-based score of Sparse-based Morphometry (SBM). The experiments on well-designed normal control (CN) and Alzheimer disease (AD) subsets extracted from MRI data set of Alzheimer’s Disease Neuroimaging Initiative (ADNI) are conducted with threshold-based classification. The analysis of abnormality percentage of AD and CN population is carried out to validate the robustness of the proposed scores. The further cross validation on Linear discriminant analysis (LDA) and Support vector machine (S VM) classification between AD and CN show significant accuracy rate, revealing the potential of statistical modeling to measure abnormality from a population of normal subjects.

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 weight-enhanced 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.

This paper presents an efficient trap escape strategy in stochastic local search for Satisfiability. The proposed method aims to enhance local search by providing 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 minima. Hence, a list of backtracked conflict variables is retrieved from local minima. 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 selecting 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 Competition 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.

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.

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 benchmark 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.