Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
solver [2013/04/23 10:37] regis.blanc |
solver [2013/04/26 21:12] vkuncak |
||
|---|---|---|---|
| Line 23: | Line 23: | ||
| ===== Related Projects ===== | ===== Related Projects ===== | ||
| + | |||
| + | * [[https://github.com/ingoem/cassowary-scala|Constraint Solver that Includes Simplex Solver]] | ||
| * [[http://lara.epfl.ch/w/software|LARA Software]] | * [[http://lara.epfl.ch/w/software|LARA Software]] | ||
| Line 32: | Line 34: | ||
| * {{projects:9_-_zhang01efficient.pdf|Efficient conflict driven learning in a boolean satisfiability solver}} | * {{projects:9_-_zhang01efficient.pdf|Efficient conflict driven learning in a boolean satisfiability solver}} | ||
| * {{projects:minisat-anextensiblesatsolver.pdf|An Extensible SAT-solver}} (original MiniSat implementation description) | * {{projects:minisat-anextensiblesatsolver.pdf|An Extensible SAT-solver}} (original MiniSat implementation description) | ||
| + | |||
| ===== SMT (Satisfiability Modulo Theories) ===== | ===== SMT (Satisfiability Modulo Theories) ===== | ||
| Line 40: | Line 43: | ||
| * {{model-based.pdf|Model-Based Theory Combination}} | * {{model-based.pdf|Model-Based Theory Combination}} | ||
| * {{projects:krstic-goel.pdf|Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL}} | * {{projects:krstic-goel.pdf|Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL}} | ||
| + | * [[http://www.google.ch/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&ved=0CDMQFjAA&url=http%3A%2F%2Fwww.math.uiowa.edu%2Fftp%2Ftinelli%2Fpapers%2FBarST-RR-05.pdf&ei=9GZ5UZfTFsi0PKWpgPgJ&usg=AFQjCNF6gUCgDuVNF2_lo2k7-KFsfAnMhQ&sig2=0QV3IFjocYkEm-TKE8EgLA&bvm=bv.45645796,d.ZWU|An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types]] | ||
| ===== Model Finding ===== | ===== Model Finding ===== | ||
| Line 47: | Line 51: | ||
| * {{projects:weber-hol-models.pdf|Bounded Model Generation for Isabelle/HOL}} | * {{projects:weber-hol-models.pdf|Bounded Model Generation for Isabelle/HOL}} | ||
| * {{projects:ruemmerThesis.pdf|Calculi for Program Incorrectness and Arithmetic}}, Philipp Rümmer's PhD thesis | * {{projects:ruemmerThesis.pdf|Calculi for Program Incorrectness and Arithmetic}}, Philipp Rümmer's PhD thesis | ||
| - | |||