Problema do Jantar Surpresa
Codificação diretamente como SAT
c --------------------------- c
c Problema do Jantar Surpresa c
c --------------------------- c
c  
c Simbolos Proposicionais
c   Schemas de fluentes
c      lixo(I)
c  	maos_limpas(I)
c  	silencio(I)
c  	jantar(I)
c  	presente(I)
c   Schemas de ações	
c 	cozinhar( I )
c 	embrulhar( I )
c 	carregar_lixo( I )
c 	triturar_lixo( I )
c
c  1 lixo( 1 )
c  2 maos_limpas( 1 )
c  3 silencio( 1 )
c  4 jantar( 1 )
c  5 presente( 1 )
c  6 lixo( 2 )
c  7 maos_limpas( 2 )
c  8 silencio( 2 )
c  9 jantar( 2 )
c 10 presente( 2 )
c 11 lixo( 3 )
c 12 maos_limpas( 3 )
c 13 silencio( 3 )
c 14 jantar( 3 )
c 15 presente( 3 )
c 16 lixo( 4 )
c 17 maos_limpas( 4 )
c 18 silencio( 4 )
c 19 jantar( 4 )
c 20 presente( 4 )
c 21 cozinhar( 1 )
c 22 embrulhar( 1 )
c 23 carregar_lixo( 1 )
c 24 triturar_lixo( 1 )
c 25 cozinhar( 2 )
c 26 embrulhar( 2 )
c 27 carregar_lixo( 2 )
c 28 triturar_lixo( 2 )
c 29 cozinhar( 3 )
c 30 embrulhar( 3 )
c 31 carregar_lixo( 3 )
c 32 triturar_lixo( 3 )
c       " c ... de comentário  " 
p cnf 32 143 
c  " p indica para o SAT-solver um problema como uma CNF, neste caso, 
c    contendo 32 símbolos proposicionais e 143 cláusulas"
c Estado Inicial: lixo(1) ^ maos_limpas(1) ^ silencio(1) ^ ~jantar(1) ^ ~presente(1)
c
1 0
2 0
3 0
-4 0
-5 0
c descrição do estado objetivo no instante 4, i.e., considerando um plano de 3 passos
c Estado Objetivo: ~lixo(4) ^ jantar(4) ^ presente(4)
c
-16 0
19 0
20 0
c
c Dominio:
c
c (:act cozinhar :prec (maos_limpas) :eff (jantar))
c (:act embrulhar :prec (silencio) :eff (presente))
c (:act carregar_lixo :prec (lixo) :eff (and (not (lixo)) (not (maos_limpas))))
c (:act triturar_lixo :prec (lixo) :eff (and (not (lixo)) (not (silencio))))
c
c Acoes implicam suas pre-condicoes:
c 	Axiomas de pre-condições schemas
c cozinhar( I ) -> maos_limpas( I )
c embrulhar( I ) -> silencio( I )
c carregar_lixo( I ) -> lixo( I )
c triturar_lixo( I ) -> lixo( I )
c
-21 2 0
-22 3 0
-23 1 0
-24 1 0
-25 7 0
-26 8 0
-27 6 0
-28 6 0
-29 12 0
-30 13 0
-31 11 0
-32 11 0
c
c Acoes implicam seus efeitos (axiomas de efeito):
c 	Schemas de Axiomas de efeitos
c cozinhar( I ) -> jantar( I + 1 )
c embrulhar( I ) -> presente( I + 1 )
c 	efeitos conjuntivos devem ser descritos por uma cláusula para cada efeito 
c carregar_lixo( I ) -> ~lixo( I + 1 )
c carregar_lixo( I ) -> ~maos_limpas( I + 1 )
c triturar_lixo( I ) -> ~lixo( I + 1 )
c triturar_lixo( I ) -> ~silencio( I + 1 )
c
-21 9 0
-22 10 0
-23 -6 0
-23 -7 0
-24 -6 0
-24 -8 0
-25 14 0
-26 15 0
-27 -11 0
-27 -12 0
-28 -11 0
-28 -13 0
-29 19 0
-30 20 0
-31 -16 0
-31 -17 0
-32 -16 0
-32 -18 0
ccccccccccccc  Axiomas de Quadro   cccccccccccccccccccc
c Acoes implicam fluentes que nao afetam (axiomas de quadro):
c	aqui aparecem sentenças do tipo:   A ^ B -> C  
c	que correspondem a cláusula: 	~A v ~B v C
c 	Schemas de Axiomas de frame
c [ lixo( I ) ^ cozinhar( I ) ] -> lixo( I + 1 )
c [ ~lixo( I ) ^ cozinhar( I ) ] -> ~lixo( I + 1 )
c [ lixo( I ) ^ embrulhar( I ) ] -> lixo( I + 1 )
c [ ~lixo( I ) ^ embrulhar( I ) ] -> ~lixo( I + 1 )
c [ maos_limpas( I ) ^ cozinhar( I ) ] -> maos_limpas( I + 1 )
c [ ~maos_limpas( I ) ^ cozinhar( I ) ] -> ~maos_limpas( I + 1 )
c [ maos_limpas( I ) ^ embrulhar( I ) ] -> maos_limpas( I + 1 )
c [ ~maos_limpas( I ) ^ embrulhar( I ) ] -> ~maos_limpas( I + 1 )
c [ maos_limpas( I ) ^ triturar_lixo( I ) ] -> maos_limpas( I + 1 )
c [ ~maos_limpas( I ) ^ triturar_lixo( I ) ] -> ~maos_limpas( I + 1 )
c [ silencio( I ) ^ cozinhar( I ) ] -> silencio( I + 1 )
c [ ~silencio( I ) ^ cozinhar( I ) ] -> ~silencio( I + 1 )
c [ silencio( I ) ^ embrulhar( I ) ] -> silencio( I + 1 )
c [ ~silencio( I ) ^ embrulhar( I ) ] -> ~silencio( I + 1 )
c [ silencio( I ) ^ carregar_lixo( I ) ] -> silencio( I + 1 )
c [ ~silencio( I ) ^ carregar_lixo( I ) ] -> ~silencio( I + 1 )
c [ jantar( I ) ^ embrulhar( I ) ] -> jantar( I + 1 )
c [ ~jantar( I ) ^ embrulhar( I ) ] -> ~jantar( I + 1 )
c [ jantar( I ) ^ carregar_lixo( I ) ] -> jantar( I + 1 )
c [ ~jantar( I ) ^ carregar_lixo( I ) ] -> ~jantar( I + 1 )
c [ jantar( I ) ^ triturar_lixo( I ) ] -> jantar( I + 1 )
c [ ~jantar( I ) ^ triturar_lixo( I ) ] -> ~jantar( I + 1 )
c [ presente( I ) ^ cozinhar( I ) ] -> presente( I + 1 )
c [ ~presente( I ) ^ cozinhar( I ) ] -> ~presente( I + 1 )
c [ presente( I ) ^ carregar_lixo( I ) ] -> presente( I + 1 )
c [ ~presente( I ) ^ carregar_lixo( I ) ] -> ~presente( I + 1 )
c [ presente( I ) ^ triturar_lixo( I ) ] -> presente( I + 1 )
c [ ~presente( I ) ^ triturar_lixo( I ) ] -> ~presente( I + 1 )
c
-1 -21 6 0
1 -21 -6 0
-1 -22 6 0
1 -22 -6 0
-2 -21 7 0
2 -21 -7 0
-2 -22 7 0
2 -22 -7 0
-2 -24 7 0
2 -24 -7 0
-3 -21 8 0
3 -21 -8 0
-3 -22 8 0
3 -22 -8 0
-3 -23 8 0
3 -23 -8 0
-4 -22 9 0
4 -22 -9 0
-4 -23 9 0
4 -23 -9 0
-4 -24 9 0
4 -24 -9 0
-5 -21 10 0
5 -21 -10 0
-5 -23 10 0
5 -23 -10 0
-5 -24 10 0
5 -24 -10 0
-6 -25 11 0
6 -25 -11 0
-6 -26 11 0
6 -26 -11 0
-7 -25 12 0
7 -25 -12 0
-7 -26 12 0
7 -26 -12 0
-7 -28 12 0
7 -28 -12 0
-8 -25 13 0
8 -25 -13 0
-8 -26 13 0
8 -26 -13 0
-8 -27 13 0
8 -27 -13 0
-9 -26 14 0
9 -26 -14 0
-9 -27 14 0
9 -27 -14 0
-9 -28 14 0
9 -28 -14 0
-10 -25 15 0
10 -25 -15 0
-10 -27 15 0
10 -27 -15 0
-10 -28 15 0
10 -28 -15 0
-11 -29 16 0
11 -29 -16 0
-11 -30 16 0
11 -30 -16 0
-12 -29 17 0
12 -29 -17 0
-12 -30 17 0
12 -30 -17 0
-12 -32 17 0
12 -32 -17 0
-13 -29 18 0
13 -29 -18 0
-13 -30 18 0
13 -30 -18 0
-13 -31 18 0
13 -31 -18 0
-14 -30 19 0
14 -30 -19 0
-14 -31 19 0
14 -31 -19 0
-14 -32 19 0
14 -32 -19 0
-15 -29 20 0
15 -29 -20 0
-15 -31 20 0
15 -31 -20 0
-15 -32 20 0
15 -32 -20 0
c
c Deve ser escolhida uma ação em cada instante
cccccccccc     Schemas de axiomas de continuidade no plano    cccccccccccc
c cozinhar( I ) v embrulhar( I ) v carregar_lixo( I ) v triturar_lixo( I )
c
21 22 23 24 0
25 26 27 28 0
29 30 31 32 0
c
c Apenas uma acao em cada instante
c	Schemas de axiomas de não paralelismo de ações
c cozinhar( I ) -> ~embrulhar( I )
c cozinhar( I ) -> ~carregar_lixo( I )
c cozinhar( I ) -> ~triturar_lixo( I )
c (repete) embrulhar( I ) -> ~cozinhar( I )
c embrulhar( I ) -> ~carregar_lixo( I )
c embrulhar( I ) -> ~triturar_lixo( I )
c (repete) carregar_lixo( I ) -> ~cozinhar( I )
c (repete) carregar_lixo( I ) -> ~embrulhar( I )
c carregar_lixo( I ) -> ~triturar_lixo( I )
c (repete) triturar_lixo( I ) -> ~cozinhar( I )
c (repete) triturar_lixo( I ) -> ~embrulhar( I )
c (repete) triturar_lixo( I ) -> ~carregar_lixo( I )
c
-21 -22 0
-21 -23 0
-21 -24 0
c -22 -21 0
-22 -23 0
-22 -24 0
-23 -21 0
-23 -22 0
-23 -24 0
-24 -21 0
-24 -22 0
-24 -23 0
-25 -26 0
-25 -27 0
-25 -28 0
-26 -25 0
-26 -27 0
-26 -28 0
-27 -25 0
-27 -26 0
-27 -28 0
-28 -25 0
-28 -26 0
-28 -27 0
-29 -30 0
-29 -31 0
-29 -32 0
-30 -29 0
-30 -31 0
-30 -32 0
-31 -29 0
-31 -30 0
-31 -32 0
-32 -29 0
-32 -30 0
-32 -31 0

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&

Codificação como SAT a partir do Graphplan  (extração manual do grafo)


c CNF resultante de um grafo de planejamento
c
p cnf 14 37
c >>> sub-objetivos do nivel 4

Devemos construir a CNF a partir do último nível do grafo.
Para cada sub-goal seleciono a lista de ações que o adicionam. 

c lista de sub-objetivos de TRUE: jantar( 4 )

True representa uma ação posterior (fictícia) ao nível 4 (análoga à ação FINISH no Pop) que tem como precondição os subgoals deste nível. Primeiramente selecionamos o subgoal jantar(4) e a lista de ações que o adicionam no nível 3

c   proposicao: jantar( 4 ) { cozinhar( 3 ), NOOP-1( 3 ) }

cada possível uma dessas ações será uma proposição na CNF
c     variavel: 1 cozinhar( 3 )
c     variavel: 2 NOOP-1( 3 )
c     deve escolher uma acao para adicionar a proposicao jantar( 4 )

em seguida construimos uma cláusula que indica que somente uma das ações poderá ser escolhida
 
c       TRUE -> cozinhar( 3 ) v NOOP-1( 3 )
1 2 0
c     somente uma acao para adicionar a proposicao jantar( 4 )
c       cozinhar( 3 ) -> ~NOOP-1( 3 )
-1 -2 0

Fazemos o mesmo para o próximo sub-goal: presente(4)

c lista de sub-objetivos de TRUE: presente( 4 )
c   proposicao: presente { embrulhar(3), NOOP-2(3)}
c     variavel: 3 embrulhar( 3 )
c     variavel: 4 NOOP-2( 3 )
c     deve escolher uma acao para adicionar a proposicao presente( 4 )
c       TRUE -> embrulhar( 3 ) v NOOP-2( 3 )
3 4 0
c     somente uma acao para adicionar a proposicao presente( 4 )
c       embrulhar( 3 ) -> ~NOOP-2( 3 )
-4 -3 0

Fazemos o mesmo para o próximo sub-goal: ~lixo(4)

c lista de sub-objetivos de TRUE: ~lixo( 4 )
c   proposicao: ~lixo { carregar_lixo(3), triturar_lixo(3), NOOP-4 (3)}
c     variavel: 5 carregar_lixo( 3 )
c     variavel: 6 triturar_lixo( 3 )
c     variavel: 7 NOOP-4( 3 )

Como neste caso existem 3 ações, precisamos garantir que somente uma será escolhida (XOR)

c     deve escolher uma acao para adicionar a proposicao ~lixo( 4 )
c       TRUE -> carregar_lixo( 3 ) v triturar_lixo( 3 ) v NOOP-4( 3 )
5 6 7 0
c     somente uma acao para adicionar a proposicao ~lixo( 4 )
c       carregar_lixo( 3 ) -> ~triturar_lixo( 3 )
-5 -6 0
c       carregar_lixo( 3 ) -> ~NOOP-4( 3 )
-5 -7 0
c       triturar_lixo( 3 ) -> ~NOOP-4( 3 )
-6 -7 0

Adicionamos todas as restriçoes MUTEX para as ações que adicionam os sub-goals desse nível

c >>> relacoes de esclusao mutua das acoes do nivel 3
c   NOOP-4( 3 ) -> ~triturar_lixo( 3 )
-7 -6 0
c   NOOP-4( 3 ) -> ~carregar_lixo( 3 )
-7 -5 0
c   triturar_lixo( 3 ) -> ~NOOP-4( 3 )
-6 -7 0
c   triturar_lixo( 3 ) -> ~carregar_lixo( 3 )
-6 -5 0
c   carregar_lixo( 3 ) -> ~NOOP-4( 3 )
-5 -7 0
c   carregar_lixo( 3 ) -> ~triturar_lixo( 3 )
-5 -6 0
c   embrulhar( 3 ) -> ~triturar_lixo( 3 )
-3 -6 0
c   cozinhar( 3 ) -> ~carregar_lixo( 3 )
-1 -5 0
c

Selecionamos agora todos os sub-objetivos que são precondições das ações possivelmente selecionadas do nível anterior. Indicamos essa dependência como: 
ação -> ação_que_adiciona_subgoal

c >>> sub-objetivos do nivel 2
c lista de sub-objetivos de cozinhar( 3 ): maos_limpas( 2 )
c   proposicao: maos_limpas( 2 ) { NOOP-2( 1 ) }
c     variavel: 8 NOOP-2( 1 )
c     deve escolher uma acao para adicionar a proposicao maos_limpas( 2 )
c       cozinhar( 3 ) -> NOOP-2( 1 )
-1 8 0

ou seja, ação -> ação_que_adiciona_subgoal

c lista de sub-objetivos de NOOP-1( 3 ): jantar( 2 )
c   proposicao: jantar( 2 ) { cozinhar( 1 ) }
c     variavel: 9 cozinhar( 1 )
c     deve escolher uma acao para adicionar a proposicao jantar( 2 )
c       NOOP-1( 3 ) -> cozinhar( 1 )
-2 9 0
c lista de sub-objetivos de embrulhar( 3 ): silencio( 2 )
c   proposicao: silencio( 2 ) { NOOP-3( 1 ) }
c     variavel: 10 NOOP-3( 1 )
c     deve escolher uma acao para adicionar a proposicao jantar( 2 )
c       embrulhar( 3 ) -> NOOP-3( 1 )
-3 10 0
c lista de sub-objetivos de NOOP-2( 3 ): presente( 2 )
c   proposicao: presente( 2 ) { embrulhar( 1 ) }
c     variavel: 11 embrulhar( 1 )
c     deve escolher uma acao para adicionar a proposicao presente( 2 )
c       NOOP-2( 3 ) -> embrulhar( 1 )
-4 11 0
c lista de sub-objetivos de carregar_lixo( 3 ): lixo( 2 )
c   proposicao: lixo( 2 ) { NOOP-1( 1 ) }
c     variavel: 12 NOOP-1( 1 )
c     deve escolher uma acao para adicionar a proposicao lixo( 2 )
c       carregar_lixo( 3 ) -> NOOP-1( 1 )
-5 12 0
c lista de sub-objetivos de triturar_lixo( 3 ): lixo( 2 )
c   proposicao: lixo( 2 ) { NOOP-1( 1 ) }
c     variavel: 12 NOOP-1( 1 )
c     deve escolher uma acao para adicionar a proposicao lixo( 2 )
c       triturar_lixo( 3 ) -> NOOP-1( 1 )
-6 12 0
c lista de sub-objetivos de NOOP-4( 3 ): ~lixo( 2 )
c   proposicao: ~lixo( 2 ) { carregar_lixo( 1 ), triturar_lixo( 1 ) }
c     variavel: 13 carregar_lixo( 1 )
c     variavel: 14 triturar_lixo( 1 )
c     deve escolher uma acao para adicionar a proposicao ~lixo( 2 )
c       NOOP-4( 3 ) -> carregar_lixo( 1 ) v triturar_lixo( 1 )
-7 13 14 0
c     somente uma acao para adicionar a proposicao ~lixo( 2 )
c       carregar_lixo( 1 ) -> ~triturar_lixo( 1 )
-13 -14 0
c
c >>> relacoes de esclusao mutua das acoes do nivel 1
c   NOOP-1( 1 ) -> ~triturar_lixo( 1 )
-12 -14 0
c   NOOP-1( 1 ) -> ~carregar_lixo( 1 )
-12 -13 0
c   NOOP-2( 1 ) -> ~carregar_lixo( 1 )
-8 -13 0
c   NOOP-3( 1 ) -> ~triturar_lixo( 1 )
-10 -14 0
c   triturar_lixo( 1 ) -> ~carregar_lixo( 1 )
-14 -13 0
c   carregar_lixo( 1 ) -> ~triturar_lixo( 1 )
-13 -14 0
c   embrulhar( 1 ) -> ~triturar_lixo( 1 )
-11 -14 0
c   cozinhar( 1 ) -> ~carregar_lixo( 1 )
-9 -13 0

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Saída do Graphplan  para o problema do Jantar surpresa. A partir dessa saída foi gerada (na mão) a CNF acima. 

Graphplan  -  Versao 1.0 por Aldebaran Perseke em 23/04/2002

problema lido
condicoes de parada: 2
>>> vertices do nivel 0 - proposicoes do estado inicial
	lixo
	maos_limpas
	silencio
	~jantar
	~presente
>>> vertices do nivel 1 - acoes aplicaveis no nivel 0
	cozinhar
	embrulhar
	carregar_lixo
	triturar_lixo
	NOOP-5
	NOOP-4
	NOOP-3
	NOOP-2
	NOOP-1
>>> arestas entre os niveis 0 e 1 - arestas de pre-condicao
	maos_limpas -> cozinhar
	silencio -> embrulhar
	lixo -> carregar_lixo
	lixo -> triturar_lixo
	~presente -> NOOP-5
	~jantar -> NOOP-4
	silencio -> NOOP-3
	maos_limpas -> NOOP-2
	lixo -> NOOP-1
>>> relacoes de exclusao do nivel 1 - exclusao mutua entre acoes
	NOOP-1 || triturar_lixo
	NOOP-1 || carregar_lixo
	NOOP-2 || carregar_lixo
	NOOP-3 || triturar_lixo
	triturar_lixo || carregar_lixo
	carregar_lixo || triturar_lixo
	embrulhar || NOOP-5
	embrulhar || triturar_lixo
	cozinhar || NOOP-4
	cozinhar || carregar_lixo
>>> vertices do nivel 2 - proposicoes de efeito das acoes do nivel 1
	jantar
	presente
	~maos_limpas
	~lixo
	~silencio
	~presente
	~jantar
	silencio
	maos_limpas
	lixo
>>> arestas entre os niveis 1 e 2 - arestas de efeito
	cozinhar -> jantar
	embrulhar -> presente
	carregar_lixo -> ~lixo
	carregar_lixo -> ~maos_limpas
	triturar_lixo -> ~lixo
	triturar_lixo -> ~silencio
	NOOP-5 -> ~presente
	NOOP-4 -> ~jantar
	NOOP-3 -> silencio
	NOOP-2 -> maos_limpas
	NOOP-1 -> lixo
>>> relacoes de exclusao do nivel 2 - exclusao mutua entre proposicoes
	lixo || ~silencio
	lixo || ~lixo
	lixo || ~maos_limpas
	maos_limpas || ~maos_limpas
	silencio || ~silencio
	~jantar || jantar
	~presente || presente
	~silencio || lixo
	~silencio || silencio
	~silencio || ~maos_limpas
	~silencio || presente
	~lixo || lixo
	~maos_limpas || lixo
	~maos_limpas || maos_limpas
	~maos_limpas || ~silencio
	~maos_limpas || jantar
	presente || ~presente
	presente || ~silencio
	jantar || ~jantar
	jantar || ~maos_limpas
>>> vertices do nivel 3 - acoes aplicaveis no nivel 2
	cozinhar
	embrulhar
	carregar_lixo
	triturar_lixo
	NOOP-10
	NOOP-9
	NOOP-8
	NOOP-7
	NOOP-6
	NOOP-5
	NOOP-4
	NOOP-3
	NOOP-2
	NOOP-1
>>> arestas entre os niveis 2 e 3 - arestas de pre-condicao
	maos_limpas -> cozinhar
	silencio -> embrulhar
	lixo -> carregar_lixo
	lixo -> triturar_lixo
	lixo -> NOOP-10
	maos_limpas -> NOOP-9
	silencio -> NOOP-8
	~jantar -> NOOP-7
	~presente -> NOOP-6
	~silencio -> NOOP-5
	~lixo -> NOOP-4
	~maos_limpas -> NOOP-3
	presente -> NOOP-2
	jantar -> NOOP-1
>>> relacoes de exclusao do nivel 3 - exclusao mutua entre acoes
	NOOP-1 || NOOP-3
	NOOP-1 || NOOP-7
	NOOP-2 || NOOP-5
	NOOP-2 || NOOP-6
	NOOP-3 || NOOP-1
	NOOP-3 || NOOP-5
	NOOP-3 || NOOP-9
	NOOP-3 || NOOP-10
	NOOP-3 || triturar_lixo
	NOOP-3 || carregar_lixo
	NOOP-3 || cozinhar
	NOOP-4 || NOOP-10
	NOOP-4 || triturar_lixo
	NOOP-4 || carregar_lixo
	NOOP-5 || NOOP-2
	NOOP-5 || NOOP-3
	NOOP-5 || NOOP-8
	NOOP-5 || NOOP-10
	NOOP-5 || triturar_lixo
	NOOP-5 || carregar_lixo
	NOOP-5 || embrulhar
	NOOP-6 || NOOP-2
	NOOP-7 || NOOP-1
	NOOP-8 || NOOP-5
	NOOP-8 || triturar_lixo
	NOOP-9 || NOOP-3
	NOOP-9 || carregar_lixo
	NOOP-10 || NOOP-3
	NOOP-10 || NOOP-4
	NOOP-10 || NOOP-5
	NOOP-10 || triturar_lixo
	NOOP-10 || carregar_lixo
	triturar_lixo || NOOP-3
	triturar_lixo || NOOP-4
	triturar_lixo || NOOP-5
	triturar_lixo || carregar_lixo
	carregar_lixo || NOOP-3
	carregar_lixo || NOOP-4
	carregar_lixo || NOOP-5
	carregar_lixo || triturar_lixo
	embrulhar || NOOP-5
	embrulhar || NOOP-6
	embrulhar || triturar_lixo
	cozinhar || NOOP-3
	cozinhar || NOOP-7
	cozinhar || carregar_lixo
>>> vertices do nivel 4 - proposicoes de efeito das acoes do nivel 3
	lixo
	maos_limpas
	silencio
	~jantar
	~presente
	~silencio
	~lixo
	~maos_limpas
	presente
	jantar
>>> arestas entre os niveis 3 e 4 - arestas de efeito
	cozinhar -> jantar
	embrulhar -> presente
	carregar_lixo -> ~lixo
	carregar_lixo -> ~maos_limpas
	triturar_lixo -> ~lixo
	triturar_lixo -> ~silencio
	NOOP-10 -> lixo
	NOOP-9 -> maos_limpas
	NOOP-8 -> silencio
	NOOP-7 -> ~jantar
	NOOP-6 -> ~presente
	NOOP-5 -> ~silencio
	NOOP-4 -> ~lixo
	NOOP-3 -> ~maos_limpas
	NOOP-2 -> presente
	NOOP-1 -> jantar
>>> relacoes de exclusao do nivel 4 - exclusao mutua entre proposicoes
	jantar || ~jantar
	presente || ~presente
	~maos_limpas || ~silencio
	~maos_limpas || maos_limpas
	~maos_limpas || lixo
	~lixo || lixo
	~silencio || ~maos_limpas
	~silencio || silencio
	~silencio || lixo
	~presente || presente
	~jantar || jantar
	silencio || ~silencio
	maos_limpas || ~maos_limpas
	lixo || ~maos_limpas
	lixo || ~lixo
	lixo || ~silencio


&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Saida 1 do GSAT

GSAT  -  Versao 1.0 por Aldebaran Perseke em 19/03/2002

trocas = 100
tentativas = 50
atomos = 14, clausulas = 37
cnf lida
Atribuicao encontrada
v -1
v 2
v 3
v -4
v 5
v -6
v -7
v -8
v 9
v 10
v -11
v 12
v -13
v -14

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Saida 2 do GSAT

GSAT  -  Versao 1.0 por Aldebaran Perseke em 19/03/2002

trocas = 100
tentativas = 50
atomos = 14, clausulas = 37
cnf lida
Atribuicao encontrada
v -1
v 2
v -3
v 4
v -5
v 6
v -7
v -8
v 9
v 10
v 11
v 12
v -13
v -14

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Saida 3 do GSAT

GSAT  -  Versao 1.0 por Aldebaran Perseke em 19/03/2002

trocas = 100
tentativas = 50
atomos = 14, clausulas = 37
cnf lida
Atribuicao encontrada
v -1
v 2
v -3
v 4
v 5
v -6
v -7
v -8
v 9
v -10
v 11
v 12
v -13
v -14

&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&
Saida 4 do GSAT (erro)

GSAT  -  Versao 1.0 por Aldebaran Perseke em 19/03/2002

trocas = 100
tentativas = 50
atomos = 14, clausulas = 37
cnf lida
Atribuicao encontrada
v -1
v 2
v 3
v -4
v 5
v -6
v -7
v -8
v 9
v 10
v 11
v 12
v -13
v -14