[dvdkhlng]

I already have problems following Proposition 1 where they introduce a different DNF with twice the clauses of the original CNF than claim that maximizing the satisfied clauses in the DNF would also yield a maximum satisfied solution for the CNF.

It's a pitty they don't release any source code that we can unit-test against problems with known solutions (while also profiling run-time to stay within polynomial bounds) :)

edit: what am I missing, their reduction to a DNF seems unsuitable to me?

I read proposition 1 [1] to mean: they find an optimal solution for the DNF V∪X, then expect the corresponding CNF C to have at least as many satisfied clauses. However isn't that insufficient? I mean there could be an even better solution with more satisfied clauses in C, that are totally missing when only looking for solutions for V∪X. But maybe I'm just misunderstanding something.

[1] https://arxiv.org/pdf/2304.12517.pdf

[pfedak]

The conversion to DNF is fine. The original clauses map directly to pairs of new clauses, so fixing an assignment to the original variables V you can always satisfy the same number of the DNF clauses. You can do worse by choosing the wrong values for X, sure, but there's always a straightforward correspondence.