Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
solver [2013/04/23 10:37] regis.blanc |
solver [2013/04/25 19:29] regis.blanc |
||
|---|---|---|---|
| Line 32: | Line 32: | ||
| * {{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 41: | ||
| * {{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 ===== | ||