Paper Accepted at CP 2024

I am happy to report that our paper, Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability, has been accepted for publication in the 30th International Conference on Principles and Practice of Constraint Programming. In the paper, we present an approach for proof-logging the solution-improving search (SIS) to MaxSAT that uses the dynamic polynomial watchdog (DPW) encoding.

Proof logging refers to producing a formal proof of correctness that can be independently verified, thus allowing for complete trust in the results outputted by a MaxSAT solver without assuming it is correctly implemented. Proof logging the SIS algorithm with the DPW was surprisingly intricate, requiring several without loss of generality type reasoning.

I want to thank all of my co-authors for their excellent work on the project!