Boolean Constraint Propagator
PSPD UnB-\(\gamma\)

1. O início de uma história
- 1.1. Forma Normal Conjuntiva
- 1.2. Iniciando o trabalho
2. O arquivo de entrada
- 2.1. Fórmula na CNF
- 2.2. Perguntas
3. Verificador
4. TODO BCP
5. Duplas definidas pelo Parieitor

1 O início de uma história

O problema mais incrível da computação é o da Satisfatibilidade Booleana, ou SAT para os íntimos, onde temos que decidir uma valoração para um conjunto de variáveis Booleanas que torne uma fórmula verdadeira.

A fórmula que estamos tratando possui somente conectivos lógicos \(\land\) (e, conjunção) e \(\lor\) (ou, disjunção), e literais de variáveis proposicionais.

As variáveis proposicionais são denotadas por letras do alfabeto em minúsculas como \(p,q,r\) ou por apenas um conjunto \(x_1, ..., x_n\). Estas variáveis podem receber os valores verdade verdadeiro (também V, ou \(1\)) ou falso (também, F ou \(0\)). Os literais são a variável ou sua negação, denotada por um \(\lnot\) , por exemplo \(\lnot x_1\).

A maneira mais comum de tratar este problema é se utilizando uma fórmula na Forma Normal Conjuntiva,FNC ou CNF [do inglês]. Neste caso a fórmula é composta por diversas cláusulas unidas por conjunções.

Uma cláusula \(c\) é a disjunção de literais. Uma fórmula \(\phi\) é a conjunção de cláusulas. Uma cláusula é dita satisfeita quando pelo meno um de seus literais assumem o valor V e não-satisfeita quando todos os seus literais assumem o valor F.

Cláusula unitária é uma cláusula representada por apenas um literal.

Literal puro é o literal que aparece em apenas uma forma em toda a fórmula, ou seja, uma variável \(x\) aparece apenas na forma \(x\) ou \(\lnot x\) na fórmula.

O problema de satisfatibilidade consistem em decidir se existe uma valoração que torna a fórmula verdadeira, ou seja, uma atribuição de valores verdade para as variáveis da fórmula que tornem todas cláusulas satisfeitas e, portanto, a fórmula satisfeita.

1.1 Forma Normal Conjuntiva

A Forma Normal Conjuntiva (Conjuctive Normal Form - CNF) é a classe de fórmulas da lógica proposicional que utiliza apenas os operadores lógicos de conjunção (\(\land\)), disjunção (\(\lor\)) e negação (\(\lnot\)), sendo este último aplicável apenas sobre as variáveis proposicionais.

A sua representação é um Grafo Direcionado Acíclido (DAG) de altura \(2\), onde a raiz é o operador de conjunção (\(\land\)), o primeiro nível são os operadores de disjunção (\(\lor\)) e o segundo nível as folhas, compostas por literais.

A fórmula abaixo pode ser representada pelo DAG na Figura 1:

\begin{equation} \label{org58ef8fd} (x_1 \lor x_2 ) \land ( x_1 \lor \lnot x_2 ) \land ( \lnot x_1 \lor \lnot x_2) \end{equation}

Figure 1: Diagrama de uma fóruma CNF

1.2 Iniciando o trabalho

O nosso trabalho consistirá no desenvolvimento de um Propagador de valores Booleanos, não se assuste! Vamos desenvolver em diversas etapas.

A primeira etapa de desenvolvimento é o Verificador de Valoração, ou seja, vamos receber uma valoração completa para as variáveis de uma fórmula e devemos verificar se a valoração satisfaz a fórmula.

Neste vídeo fiz uma conversa com os alunos da disciplina, onde apresento o início do trabalho.

Nas próximas seções as etapas serão discutidas cuidadosamente.

2 O arquivo de entrada

A entrada é composta por duas partes. A primeira é relacionada à fórmula, e; a segunda é relaciada às perguntas que devem ser respondidas.

O formato das perguntas será diferente de acordo com o entregável do momento, no entanto, o formato da fórmula permanecerá sempre o mesmo.

O arquivo de entrada será passado sempre pela entrada padrão e todas as suas respostas devem ser colocadas na saída padrão. AKA stdin e stdout.

2.1 Fórmula na CNF

A entrada da fórmula é composta por diversas linhas. A primeira linha é composta com por dois números inteiros \(V\) e \(C\) representando, respectivamente, o número de variáveis na fórmula e o número de cláusulas.

Você deve esperar que \(V > 1\) e que \(C > 0\), já o limite superior é pouco conhecido, uma estimativa para o trabalho é que \(V <= 2^{20}\) e \(C <= 2^{27}\).

As variáveis são indexadas pelo intervalo, fechado, inteiro \([1,V]\). Os literais aparecem na forma da variável (o número positivo) e o literal negado é representado pelo número negativo.

Após a primeira linha existem \(C\) linhas, cada uma contendo uma cláusula. Cada cláusula é composta por um conjunto de literais de variáveis da fórmula. Não acontecem literais repetidos, e nem tautologias (aparendo o literal positivo e negativo da mesma variável proposicional). A linha termina com \(0\), indicando o fim da cláusula. \(0\) não é uma variável proposicional.

Exemplo de entrada, que representa o exemplo \eqref{org58ef8fd}:

Nada garante que os literais aparecerão numericamente ordenados nas cláusulas

2.2 Perguntas

As perguntas que serão feitas ao seu programa seguirão feitos pela entrada padrão e possuirão diversas linhas. O formato dependerá do tipo de teste a ser realizado.

Nas seções seguintes trataremos dos casos de entrada.

3 Verificador

O primeiro programa que esperamos que seja desenvolvido é o verificador de valoração.

O verificador de valoração recebe uma fórmula na CNF (veja a seção 2.1) e depois receberá um conjunto de valoração a ser verificada.

O conjunto de valoração não será, necessariamente, fornecido antecipadamente, ou seja, é possível que a próxima valoração seja gerada apenas após a verificação da anterior. Deixando, portanto, o verificador como um programa interativo com o corretor.

3.1 Para que serve o verificador?

A ideia do verificador é ser o auxiliar do algoritmo WalkSAT, um resolvedor SAT de busca local.

Este algoritmo gera uma valoração aleatória para as variáveis proposicionais e caso ela não satisfaça a fórmula, ele procura inverter a valoração de algumas variáveis, e tenta isso algumas vezes.

Os algoritmos GSAT e WalkSAT não são completos, isto é, não conseguem afirmar que a fórmula é UNSAT (quando não há uma valoração que satisfaça a fórmula) pois ele não testa todas as possibilidades.

Como o WalkSAT gera diversas tentativas, é importante que o verificador seja rápido, para evitar muita espera na tarefa de identificar quais cláusulas ficaram falsas.

3.2 Entrada e Saída

3.2.1 Entrada

A entrada é composta primeiramente pela fórmula em CNF e depois haverão um conjunto de linhas, onde cada linha possui a valoração de cada variável em sua forma verdadeira, ou seja havendo o numeral \(1\) siginifica que a variável proposicional \(1\) é verdadeira, já \(-2\) significa que a variável proposicional \(2\) é falsa, e a sua negação que é verdadeira.

A valoração é composta por dois tipos de linhas, as linhas full e as linhas flip.

As linhas do tipo full possuem a string full no início e seguem com \(V\) numerais ordenados pela sua forma absoluta, (ex: -1 -2 3 4 -5 6 7 -8). Cada numeral representa o literal valorado como Verdadeiro.

As linhas do tipo flip modificam somente uma variável proposicional, ou seja, se a variável for verdadeira a sua negação passa a ser verdadeira. Esta possui a string flip seguida do indexado da variável que deve ter sua valoração trocada (sempre será um número positivo).

Exemplo de entrada:

2 3
1 2 0
1 -2 0
-1 -2 0
full -1 -2
flip 2
flip 1
flip 2

No exemplo acima iniciamos com a valoração: -1 -2

A seguir acontece um flip em 2, ficando a valoração: -1 2

Depois acontece um flip em 1, ficando: 1 2

E por fim mais um flip em 2, finalizando a entrada com a valoração: 1 -2

3.2.2 Saída

A saída é composta por diversas linhas podendo ser:

SAT, quando a fórmula é satisfeita, ou seja, todas cláusulas foram satisfeitas.
lista das cláusulas que não foram satisfeitas, a primeira cláusula possui indexador \(0\). Segundo o formato: [K clausulas falsas] seguido dos identificadores de cada clásula. Onde \(K\) é a quantidade de clásulas falsas.
- As cláusulas devem ser apresentadas em ordem crescente (primeiro a de menor índice e a última a de maior índice)
lista de literais falsos, sem repetição e ordenados por quantidade de vezes que aparecem nas cláusulas, das cláusulas não satisfeitas seguindo o formato [lits] seguido dos identificadores dos literais que estão falsos.
- (Sat, 13 Mar 2021 12:35:40 -0300) Os literais devem estar ordenados do que ocorre mais vezes para o que ocorre menos vezes
- O desempate dos literais com a mesma contagem deve ser feito preferindo a variável de maior grandeza, ou seja, havendo empate entre o literal \(-2\) com 1 ocorrência e \(1\) com uma ocorrência, considere \(-2\) como maior. Use o valor absoluto do literal.

Exemplo de saída para o exemplo acima:

[1 clausulas falsas] 0
[lits] 2 1
[1 clausulas falsas] 1
[lits] -2 1
[1 clausulas falsas] 2
[lits] -2 -1
SAT

3.3 Executando os testes

Para efetuar os testes você pode rodar um comando parecido com:

time ./meuverificador < arquivo.in

Da maneira acima você irá executar o seu verificador e irá identificar em quanto tempo o seu programa executa.

Compile o seu programa utilizando no mínimo as flags abaixo:

-O2 -static

Se a sua implementação utiliza a math.h, passe -lm, e quando for utilizar threads, passe -lpthread. Se for utilizar OpenMP não esqueça que o parâmetro é -fopenmp.

3.4 Arquivos de exemplo

Alguns arquivos de exemplo são fornecidos, tanto o arquivo de entrada quanto a saída esperada (gabarito), esses são conjuntos pequenos e podem ser baixados pelo github

O repositório é: https://github.com/bcribas/pspd-2020.2
Leia o arquivo README.org dentro do pacote para explicações de como utilizá-lo.

3.4.1 Mais arquivos de exemplo

Em tese você pode utilizar qualquer fórmula do padrão DIMACS, em CNF, para gerar os arquivos de entrada e o gabarito com o gerador.

Você pode baixar mais exemplo pelo site abaixo:

https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

3.5 Entregas e Prazo

3.5.1 O que devo refletir?

Quanto tempo a sua implementação demora para os casos fornecidos
Como é feita a otimização para paralelizar o algoritmo?
- Como o desempenho é alterado rodando o programa com \(2\), \(4\), \(6\), \(8\) e \(12\) threads?
- O desempenho é modificado quando o arquivo de saída é redirecionado para /dev/null?
  - E quando a impressão é comentada?
  - Qual o impacto da leitura do arquivo de entrada no tempo global?
A partir de qual tamanho de fórmula a paralelização faz diferença?

3.5.2 Entregando

Gere um relatório simples contendo gráficos de desempenho para as diversas execuções
- Coloque a comparação da sua solução com a implementação sequencial fornecida;
Avalie o gargalo do seu algoritmo
- O maior problema acontece nas estruturas de controle (ex:semáforos)?
- O tempo de leitura da entrada é perceptível?
- Isole o tempo de execução da função que avalia a verificação (descontando o tempo de leitura da fórmula e de cada valoração full e flips)
Qual é a complexidade do seu verificador?
- O seu algoritmo aproveita resultados parciais para avaliar flips mais rapidamente?

Esta é uma somativa de Peso 2

3.5.3 Prazo

O prazo para este item (verificador) é ~~31 de março de 2021~~, 05 de maio de 2021
Esta atividade conta como uma atividade somativa e deve ser feita de acordo com a separação de duplas marcadas pelo parieitor
Notas da conversa do dia 14 de abril

4 TODO BCP

Em construção…

5 Duplas definidas pelo Parieitor

Nome1	Nome2
Adrianne Alves da Silva	Matheus Roberto Alves da Silva
Alexandre Miguel Rodrigues Nunes Pereira	Romulo Vinicius de Souza
Daniel Maike Mendes Goncalves	Jôberth Rogers Tavares Costa
Djorkaeff Alexandre Vilela Pereira	Gabriela Barrozo Guedes
Eduardo Vieira Lima	Samuel de Souza Buters Pereira
Eugenio Sales Siqueira	Lucas Maciel Aguiar
Gabriel Marques Tiveron	Luis Henrique Pereira Taira
Gustavo Marques Lima	Ivan Diniz Dobbin
Joao Gabriel Rossi de Borba	João Matheus de Sousa Rodrigues
Joao Vitor Morandi Lemos	Jose Aquiles Guedes de Rezende
Lucas Alexandre Fernandes Martins	Matheus de Cristo Doreia Estanislau
Marcelo Araujo dos Santos	Renan Cristyan Araujo Pinheiro
Victor Hugo Dias Coelho	sozinho
Vitor Meireles Oliveira	nao marcou (sozinho*)

Boolean Constraint Propagator PSPD UnB-\(\gamma\)

Table of Contents