RSat is a complete Boolean satisfiability solver with an exhaustive search interface for applications such as model counting and knowledge compilation. RSat uses a phase selection heuristic that is oriented toward reducing work repetition and a frequent restart policy. For a complete description of RSat please see the list of papers. RSat won gold medals from the SAT’07 competition in the industrial category. The previous version of RSat also won the third place in SAT-Race 2006. RSat is developed by the UCLA Automated Reasoning Group.

References in zbMATH (referenced in 18 articles )

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

  1. Dilkina, Bistra; Gomes, Carla P.; Sabharwal, Ashish: Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search (2014)
  2. Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014)
  3. Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron: 6 years of SMT-COMP (2013) ioport
  4. Guo, Wen-Sheng; Yang, Guo-Wu; Hung, William N.N.; Song, Xiaoyu: Complete Boolean satisfiability solving algorithms based on local search (2013)
  5. Lagniez, Jean-Marie; Biere, Armin: Factoring out assumptions to speed up MUS extraction (2013)
  6. Gogate, Vibhav; Dechter, Rina: SampleSearch: importance sampling in presence of determinism (2011)
  7. Katebi, Hadi; Sakallah, Karem A.; Marques-Silva, João P.: Empirical study of the anatomy of modern SAT solvers (2011)
  8. Kroc, Lukas; Sabharwal, Ashish; Selman, Bart: Leveraging belief propagation, backtrack search, and statistics for model counting (2011)
  9. Pipatsrisawat, Knot; Darwiche, Adnan: On the power of clause-learning SAT solvers as resolution engines (2011)
  10. Brummayer, Robert; Lonsing, Florian; Biere, Armin: Automated testing and debugging of SAT and QBF solvers (2010)
  11. Kilani, Yousef: Improving GASAT by replacing tabu search by DLM and enhancing the best members (2010) ioport
  12. Pipatsrisawat, Knot; Darwiche, Adnan: On modern clause-learning satisfiability solvers (2010) ioport
  13. Sturm, Thomas; Zengler, Christoph: Parametric quantified SAT solving (2010)
  14. Brummayer, Robert; Biere, Armin: Lemmas on demand for the extensional theory of arrays (2009)
  15. Chieu, H.L.; Lee, W.S.: Relaxed survey propagation for the weighted maximum satisfiability problem (2009)
  16. Audemard, G.; Bordeaux, L.; Hamadi, Y.; Jabbour, S.; Sais, L.: A generalized framework for conflict analysis (2008)
  17. Biere, Armin: Adaptive restart strategies for conflict driven SAT solvers (2008)
  18. Eibach, Tobias; Pilz, Enrico; Völkel, Gunnar: Attacking Bivium using SAT solvers (2008)

Further publications can be found at: