A Study of Local Minimum Avoidance Heuristics for SAT

Paper


Duong, Thach-Thao, Pham, Duc Nghia and Sattar, Abdul. 2012. "A Study of Local Minimum Avoidance Heuristics for SAT." De Raedt, Luc, Bessiere, Christian, Dubois, Didier, Doherty, Patrick, Frasconi, Paolo, Heintz, Fredrik and Lucas, Peter (ed.) 20th European Conference on Artificial Intelligence (ECAI 2012). Montpellier, France 27 - 31 Aug 2012 Netherlands. https://doi.org/10.3233/978-1-61499-098-7-300
Paper/Presentation Title

A Study of Local Minimum Avoidance Heuristics for SAT

Presentation TypePaper
AuthorsDuong, Thach-Thao (Author), Pham, Duc Nghia (Author) and Sattar, Abdul (Author)
EditorsDe Raedt, Luc, Bessiere, Christian, Dubois, Didier, Doherty, Patrick, Frasconi, Paolo, Heintz, Fredrik and Lucas, Peter
Journal or Proceedings TitleFrontiers in Artificial Intelligence and Applications
ERA Conference ID42769
Journal Citation242, pp. 300-305
Number of Pages6
Year2012
Place of PublicationNetherlands
ISSN0922-6389
1879-8314
ISBN9781614990970
9781614990987
Digital Object Identifier (DOI)https://doi.org/10.3233/978-1-61499-098-7-300
Web Address (URL) of Paperhttps://ebooks.iospress.nl/publication/6989
Conference/Event20th European Conference on Artificial Intelligence (ECAI 2012)
European Conference on Artificial Intelligence
Event Details
European Conference on Artificial Intelligence
ECAI
Rank
A
A
A
A
A
A
Event Details
20th European Conference on Artificial Intelligence (ECAI 2012)
Event Date
27 to end of 31 Aug 2012
Event Location
Montpellier, France
Abstract

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.

KeywordsArtificial intelligence; Local search (optimization); Stochastic systems; Verification
ANZSRC Field of Research 2020460210. Satisfiability and optimisation
Byline AffiliationsGriffith University
Institution of OriginUniversity of Southern Queensland
Permalink -

https://research.usq.edu.au/item/q711w/a-study-of-local-minimum-avoidance-heuristics-for-sat

Download files


Published Version
  • 34
    total views
  • 34
    total downloads
  • 2
    views this month
  • 2
    downloads this month

Export as

Related outputs

Moving Objects Segmentation in Video Sequence based on Bayesian network
Duong, Thach-Thao and Duong, Anh-Duc. 2010. "Moving Objects Segmentation in Video Sequence based on Bayesian network." 8th IEEE-RIVF International Conference on Computing and Communication Technologies: Research, Innovation and Vision for the Future (RIVF 2010). Hanoi, Vietnam 01 - 04 Nov 2010 https://doi.org/10.1109/RIVF.2010.5633458
Trap Avoidance in Local Search Using Pseudo-Conflict Learning
Pham, Duc Nghia, Duong, Thach-Thao and Sattar, Abdul. 2012. "Trap Avoidance in Local Search Using Pseudo-Conflict Learning." 26th AAAI Conference on Artificial Intelligence (AAAI 2012). Toronto, Canada 22 - 26 Jul 2012 United States.
Weight-Enhanced Diversification in Stochastic Local Search for Satisfiability
Duong, Thach-Thao, Pham, Duc Nghia, Sattar, Abdul and Newton, M. A. Hakim. 2013. "Weight-Enhanced Diversification in Stochastic Local Search for Satisfiability." Rossi, Francesca (ed.) 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013). Beijing, China 03 - 09 Aug 2013
Integrated data envelopment analysis: Linear vs. nonlinear model
Mahdiloo, Mahdi, Toloo, Mehdi, Duong, Thach-Thao, Saen, Reza Farzipoor and Tatham, Peter. 2018. "Integrated data envelopment analysis: Linear vs. nonlinear model." European Journal of Operational Research. 268 (1), pp. 255-267. https://doi.org/10.1016/j.ejor.2018.01.008
Some comments on improving discriminating power in data envelopment models based on deviation variables framework
Mahdiloo, Mahdi, Lim, Sungmook, Duong, Thach-Thao and Harvie, Charles. 2021. "Some comments on improving discriminating power in data envelopment models based on deviation variables framework." European Journal of Operational Research. 295 (1), pp. 394-397. https://doi.org/10.1016/j.ejor.2021.02.056
Trap escape for local search by backtracking and conflict reverse
Duong, Huu-Phuoc, Duong, Thach-Thao, Pham, Duc Nghia, Sattar, Abdul and Duong, Anh Duc. 2013. "Trap escape for local search by backtracking and conflict reverse." Jaeger, Manfred, Nielsen, Thomas Dyhre and Viappiani, Paolo (ed.) 12th Scandinavian Conference on Artificial Intelligence (SCAI 2013). Aalborg, Denmark 20 - 22 Nov 2013 Amsterdam. https://doi.org/10.3233/978-1-61499-330-8-85
Diversify Intensification Phases in Local Search for SAT with a New Probability Distribution
Duong, Thach-Thao, Pham, Duc-Nghia and Sattar, Abdul. 2013. "Diversify Intensification Phases in Local Search for SAT with a New Probability Distribution." Cranefield, Stephen and Nayak, Abhaya (ed.) 26th Australasian Joint Conference on Artificial Intelligence (AI 2013). Dunedin, New Zealand 01 - 06 Dec 2013 Switzerland. https://doi.org/10.1007/978-3-319-03680-9_18
A Method to Avoid Duplicative Flipping in Local Search for SAT
Duong, Thach-Thao, Pham, Duc Nghia and Sattar, Abdul. 2012. "A Method to Avoid Duplicative Flipping in Local Search for SAT." Thielscher, Michael and Zhang, Dongmo (ed.) 25th Australasian Joint Conference on Artificial Intelligence (AI 2012). Sydney, Australia 04 - 07 Dec 2012 Berlin. https://doi.org/10.1007/978-3-642-35101-3_19
Image retrieval based on visual information concepts and automatic image annotation
Ly, Quoc Ngoc, Duong, Anh Doc, Duong, Thach Thao and Ngo, Duc Thanh. 2006. "Image retrieval based on visual information concepts and automatic image annotation." Duc, Duong Anh, Dong, Thuy Thi Bich, Ho, Tu-Bao and Nguyen, Dinh Thuc (ed.) 1st International Conference on Theories and Applications of Computer Science (ICTACS 2006). Ho Chi Minh City, Vietnam 03 - 05 Aug 2006 United States. https://doi.org/10.1142/9789812772671_0006