At the 27th International Conference on Theory and Applications of Satisfiability Testing (SAT) in India, WASP PhD student Andy Oertel and Mathematical Insights into Algorithms for Optimization (MIAO) group from Lund University received significant recognition for their proof checker VeriPB and the pseudo-Boolean solver RoundingSat.
For the second consecutive year, VeriPB was used as an official proof checker in the SAT competition, securing a silver medal when integrated with an existing SAT solver. VeriPB ensures the correctness of proofs generated by the software and when combined with CakePB it provides formal correctness guarantees about the software’s output.
Andy Oertel’s research focuses on certification for combinatorial optimization, which is applied in various fields such as scheduling, logistics, vehicle routing, and supply chain management. Certification, or proof logging, ensures that the software not only provides a solution but also generates a proof certifying the solution’s correctness.
RoundingSAT – best solver for decision and optimization
MIAO group’s open-source solver RoundingSat serves as research software to explore new solving approaches for combinatorial optimization. In the Pseudo-Boolean Competition, 9 of the 12 best solvers were based on RoundingSAT’s code base.
“The primary difference between RoundingSat and other solvers lies in the conflict analysis part of the solving routine. Conflict analysis involves learning new constraints implied by existing ones. RoundingSat employs the division rule for conflict analysis, setting it apart from other solvers,” says Andy.
Best paper was analysis of VeriPB
This year’s SAT best paper was a theoretical analysis of the proof system developed for VeriPB, while the best student paper explored improvements to RoundingSat.
The achievements of Andy Oertel and the MIAO group at the conference highlight the importance and impact of their research in the fields of satisfiability testing and combinatorial optimization.
Published: November 11th, 2024