In this paper we present a new randomized algorithm for SAT, i.e., the satisfiability problem for Boolean formulas in conjunctive normal form. Despite its simplicity, this algorithm performs well on many common benchmarks ranging from graph coloring problems to microprocessor verification. Our algorithm is inspired by two randomized algorithms having the best current worst-case upper bounds. We combine the main ideas of these algorithms in one algorithm. The two approaches we use are local search (which is used in many SAT algorithms, e.g., in GSAT and WalkSAT) and unit clause elimination (which is rarely used in local search algorithms). In this paper we do not prove any theoretical bounds. However, we present encouraging results of computational experiments comparing several implementations of our algorithm with other SAT solvers. We also prove that our algorithm is probabilistically approximately complete.

References in zbMATH (referenced in 33 articles , 1 standard article )

Showing results 1 to 20 of 33.
Sorted by year (citations)

1 2 next

  1. Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
  2. Lai, Xinsheng; Zhou, Yuren: The analysis of expected fitness and success ratio of two heuristic optimizations on two bimodal MaxSat problems (2012)
  3. Saitta, Lorenza; Giordana, Attilio; Cornuéjols, Antoine: Phase transitions in machine learning. (2011)
  4. Audemard, Gilles; Lagniez, Jean-Marie; Mazure, Bertrand; Saïs, Lakhdar: Boosting local search thanks to cdcl (2010)
  5. Belov, Anton; Stachniak, Zbigniew: Improved local search for circuit satisfiability (2010)
  6. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010)
  7. Belov, Anton; Stachniak, Zbigniew: Improving variable selection process in stochastic local search for propositional satisfiability (2009)
  8. Zhou, Yuren; He, Jun; Nie, Qing: A comparative runtime analysis of heuristic algorithms for satisfiability problems (2009)
  9. Goldberg, Eugene: A decision-making procedure for resolution-based SAT-solvers (2008)
  10. Heule, Marijn J.H.; van Maaren, Hans: Parallel SAT solving using bit-level operations (2008)
  11. Järvisalo, Matti; Junttila, Tommi; Niemelä, Ilkka: Justification-based local search with adaptive noise strategies (2008)
  12. Wei, Wanxia; Li, Chu Min; Zhang, Harry: A switching criterion for intensification and diversification in local search for SAT (2008)
  13. Heule, Marijn; van Maaren, Hans: From idempotent generalized Boolean assignments to multi-bit search (2007)
  14. Kautz, Henry; Selman, Bart: The state of SAT (2007)
  15. Chrabakh, Wahid; Wolski, Rich: GridSAT: Design and implementation of a computational grid application (2006)
  16. Chrabakh, Wahid; Wolski, Rich: GridSAT: Design and implementation of a computational grid application (2006)
  17. Goldberg, Eugene: Determinization of resolution by an algorithm operating on complete assignments (2006)
  18. Markström, Klas: Locality and hard SAT-instances (2006)
  19. Brglez, Franc; Li, Xiao Yu; Stallmann, Matthias F.: On SAT instance classes and a method for reliable performance experiments with SAT solvers (2005)
  20. Hirsch, Edward A.; Kojevnikov, Arist: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination (2005)

1 2 next