# Integer programming to MAX-SAT translation

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  and Integer programming is NP-complete . 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.