SAIPS

The Propositional Satisfiability problem (SAT) is a fundamental formalism in constraint programming that is used to model and solve a wide variety of academic and industrial decision problems. While modern SAT solvers have achieved the ability to address instances featuring millions of variables and clauses within reasonable time frames, they can still fail drastically on specific instances. The mission of the SAIPS chair is  to develop innovative AI-driven problem-solving methodologies by integrating symbolic AI and machine learning to create scalable and robust solutions. The focus is on enhancing Satisfiability and Maximum Satisfiability (MaxSAT) solvers, improving their scalability, robustness, and adaptability through novel algorithmic techniques and machine learning-driven heuristics. A key goal is to analyze solver behavior, optimize proof generation, and enhance explainability using graph-based ML models. Additionally, the project applies these advances to complex scheduling problems, including university timetabling and energy-aware assembly line balancing. By combining solver innovations with practical applications, the research aims to demonstrate the real-world impact of advanced SAT and MaxSAT techniques.