Encoding set of At-Most-One constraints as a MAX-SAT problem

Question

Assume a set of variable $V$ = $\{v_1,...,v_m\}$.

Given total $n$ at-most-one (AMO) constraints (at most one element in a given set is true) set [of the below form], over the variable set $V$,

$$ AMO \, (v_1, v4, \neg v_6, v_{10}) \\ ... \\ AMO \, (v_2, \neg v3, v_7)$$

Problem: Find an assignment to $V$ that maximize
         the number of satisfiable AMO constraint set. 

I'm unable to represent it as MAX-SAT problem.

Tried so far (Attempt 1): Using hard constraint for each of At-Most-One constraint. This will not work as encoding of $AMO (v_i,...,v_w)$ will have multiple clauses for each $AMO$ and all of them have assigned same weight (top weight). A solution to this set may not be the maximal one.

Attempt (2): To fix the above problem, I tried relative clause weight; i.e., for each clause assign weight proportional to size of the clause. This will give preference of assigning satisfying shorter clause. But this do not work in extreme situations like if all clause have same length.

I have experience with SAT solvers but this is my first MAX-SAT problem attempt.

Answer 1

The standard way to create soft constraints in MaxSAT is to use label variables:

For each $AMO_j$ constraint, create a new variable $l_j$. Then create an unit clause $(\lnot l_j)$ with weight $1$ and add the literal $l_j$ to every clause of the standard $AMO_j$ encoding that contains only hard (infinite weight) clauses.

Now the label variable $l_j$ acts as a switch: setting $l_j = true$ will "turn off" the $AMO_j$ hard constraint, but does not satisfy the unit clause $(\lnot l_j)$.