Integer programming to MAX-SAT translation

Question

Reading A Comparison of Methods for Solving MAX-SAT Problems, I can see that a MAX-SAT problem can be translated to an integer programming (IP) problem.

Definition of MAX-SAT [Wikipedia]:

The maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula.

Definition of integer programming [Wikipedia]:

An integer programming problem is a mathematical optimization or feasibility program in which some or all of the variables are restricted to be integers

Is there a similar translation backwards? Given an IP problem that can be translated to a MAX-SAT.

The MAX-SAT problem is NP-hard [2] and Integer programming is NP-complete [3]. technically it might not be very suitable to solve a (in principle) simpler problem using a formulation which is (in principle) harder to solve. But it will be great to understand the encoding both ways. My motivation is to compare MAX-SAT solvers with IP solvers.

More precisely given an IP problem like: $$x_1 + x_{2} + \neg x_3 \leq 1 \\ \neg x_1 + x_4 + x_3 \leq 1 \\ ... $$

with total n inequalities/equations and each $x_i \in \mathbb{B}$. Such that maximize as many as equations (from total n). Encode it as a MAX-SAT problem.

First Attempt: Each inequality encodes AtMostOne of the complement of the variables (or AtleastN-1 of the original IP inequality). But representing AtMostOne in CNF will create multiple clauses and destroys the possible use of direct MAX-SAT.

Answer 1

The decision versions of both MaxSAT and integer programming are in fact NP-complete, so there is polynomial reduction from integer programming to MaxSAT.

In the context of solvers, modern MaxSAT solvers support "weighted partial MaxSAT"-encodings (weighted clauses with possibly infinite weights), so you can add any SAT encoded hard constraints by encoding them as clauses with infinite weight.

For comparing MaxSAT and IP solvers, I would strongly suggest looking at modern literature on "implicit hitting set" algorithms for MaxSAT. The solvers using this algorithm use both IP solvers and SAT solvers as subroutines for solving MaxSAT. It might even be that if you use some direct translation from IP to MaxSAT and give the resulting instance for these solvers, the solver will under the hood just directly solve the original IP instance with the IP solver. Also, there is a lot of recent research comparing IP and MaxSAT solvers for solving specific problems (just search "integer programming maxsat" in Google Scholar).