A Core-Guided MaxSAT solver

CGSS is an effective implementation of the OLL algorithm for MaxSAT. The first version of CGSS was built on top of the RC2 MaxSAT solver in Python. The current–and much more effective–version is a reimplementation from scratch in C++. Most notably, CGSS extends RC2 with the so called structure sharing (SS) technique that results in more compact encodings of the constraints required for optimization. More details can be found in (Ihalainen et al., 2021).

CGSS is developed by my PhD student Hannes Ihalainen who wrote his M.Sc. thesis on it. The implementation is available in open source on bitbucket. The first (Python) version of CGSS was further extended with proof logging in 2023 by Andy Oertel. The source code of the proof-logging version can be found on gitlab