| EPSRC Reference: |
GR/S58393/01 |
| Title: |
An algorithmic platform for efficient satisfiability based problem solving |
| Principal Investigator: |
Kullmann, Dr O |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
Swansea University |
| Scheme: |
First Grant Scheme Pre-FEC |
| Starts: |
03 February 2004 |
Ends: |
02 April 2007 |
Value (£): |
111,440
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The SAT problem is to decide, given a set of boolean constraints, whether there is a global solution satisfying all constraints. It is one of the most versatile problems in complexity theory, and many problems of practical relevance can be formulated as SAT problems and solved by means of highly optimised SAT solvers. Based on novel theoretical approaches, and starting with one of the strongest (award-winning) solvers, OKsolver, the goal of this project is to develop new techniques and algorithms for SAT solving, and to integrate the corresponding tools into an algorithmic platform, supporting a wide spectrum of users.OKsolver will be evolved into the generic library OKlibrary for SAT solving. This library will support the new algorithmic methods together with a broad range of alternative techniques, and its design and implementation will exploit current methods from Generative Programming. OKlibrary is designed to play the same role for SAT solving as the STL library for C++ programming in general, and will also fully generalise to non-boolean domains. A breakthrough in our understanding of heuristics is envisaged by exploring adaptive meta.heuristics in combination with investigations in statistical physics. The adaptive heuristics will be based on data mining in the database OKdatabase for random formulas, which will be a rich source for data on phase transitions in SAT. The whole software plus user interfaces is to be inteqrated into OKplatform.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.swan.ac.uk |