O problema de satisfação máxima (Max-Sat) é o problema de encontrar o número máximo de cláusulas que podem ser satisfeitas em uma instância de satisfação booleana. O problema exatamente 1 em 2 Sat pergunta, dado um conjunto de cláusulas, cada uma com dois literais, existe um conjunto de literais, de modo que cada cláusula tenha exatamente um literal desse conjunto.
A complexidade de fazer escolhas únicas: Aproximando 1-em-k SAT por Guruswami e Trevisan fornece um método para aproximar Max 1 em 2 Sat. Eles afirmam que monótonos (sem literais negados) Max 1 em 2 Sat "admite uma aproximação eletrônica no tempo polinomial".
Gostaria de encontrar um algoritmo exato para o problema Max monotone 1 em 2 Sat.
graph-algorithms
sat
max2sat
Russell Easterly
fonte
fonte
Respostas:
Uma cláusula monótona 1 em 2 exige que as duas variáveis tenham valores diferentes. Assim, você pode modelar o problema como um problema gráfico, com um vértice por variável que será colorido em preto ou branco e uma aresta para uma cláusula indicando que as cores precisam ser diferentes. Portanto, a questão é tornar o gráfico bipartido excluindo um número mínimo de arestas. Esse é o problema MaxCut ou Edge Bipartization. É NP-difícil.
Para a bipartização de arestas, existe um algoritmo que é executado rapidamente quando poucas arestas precisam ser excluídas. Eu escrevi uma implementação para um problema um pouco mais geral descrito aqui ( código fonte ).
fonte
Um algoritmo exato para o problema Max Monotone 1 em 2 Sat (ou seja, MaxCut) executando mais rápido que (aproximadamente tempo) pode ser encontrado no capítulo 6 da minha tese de doutorado, aqui: http: // web.stanford.edu/~rrwill/thesis.pdf O ( 1,8 n )2n O(1.8n)
Não conheço outro algoritmo exato para o problema que melhora a pesquisa exaustiva em todas as instâncias. Para instâncias esparsas (com cláusulas ), Greg Sorkin e seus co-autores têm vários resultados algorítmicos. Veja aqui: https://sites.google.com/site/gregorysorkin/pubxO(n)
fonte