COMBINATORIC OF MINIMALLY UNSATISFIABLE CLAUSE-SETS
Lead Research Organisation:
Swansea University
Department Name: College of Science
Abstract
The basics of the anticipated PhD topic, the study of minimally unsatisfiable formulas (MUs) of low complexity,
have been established. A first result, to be submitted to SAT 2017 (the main conference of the field) in March,
is a new proof of the MU(2)-characterisation.
Also a first journal submission should come out of this, which will include more material on MU(1).
So I am happy with the progress, and I am confident that the PhD will be successfully completed.
have been established. A first result, to be submitted to SAT 2017 (the main conference of the field) in March,
is a new proof of the MU(2)-characterisation.
Also a first journal submission should come out of this, which will include more material on MU(1).
So I am happy with the progress, and I am confident that the PhD will be successfully completed.
Organisations
People |
ORCID iD |
| Oliver Kullmann (Primary Supervisor) | |
| Hoda Abbasizanjani (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509553/1 | 01/10/2016 | 30/06/2022 | |||
| 1773023 | Studentship | EP/N509553/1 | 01/10/2015 | 30/11/2019 | Hoda Abbasizanjani |
| Description | My research is about Boolean Satisfiability problem (SAT). In simple words, SAT is about a list of constraints, all of which we want to satisfy simultaneously. Each constraint might be very easy to satisfy individually, but satisfying all of them might be very difficult since there might be many conflicts between constraints. The task of modeling and reasoning about real-world problems often involves analyzing over-constrained representations, where not all constraints of a problem can be simultaneously satisfied. In many cases, knowing that a problem is unsatisfiable is not enough and the need to analyze over-constrained (or unsatisfiable) problems occurs in many settings, including data and knowledge bases, artificial intelligence, applied formal methods, operations research and description logics. For example consider an engineer designing a system with a desire specification. If the system is inconsistent, we cannot just delete a part of our system, because we need the functionalities contained in that part. Instead, we would like to locate and understand the problem, and, basing on this information, re-design only the small part of the system causing the problem. So the main focus of my research is to understand these unsatisfiable problems and their underlying structure. An interesting fact is that the structure of these unsatisfiable problems is independent of the application, once we have same constrains we get same structure. So far we have characterized the structure of the most fundamental classes of unsatisfiable problems and we are working on characterizing more classes of these problems. |
| Exploitation Route | As mentioned earlier a wide range of computational problems in various fields can be represented as a SAT problem and in the case of unsatisfiability, our findings will help researchers and engineers to understand an unsatisfiable problem and to re-store satisfiability with minimum efforts. |
| Sectors | Digital/Communication/Information Technologies (including Software),Electronics |
| URL | http://cs.swan.ac.uk/~cshoda/ |
| Description | British Colloquium for Theoretical Computer Science 2018 |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | International |
| Primary Audience | Postgraduate students |
| Results and Impact | I gave a talk at the British Colloquium for Theoretical Computer Science 2018, Royal Holloway, University of London. The talk was about specific research topic during my PhD at Swansea university. The main audience were from research students and early career researchers in Computer Science. After my talk there was a discussion regarding possible extensions of my work and some interesting ideas were suggested. |
| Year(s) Of Engagement Activity | 2018 |
| URL | http://bctcs18.cs.rhul.ac.uk/ |
| Description | Parallel Simulink Simulations on Cluster |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Other audiences |
| Results and Impact | The presentation took place during my industrial internship at Jaguar Land Rover. The company has a Simulink-based analysis tool to simulate vehicle level behaviour, as a substitute for physical tests. As each full simulation using this tool takes at least 10 minutes, performing large number of simulations is too much time consuming. So for this reason I managed to write a set of scripts in order to successfully run the tool on the company's cluster and speed up the simulations by leveraging the MATLAB parallel computing tool. And in the presentation I talked about the methodology and tool I used to do this. |
| Year(s) Of Engagement Activity | 2019 |
| Description | Research Away Day (Department of Computer Science, Swansea University) |
| Form Of Engagement Activity | A talk or presentation |
| Part Of Official Scheme? | No |
| Geographic Reach | Local |
| Primary Audience | Postgraduate students |
| Results and Impact | The research away day of Department of Computer Science included research talks from PhD students and Research Assistants regarding their research.The audience were PhD students, Research Assistants and lecturers from Department of Computer Science, Swansea University. The questions and discussions followed each talks. In my presentation, I talked about main focus of my research. |
| Year(s) Of Engagement Activity | 2017 |