Integration of SAT Solving and Machine Learning
SECOND CALL
APPLICATION ID: ALL16
What we are looking for:
Research proposals that explore the synergy between traditional SAT/MaxSAT solving and machine learning techniques. Proposals should aim at developing solvers capable of solving large and complex instances. Of particular interest are proposals aimed at addressing practical scheduling and planning challenges within the domain of assistive robotics.
The context:
The project is set in the context of advancing the state-of-the-art of SAT (Boolean Satisfiability) and MaxSAT (Maximum Satisfiability) problem-solving by bridging the gap between symbolic and sub-symbolic AI. The significance of this advancement lies in its potential to handle problem instances with millions of variables and constraints which are currently beyond the scope of existing solvers.
The problem to address:
The specific challenge addressed by this project is solving large-scale combinatorial problems by integrating machine learning techniques into the realm of SAT/MaxSAT solving. Additionally, there is the challenge of defining suitable encodings for practical scheduling and planning problems in the domain of assistive robotics, and solving them with the resulting solvers.
Objectives:
- To investigate the potential of integrating machine learning techniques with traditional SAT and MaxSAT algorithms to solve large-scale combinatorial problems.
- To develop solvers and encodings showcasing the effectiveness of these integrated approaches across various AI scenarios, with a particular emphasis on their applicability in assistive robotics.
Expected Outcomes:
- A detailed analysis of the enhanced capabilities of SAT and MaxSAT solvers when augmented with machine learning techniques. This analysis will include a comparison with the performance of traditional solvers.
- Present innovative solutions or prototypes employing this integrated approach in practical AI applications, particularly showcasing their utility in assistive robotics
