[Proof Complexity] MIAO seminar Tue Dec 3 at 14:00 CET with George Katsirelos: Relating implicit hitting set and core-guided MaxSAT solvers via linear programming

[Jakob Nordström]

Dear all,

On Tuesday December 3 at 14:00 CET we will have the opportunity to 
listen to the MIAO seminar "Relating implicit hitting set and 
core-guided MaxSAT solvers via linear programming" given by George 
Katsirelos from INRAE. You find the abstract at the bottom of this message.

We will run this as a hybrid seminar at the University of Copenhagen. 
Local participants are warmly welcome to auditorium Store UP1 at 
Universitetsparken 3, while other participants are equally warmly 
welcome to join virtually at https://lu-se.zoom.us/j/61925271827 . 
Please feel free to share this information with colleagues who you think 
might be interested. We are also hoping to record the seminar and post 
on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch 
for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular 
talk, and then after a break a ca-1-hour in-depth technical presentation 
with (hopefully) a lot of interaction. The intention is that the first 
part of the seminar will give all listeners a self-contained overview of 
some exciting research results, and after the break people who have the 
time and interest will get an opportunity to really get into the 
technical details. (However, for those who feel that the first part was 
enough, it is perfectly fine to just discretely drop out during the 
break. No questions asked; no excuses needed.)

More information about the MIAO seminar series can be found at 
https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive 
these announcements, or receive several copies of them, please send a 
message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Tuesday Dec 3 at 14:00 in auditorium Store UP1, Universitetsparken 3, 
University of Copenhagen, and on Zoom
*Relating implicit hitting set and core-guided MaxSAT solvers via linear 
programming
*(George Katsirelos, INRAE)
/
Many current complete MaxSAT algorithms fall into two categories: 
core-guided or implicit hitting set. The two kinds of algorithms seem to 
have complementary strengths in practice, so that each kind of solver is 
better able to handle different families of instances. This suggests 
that a hybrid might match and outperform either, but the techniques used 
seem incompatible. In this talk, I will focus on PMRES and OLL, two 
core-guided algorithms based on max resolution and soft cardinality 
constraints, respectively. I will show that these algorithms implicitly 
discover cores of the original formula. Moreover, in some cases they 
compute the optimum hitting set of these cores at each iteration. More 
importantly, I will also give compact integer linear programs for each 
which encode this hitting set problem, and whose continuous relaxation 
has an optimum that matches the bound computed by the respective 
algorithms. This allows the design of hybrid algorithms, with components 
from implicit hitting set, core-guided, and beyond, with linear programs 
as the shared representation between the various components.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se