In the XCSP3 2023 competition for constraint solvers, Dr. Martin Lester’s solver Exchequer won 1st place in the Mini CSP track and 2nd place in the Mini COP track:https://www.xcsp.org/competitions/Constraint solvers take descriptions of problems in a standardised format as input and use general-purpose techniques to find solutions. They can be applied to a wide range of real-world problems in operations research, as well as combinatorial problems in mathematics and puzzle games.Exchequer works by translating the constraint problem into a C program and using a program model checker to turn that into a Boolean Satisfiability (SAT) instance, which it solves using a SAT solver. You can find Exchequer and some information about how it works here:https://gitlab.act.reading.ac.uk/ta918887/exchequerThe Mini tracks of the XCSP3 competition are mainly for less established solvers that demonstrate a new or experimental technique. Exchequer entered the XCSP3 competition for the first time in 2022, when it won 1st place in the Mini CSP track. This year was the first time it entered the Mini COP track.Dr. Lester has a short paper about the underlying techniques used in the solver at the ModRef 2022 workshop:https://modref.github.io/ModRef2022.htmlhttps://scholar.google.com/citations?view_op=view_citation&citation_for_view=Prq6EukAAAAJ:qjMakFHDy7sC
Many Congratulations to Dr. Martin Lester!!