MAC0323 - Algoritmos e Estruturas de Dados II (2021i)

Introdução.  Neste exercício, você resolverá o Creative Problem 4.2.34, 2-Satisfiability, de S&W.

Satisfatibilidade.  Seja $\phi$ uma fórmula booleana, com variáveis $x_1,\dots,x_N$. Dizemos que $\phi$ é satisfatível se existe uma atribuição de valores-verdade ("true" ou "false" ou $1$ ou $0$) às variáveis $x_i$ de forma que $\phi$ torna-se verdadeira com esses valores.

Problema SAT. Dada uma fórmula booleana, decidir se ela é satisfatível.

O SAT é um problema de natureza fundamental em computação: ele é um problema NP-completo. Assim, acredita-se que não há algoritmo polinomial para SAT, e sabe-se que todo problema NP admite um algoritmo polinomial caso SAT admita tal algoritmo. Você estudará essas coisas (em geral, brevemente) em MAC0338, Análise de Algoritmos, e caso você queira estudar essas coisas mais a fundo, faça MAC0414, Autômatos, Computabilidade e Complexidade, ou MAC0430, Algoritmos e Complexidade de Computação.

Mesmo restringindo a entrada a certas fórmulas de formato especial, o Problema SAT continua difícil (NP-completo). Seja $k$ um inteiro positivo. Dizemos que uma fórmula booleana $\phi$ é uma fórmula $k$SAT se $\phi$ é uma conjunção de disjunções, onde cada disjunção tem exatamente $k$ literais (um literal é uma variável ou sua negação). As disjunções em $\phi$ são chamadas de cláusulas. Assim, $\phi$ é uma fórmula $k$SAT se $\phi$ é um "e" de cláusulas, com cada cláusula contendo $k$ variáveis (ou suas negações). Por exemplo, eis um $3$SAT:

\(\phi=(x_1\vee x_2\vee\neg x_3)\wedge(x_2\vee x_3\vee\neg x_4) \wedge(x_3\vee x_4\vee x_1)\wedge(x_4\vee\neg x_1\vee x_2) \wedge(\neg x_1\vee\neg x_2\vee x_3)\wedge(\neg x_2\vee\neg x_3\vee x_4) \wedge(\neg x_3\vee\neg x_4\vee\neg x_1)\wedge(\neg x_4\vee x_1\vee\neg x_2).\)

 A $\phi$ acima é constituída de $8$ cláusulas.

Problema $k$SAT. Dada uma fórmula booleana $k$SAT, decidir se ela é satisfatível.

O Problema $k$SAT para $k=3$ é também NP-completo. Entretanto, o $2$SAT admite algoritmo polinomial; de fato, $2$SAT admite um algoritmo linear. Neste exercício, você encontrará e implementará tal algoritmo.

Grafos de implicação.  Sabemos que $a\vee b$ é equivalente a ambos $\neg a\Rightarrow b$ e $\neg b\Rightarrow a$. Assim, um $2$SAT pode ser representado como um grafo dirigido, como vimos no Exercício T05. Aliás, você deve fazer o T05 antes de fazer este exercício.

O programa ImplicationGraph.java fornecido abaixo cria o grafo de implicações de um $2$SAT dado.

Sua tarefa.  Neste exercício, você deve escrever o programa TwoSAT.java, que implementa a seguinte API:

public class TwoSAT
-------------------------------------------------------------------------------------
              TwoSAT(ImplicationGraph impgr) ... resolve o 2SAT codificado em imprgr
      boolean hasSolution()                  ... true se e só se satisfatível
    boolean[] assignment()                   ... o satisfying assignment
       String unSATProof()                   ... certificado de não satisfatibilidade

O construtor TwoSAT() deve ter complexidade $O(N + M)$ quando o $2$SAT codificado em impgr tem $N$ variáveis e $M$ cláusulas. O método hasSolution() deve ter complexidade constante, enquanto que assignment() deve ter complexidade $O(N)$. De fato, as "respostas" para as chamadas de hasSolution() e assignment() devem ser computadas quando o construtor TwoSAT() for chamado; hasSolution() e assignment() devem apenas devolver os valores computados.

Quando o $2$SAT fornecido não é satisfatível, unSATProof() deve devolver um certificado para esse fato. Isto é discutido mais abaixo. O método unSATProof() deve ter complexidade $O(L)$, onde $L$ é o comprimento do certificado. Este certificado deve ser computado quando o construtor for chamado.

O programa TwoSATClient.java ilustra o uso de TwoSAT.java. Exemplos de execução de TwoSATClient.java seguem abaixo.

$2$SAT aleatórios.  Para verificar seus programas, você pode achar conveniente usar o gerador de instâncias InstanceGenerator.java. Este programa recebe $N$, $M$ e $\mathit{seed}$ e produz um $2$SAT aleatório com $N$ variáveis e $M$ cláusulas, usando $\mathit{seed}$ como a semente de StdRandom.java.

Execuções de TwoSATClient.java.  Considere as seguintes duas execuções:

$ java-algs4 InstanceGenerator 4 13 3232021 | java-algs4 TwoSATClient
Satisfying assignment:
1: true
2: false
3: true
4: false
Assignment: true false true false
4 variables
26 implications
1 [true]: 3 [true] -2 [true] 1 [true]
-1 [false]: 4 [false] -3 [false] -2 [true] -1 [false]
2 [false]: -3 [false] -1 [false] 1 [true]
-2 [true]: -4 [true] 3 [true]
3 [true]: -4 [true] 3 [true] -2 [true] 1 [true]
-3 [false]: 4 [false] -3 [false] 2 [false] -1 [false]
4 [false]: 4 [false] -3 [false] 2 [false]
-4 [true]: -4 [true] 3 [true] 1 [true]
Truth value of 2SAT: true
$ java-algs4 InstanceGenerator 4 14 3232021 | java-algs4 TwoSATClient
Not satisfiable:

1 => -2 => -1
-1 => 4 => 2 => 1

Check the graph:

4 variables
28 implications
1: 3 -2 2 1
-1: 4 -3 -2 -1
2: -3 -1 1
-2: -4 3 -1
3: -4 3 -2 1
-3: 4 -3 2 -1
4: 4 -3 2
-4: -4 3 1
$

No primeiro caso, InstanceGenerator.java gerou uma instância satisfatível, e TwoSATClient.java encontrou uma solução. No segundo caso, a instância gerada (que contém apenas uma cláusula a mais que a instância anterior) não é satisfatível. TwoSATClient.java, não apenas disse que a instância não é satisfatível, mas também forneceu um certificado para essa afirmação: o grafo de implicações contém as implicações $x_1\Rightarrow\neg x_2\Rightarrow\neg x_1$ e $\neg x_1\Rightarrow x_4\Rightarrow x_2\Rightarrow x_1$ e portanto $x_1\Leftrightarrow\neg x_1$, que é uma contradição.

No caso de instâncias não satisfatíveis, o método unSATProof() de TwoSAT.java deve devolver dois caminhos dirigidos no grafo de implicações: um de uma variável $x_i$ para sua negação $\neg x_i$ e outro de $\neg x_i$ para $x_i$ (como no exemplo acima).

Limiar de $2$SAT.  Consideremos instâncias aleatórias de $2$SAT, como aquelas geradas por InstanceGenerator.java. Sabe-se que, quando o número de cláusulas $M$ supera sensivelmente $N$, o número de variáveis, os $2$SATs aleatórios são insatisfatíveis com probabilidade alta. Para estimar essas probabilidades, você pode usar o programa Estimate.java, que depende de TwoSAT.java.

Exemplos de execução

$ java-algs4 Estimate 1000 1000 10000 888
Simulation time: 10.633 seconds
Fraction satisfiable: 0.9335
$ java-algs4 Estimate 1000 1150 10000 888
Simulation time: 10.999 seconds
Fraction satisfiable: 0.498
$ java-algs4 Estimate 1000 1250 10000 888
Simulation time: 10.38 seconds
Fraction satisfiable: 0.1194
$ java-algs4 Estimate 1000 1300 10000 888
Simulation time: 10.693 seconds
Fraction satisfiable: 0.0392
$

Veja outros exemplos de execução de Estimate.java nos arquivos experiments*.txt.

Desempenho.  Exemplos de execução são dados nos arquivos experiments1.txt e experiments2.txt (mesmo conjunto de execuções em duas máquinas diferentes). Espera-se que seu programa tenha desempenho, grosso modo, similar.

Entrega.  Você deve entregar apenas o programa TwoSAT.java.