Uniform Reduction to SAT and SMT
Event details
| Date | 20.06.2011 |
| Hour | 16:15 |
| Speaker | Prof. Predrag Janicic, University of Belgrade |
| Location | |
| Category | Conferences - Seminars |
SAT is a problem of satisfiability in propositional logic, and the satisfiability modulo theory (SMT) is a problem of satisfiability with respect to a background theory (e.g., linear arithmetic, theory of arrays) expressed in classical first-order logic with equality. Over the last decade, SAT and SMT solvers made tremendous advances both in theoretical and in practical aspects. They have a wide range of applications, primarily in software verification, planning, scheduling, cryptanalysis, electronic design automation, etc. Typically, problems are reduced to SAT/SMT by problem-specific, ad-hoc tools. In this talk, a general framework, URSA Major, for reducing problems to SAT/SMT will be presented. The system can be also considered as a general modelling system for specifying and solving a wide class of problems (e.g., NP problems). The specification language is C-like, but based on a novel imperative-declarative programming paradigm. A problem is specified by a test (expressed in an imperative form) that given values indeed make a solution to the problem. From a problem specification, a corresponding propositional or first-order formula (in a suitable theory) is generated and passed to a SAT/SMT solver. If the formula is satisfiable, then its model is transformed back to the values of the unknowns. The system will be illustrated by examples from several domains. Prof. Janicic's homepage
Practical information
- General public
- Free