Improving Satisfiability Solving in Python

Primary supervisor

Alexey Ignatiev

Propositional satisfiability (SAT) is a well-known example of NP-complete problems. Although NP-completeness may be perceived as a drawback, it allows one to solve all the other problems in NP by reducing them to SAT and relying on the power of modern SAT solvers. This is confirmed by a wealth of successful examples of use cases for modern SAT solving, including generalisations and extensions of SAT as well as a wide variety of practical applications in artificial intelligence (AI). This project will develop various ways to improve PySAT,  a critical Python Package Index (PyPI) package used for effective prototyping and problem solving with SAT, and augment PySAT with additional functionality.

Student cohort

Single Semester
Double Semester

Aim/outline

This project will explore and develop a range of ways of improving PySAT and augmenting it with additional functionality, including preprocessing techniques, solvers as well as cardinality and pseudo-Boolean encodings.

Required knowledge

Students applying for this project should have excellent programming skills (as evidenced, for example, by high marks in FIT2004). They should also demonstrate good understanding of the computability theory and intractability (FIT2014). In addition, it would be desirable for them to have done the "Programming languages and paradigms" unit (FIT2102) or, if a masters student, the "Modelling discrete optimisation" and "Solving discrete optimisation problems" units (FIT5216 and FIT5220).