Codificando o conjunto de restrições At-Most-One como um problema MAX-SAT

Question

Suponha um conjunto de variáveis $V$ = $\{v_1,...,v_m\}$.

Dado total $n$ restrições de no máximo um (AMO) (no máximo um elemento em um determinado conjunto é verdadeiro) set [do formulário abaixo], sobre a variável set $V$,

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

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

Não consigo representá-lo como um problema MAX-SAT.

Tentei até agora (tentativa 1):Usando restrição rígida para cada restrição At-Most-One.Isso não funcionará como codificação de $AMO(v_i,...,v_w)$ terá múltiplas cláusulas para cada $AMO$ e todos eles atribuíram o mesmo peso (peso superior).Uma solução para este conjunto pode não ser a máxima.

Tentativa (2):Para corrigir o problema acima, tentei o peso relativo da cláusula;ou seja, para cada cláusula atribua um peso proporcional ao tamanho da cláusula.Isso dará preferência à atribuição de cláusulas mais curtas e satisfatórias.Mas isso não funciona em situações extremas, como se todas as cláusulas tivessem o mesmo comprimento.

Tenho experiência com solucionadores SAT, mas esta é minha primeira tentativa de problema MAX-SAT.

Answer 1

A maneira padrão de criar restrições flexíveis no MaxSAT é usar variáveis ​​de rótulo:

Para cada $AMO_j$ restrição, crie uma nova variável $l_j$.Em seguida, crie uma cláusula unitária $(\lnot l_j)$ com peso $1$ e adicione o literal $l_j$ para cada cláusula da norma $AMO_j$ codificação que contém apenas cláusulas rígidas (peso infinito).

Agora a variável rótulo $l_j$ funciona como um interruptor:contexto $l_j = verdadeiro$ irá "desligar" o $AMO_j$ restrição rígida, mas não satisfaz a cláusula unitária $(\lnot l_j)$.