Definição de Planar 3-SAT

O que você achou confuso sobre os resultados?

Vejo definições diferentes, como alguns dizem: O gráfico bipartido entre cláusulas e literais deve ser plano (não sei por literais, eles significam apenas xi ou ambos xi e sua negação, quero dizer que não sei qual é o gráfico de gadgets exatamente aqui?). Alguns outros definem dois tipos para isso: apenas as arestas bipartidas entre cláusulas e literais, ou essas mais (x_i, ~ x_i). Ou algum outro diz, o gráfico acima mais os (x_i, x_ {i + 1})? Não consigo encontrar o artigo original publicado nele? Basicamente, não consigo encontrar uma boa referência com uma definição perfeita para isso?

A referência original é: D. Lichtenstein, "Fórmulas planares e seus usos" (1982) ; mas existem muitas pequenas variações que ainda são NP-completas (a prova NPC da maioria delas é fácil).

@Marzio De Biasi Muito obrigado! Mas, com base nesse par, o planar 3-SAT é o caso em que o gráfico bipartido entre as cláusulas que os literais (apenas x_i não são negações) é planar. Direita? Podemos concluir facilmente que incluímos também a negação de x_i apenas adicionando uma vantagem entre eles, sem perturbar a planaridade, certo?

@tinLoaf: como citado na muito boa palestra vinculada por David Eppstein em sua resposta, você pode olhar para Mark de Berg e Amirali Khosravi, ótimas partições de espaço binário no plano; em que está provado que o 3-SAT plano monótono é NPC: as variáveis ​​são colocadas em uma linha horizontal, todas as cláusulas positivas são desenhadas acima, todas as cláusulas negativas são desenhadas abaixo; nessa representação, é fácil substituir cada variável por dois literais empilhados (e também vinculados), o literal positivo acima, o literal negativo abaixo, sem interromper a condição de planaridade. $x_i$$+x_i$$-x_i$