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.