Cambalache 3,14 - La vidriera irrespetuosa

A Geometria Computacional possui um vasto campo de aplica\c{c}\~{o}es nas \'{a}reas das Ci\^{e}ncias da Informa\c{c}\~{a}o Geogr\'{a}fica, Electr\'{o}nica e Computa\c{c}\~{a}o, entre muitas outras. Nestes dom\'{\i}nios, problemas de etiquetado de mapas, tra\c{c}ados de circuitos integrados ou cria\c{c}\~{a}o de diagramas de fluxos e organogramas constituem exemplos particulares de problemas cujas inst\^{a}ncias s\~{a}o redut\'{\i}veis ao problema da satisfa\c{c}\~{a}o proposicional (\textsc{sat}). Pelo que a sua resolu\c{c}\~{a}o pode ser conseguida a partir da resolu\c{c}\~{a}o de determinadas inst\^{a}ncias de \textsc{sat}.

\textsc{Sat} \'{e} um bem conhecido problema NP-completo, fundamental nas Ci\^{e}ncias da Computa\c{c}\~{a}o. Apesar da sua intratabilidade, s\~{a}o conhecidas diversas (sub)classes resol\'{u}veis em tempo polinomial. No presente trabalho apresenta-se uma nova classe de satisfa\c{c}\~{a}o polinomial: \textsc{purl} (\emph{PropUnit Removable Literal}).A qual, em certo sentido, constitui uma superclasse relativamente \`{a}s classes de satisfa\c{c}\~{a}o polinomial identificadas no trabalho de Franco e van Gelder como \emph{bem conhecidas}~\cite{FG03}. A partir desta nova classe define-se uma hierarquia de classes de satisfa\c{c}\~{a}o, \textsc{purl} $\subset$ $\textsc{purl} $\subset \cdots \subset$ $k$\textsc{purl}, na linha dos trabalhos sobre hierarquias de Gallo e Scutella.

\textsc{Purl} \'{e} definida a partir do conceito de literal p-elimin\'{a}vel, pelo qual as cl\'{a}usulas de uma f\'{o}rmula proposicional se podem simplificar. Dado que a f\'{o}rmula simplificada e a original s\~{a}o logicamente equivalentes, o procedimento de identifica\c{c}\~{a}o e exclus\~{a}o de literais p-elimin\'{a}veis poder\'{a} ser adoptado como metodologia de pr\'{e}-processamento para qualquer inst\^{a}ncia de \textsc{sat}. Como os literais p-elimin\'{a}veis s\~{a}o reconhec\'{\i}veis em tempo linear, este pr\'{e}-processamento \'{e} efectuado em tempo polinomial.

Para uma adequada codifica\c{c}\~{a}o com recurso a vari\'{a}veis l\'{o}gicas booleanas, reduzindo as inst\^{a}ncias do problema de etiquetado de pontos alinhados com etiquetas quadradas a inst\^{a}ncias de \textsc{sat}, obt\'{e}m-se a classe \textsc{uc-4p-sat}, subclasse de \textsc{purl}. Por outro lado, reduzindo as inst\^{a}ncias do problema de emparelhamento ortogonal simples no cilindro obt\'{e}m-se a classe de satisfa\c{c}\~{a}o proposicional \textsc{eosc-sat}, subclasse de 2\textsc{purl}. Para al\'{e}m do interesse espec\'{\i}fico destes problemas, a t\'{e}cnica utilizada poder\'{a} ser adoptada na resolu\c{c}\~{a}o em tempo polinomial de outros
problemas.

Como principais contributos do presente trabalho salientam-se, entre outros, a defini\c{c}\~{a}o da nova classe de satisfa\c{c}\~{a}o polinomial e a aplica\c{c}\~{a}o do conceito de literal p-elimin\'{a}vel na resolu\c{c}\~{a}o de problemas pr\'{a}ticos. \textsc{Purl}, cont\'{e}m propriamente cada uma das classes polinomiais \emph{bem conhecidas}. Pelo que a metodologia desenvolvida a partir do conceito de literal p-elimin\'{a}vel (para resolu\c{c}\~{a}o das inst\^{a}ncias de \textsc{purl}, e portanto do problema da satisfa\c{c}\~{a}o proposicional das inst\^{a}ncias de todas estas classes) constitui uma abordagem unificadora.

No presente trabalho, mostra-se ainda que o algoritmo de reconhecimento e exclus\~{a}o de literais p-elimin\'{a}veis pode ser utilizado eficientemente na resolu\c{c}\~{a}o de algumas inst\^{a}ncias do problema da satisfa\c{c}\~{a}o proposicional.

A concluir, na parte final do presente trabalho utiliza-se o conceito de literal p-elimin\'{a}vel para a resolu\c{c}\~{a}o de dois problemas geom\'{e}tricos que estavam por resolver. Esta mesma metodologia poder\'{a} ser aplicada na resolu\c{c}\~{a}o de problemas similares, de natureza geom\'{e}trica ou n\~{a}o.