Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
solver [2013/04/09 12:03] vkuncak |
solver [2013/04/25 19:29] regis.blanc |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| * http://www.scala-lang.org/gsoc2013 | * http://www.scala-lang.org/gsoc2013 | ||
| - | The goal of this project is to develop a reasonably efficient constraint solver in Scala. You will build on a SAT solver we are currently releasing and will add incremental SAT solving capabilities as well as reasoning about functional data structures. The constraint solver can be used for constraint programming, automated testing, verification, and synthesis in Scala. | + | The goal of this project is to develop a reasonably efficient constraint solver in Scala. You will build on a SAT solver we are developing and will add incremental SAT solving capabilities as well as reasoning about functional data structures. The constraint solver can be used for constraint programming, automated testing, verification, and synthesis in Scala. |
| + | |||
| + | The following report describes the SAT solver: | ||
| + | * https://infoscience.epfl.ch/record/186129 | ||
| + | |||
| + | The solver is open source and available on GitHub: | ||
| + | * https://github.com/regb/scabolic | ||
| Constraints solvers are fast theorem provers for certain classes of constraints, including propositional logic, theories of algebraic data types, integer arithmetic, arrays, and other theories of interest. Many great tools currently use [[http://combination.cs.uiowa.edu/smtlib/|off-the-shelf SMT solvers]]. Having a solver fully in Scala would open up further possibilities for integration and optimizations at the boundary between the solver and the system that uses it. It would also simplify the deployment of such tools. | Constraints solvers are fast theorem provers for certain classes of constraints, including propositional logic, theories of algebraic data types, integer arithmetic, arrays, and other theories of interest. Many great tools currently use [[http://combination.cs.uiowa.edu/smtlib/|off-the-shelf SMT solvers]]. Having a solver fully in Scala would open up further possibilities for integration and optimizations at the boundary between the solver and the system that uses it. It would also simplify the deployment of such tools. | ||
| Line 26: | 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 34: | 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 ===== | ||