Reinforcement Learning for SAT encodings of constraint models
Lead Research Organisation:
University of York
Department Name: Computer Science
Abstract
This poject seeks to use machine learning to find the best translation of a sophisticated real-world problem into a Boolean Satisfiability Problem, allowing the use of efficient solvers to ultimately address the original problem.
| Description | So far we have shown empirically that it is possible to automatically select representations which improve the speed of solving constraint satisfaction problems when encoded to Boolean formulae. From our corpus of constraint satisfaction problems, we have identified and extracted features which relate to certain types of constraint and used them to train machine-learning models which can make better predictions than using generic problem-specific features, or indeed than just using the overall best representation. |
| Exploitation Route | This approach could be extended to other constraint types and indeed to other decisions in the problem-solving process. |
| Sectors | Creative Economy,Digital/Communication/Information Technologies (including Software),Electronics,Transport |
| Description | Girona |
| Organisation | University of Girona |
| Country | Spain |
| Sector | Academic/University |
| PI Contribution | My supervisors and I worked with 4 academics from the University of Girona on a journal paper. I carried out some analysis on the workings of the proposed new encodings of constraints. I also contributed explanatory diagrams and plots to the paper. |
| Collaborator Contribution | Our collaborators in Girona developed some specialised encodings of pseudo-Boolean constraints into Boolean SAT - the focus of the journal paper |
| Impact | A paper accepted in the Journal of Artificial Intelligence (see URL). |
| Start Year | 2020 |
| Description | St Andrews |
| Organisation | University of St Andrews |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | My supervisor and I have worked on a paper submitted to a high-quality journal together with academics from St. Andrews. I carried out the vast majority of experiments, aggregated and reported on results in several cycles, to enable further questions to be posed and answered. I provided all the plots for the paper. |
| Collaborator Contribution | Our collaborators helped by proposing suitable problem instances to attempt, and by writing explanations of the features of problems which would be exploited by the main contribution presented in the paper. We held weekly meetings to discuss the research, at which everyone participated with suggestions and questions. Everyone was involved in writing parts of the paper. |
| Impact | The main article in question is under review with the Artificial Intelligence journal. |
| Start Year | 2019 |
| Description | TakeAIM |
| Form Of Engagement Activity | Participation in an activity, workshop or similar |
| Part Of Official Scheme? | No |
| Geographic Reach | National |
| Primary Audience | Industry/Business |
| Results and Impact | I submitted an entry to the "Take AIM" competition run by the Smith Institute - the challenge was to explain our (mathematically-related) work to a lay readership in fewer than 250 words. |
| Year(s) Of Engagement Activity | 2021 |
| URL | https://www.smithinst.co.uk/takeaim/ |