URSA: A System for Uniform Reduction to SAT
Lecturer: Predrag Janicic
Title: URSA: A System for Uniform Reduction to SAT
Date: 29 october 2019, 14.30
Location: University of Milan, Dept Computer Science, via Celoria 18,
8th floor, Department Council Meeting Room
Contact person: Fabio Scotti
There is a huge number of problems, from various areas, being solved by reduction to SAT. However, for many applications, translation to SAT is performed by specialized, problem-specific tools. In this talk, a system for uniform solving of a wide class of problems by reducing them to SAT, URSA, will be presented. The system uses a new specification language that combines imperative and declarative programming paradigms. So, the system can be seen not only as a tool for solving problems by reducing them to SAT, but also as a general-purpose constraint solving system (for finite domains). Some applications of URSA will also be briefly discussed: for proving conjectures related to some combinatorial geometry problems, for some chess-related problems, and for some cryptography problems.
Predrag Janicic received a PhD in computer science from the University of Belgrade in 2001, where he now holds a position of full professor. He has published 7 books, 1 book chapter and more than 50 research article in international journals and conferences. His main research interests are in the area of automated reasoning (automated theorem proving in coherent logic, automated and interactive proving of geometrical theorems, SAT/SMT) and mathematical software (dynamic geometry software, symbolic computation). He worked as a visiting researcher at the University of Edinburgh and visited a number of other universities (including Birmingham, Heriot-Watt, Cambridge, TU Berlin, Genova, Coimbra, Linz, Graz, "La Sapienza", EPFL, Strasbourg).