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 22 articles )

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

1 2 next

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

1 2 next

Further publications can be found at: