My paper “Unifying Reasoning and Core-Guided Search for Maximum Satisfiability” got accepted for publication at JELIA 2019. The paper reports on a theoretical investigation of the correctness MaxSAT solving techniques that can be seen as instance transformations. In fact, many approaches to MaxSAT solving transform a MaxSAT instance to be solved while preserving an optimal solution until the optimal solution is in some sense “trivial” to find (details in the paper).
We show that previously established theoretical notions for establishing the correctness of such methods are not general enough to capture all modern MaxSAT solving techniques, thus making the development of solvers that combine different methods difficult. We also propose a new type of instance transformation that covers all previously proposed notions that we are aware off. Finally we also generalize some known results from reasoning techniques from SAT solving to MaxSAT, thus bridging the gap between SAT solving and MaxSAT solving.
I am exited about this line of work, it feels like there is more to understand in this direction, hopefully I can extend this work in the near future.