Representação de Fórmulas Lógicas através de Estruturas de Dados

Representação de Fórmulas Lógicas através de Estruturas de Dados

(Parte 1 de 2)

Representação de Fórmulas Lógicas através de Estruturas de Dados

Emerson Shigueo Sugimoto1 , Adolfo Neto1

1 Departamento Acadêmico de Informática – Universidade Tecnológica Federal do

Paraná (UTFPR) Caixa Postal 80230-901, nº 3165 – Curitiba – PR – Brasil eme.vbnet@gmail.com adolfo@utfpr.edu.br

Abstract. This paper presents and performs the analysis of different forms of representation of propositional logic formulas via data structures created through a language of object-oriented programming, specifically the language used in this work has been Java. The main goal is to represent logical formulas with a low memory footprint, efficiently from a computational standpoint.

Resumo. Este trabalho apresenta e realiza a análise de diferentes formas de representação de fórmulas lógicas proposicionais através de estruturas de dados criadas através de uma linguagem de programação orientada a objetos, especificamente neste trabalho a linguagem utilizada foi o Java. O principal objetivo é representar fórmulas lógicas com um baixo consumo de memória, de forma eficiente do ponto de vista computacional.

1. Introdução

A representação de fórmulas lógicas de uma forma eficiente do ponto de vista computacional é de fundamental importância para provadores de teoremas, por eficiente subentende-se o baixo consumo de memória e o menor tempo utilizado na construção destas fórmulas. Quanto menor o consumo de memória e tempo de criação, maior será o poder computacional de um provador de teoremas, visto que ele necessita representar dezenas, centenas ou milhares de fórmulas lógicas durante a sua execução.

Este trabalho tem por objetivo apresentar e analisar soluções computacionais para representação de fórmulas lógicas proposicionais através de uma estrutura de dados criada através de uma linguagem de programação orientada a objetos. Para tanto foram analisados os consumos de memória e tempo de execução de todas as soluções.

Foramdesenvolvidas quatro soluções para representação das fórmulas e também

2. Materiais e Métodos foi feita a análise da representação de fórmulas apresentada no provador de teoremas KEMS [6], totalizando-se cinco soluções analisadas. Os testes foram realizados em uma máquina com 512 MB de memória RAM, processador AMD Athlon(tm) 64 3000+ e sistema operacional GNU/Linux versão 5.0, disponibilizada pela Universidade Tecnológica Federa do Paraná (UTFPR).

A análise de consumo de tempo foi feita pelo software perf [7], ele permite o monitoramento de uso de recursos ou eventos acionados à partir da execução de um processo. Ele realiza uma análise de performance de softwares que funcionam sob o sistema operacional Linux.

Para o controle de versões das soluções propostas, foi utilizado o sistema de controle de versões Git [1]. Além disso, o código foi disponibilizado no site Github [2], que permite de forma gratuita a hospedagem de arquivos e o controle de versões de um software de forma online e entre diversos colaboradores. As soluções desenvolvidas estão disponíveis através do link git@github.com:surfx/IC.git [3].

Para análise e testes das soluções apresentadas, a tecnologia JUNIT [5] de testes padronizados em Java foi utilizada.

Uma fórmula da lógica proposicional pode ser atômica ou uma fórmula composta, sendo que uma fórmula composta pode formada de fórmulas atômicas ou de outras fórmulas compostas. Toda fórmula atômica possui um identificador, em nossas soluções, o identificador é representado através de uma String, assim "A" ou "B3_5" são exemplos de identificadores. Toda fórmula composta tem um conectivo e zero ou mais subfórmulas, que podem ser fórmulas atômicas ou outras fórmulas compostas. Todo conectivo possui uma aridade (um número inteiro maior ou igual a zero), assim a aridade do conectivo determina a quantidade de subfórmulas, isto é, se em uma fórmula composta o conectivo tem aridade três, esta fórmula terá três subfórmulas. Exemplos de fórmulas:

A&B, conectivo: &, aridade: 2. Subfórmulas: A, B

A&(B&C), conectivo: &, aridade: 2. Subfórmulas: A, B&C

!A, conectivo: !, aridade: 1. Subfórmulas: A

TOP, conectivo: TOP, aridade: 0. Subfórmulas: 0 Exemplos de conectivos:

Zero-ários: TOP (veracidade), BOTTOM (falsidade).

Unários: ! (negação, não), @ (consistência), * (inconsistência).

Binários: & (conjunção, e), | (disjunção, ou), -> (implicação; se, então).

3. Resultados e Discussão

O diagrama de classes da solução 1 esta representado na Figura 1. Esta solução utiliza uma estrutura de dados chamada lista ligada (linked list) de objetos que implementem a interface IFormula para armazenar as subfórmulas. Assim o objeto FormulaComposta, que implementa a interface IFormula, possui um objeto conectivo, e este por sua vez possui a lista de subfórmulas, que podem ser fórmulas atômicas ou outras fórmulas compostas. O objetivo da criação da lista ligada era o de eliminar a possibilidade de ponteiros de objetos IFormula nulos, nos casos de conectivos zero-ários e unários que poderiam existir no objeto Conectivo.

A solução 2 (diagrama de classes representado na Figura 2) especifica mais os conectivos do que a solução 1, nesta solução a interface IConectivo é especificada em outras interfaces, a IConectivoUnario e IConectivoBinario, e a interface IFormula é especificada em outras interfaces, a interface IFormulaComposta e IFormulaAtomica, eliminando-se desta forma a necessidade da criação de uma lista encandeada para armazenamento de fórmulas por parte do objeto Conectivo, da solução 1. Semelhantemente à solução 1, a classe FormulaComposta e FormulaAtomica possuem um conectivo, e este, que pode ser unário, binário ou zeroário, contém as subfórmulas.

Figura 1. Diagrama de classes da Solução 1

Figura 2. Diagrama de classes da Solução 2

A solução 3 (diagrama de classes representado na Figura 3) tem a mesma configuração base da solução 2, a diferença é que nesta solução foi criado um repositório de identificadores de fórmulas, estes que são representados por Strings (ex.: "A1", "B2") são transformados em um número do tipo Short, que possui um tamanho computacional menor do que uma variável do tipo String. Desta forma uma classe

Factory (FormulaFactory) foi criada com a função de criar fórmulas através da classe Flyweigth RepositorioIdentificadores, que por sua vez converte os identificadores Strings em Shorts através do uso de uma lista ligada (linked list). Objetiva-se aqui compensar a manutenção desta estrutura de lista ligada na memória com relação ao número de fórmulas criadas.

Figura 3. Diagrama de classes da Solução 3

A Solução 4 (diagrama de classes representado na Figura 4) é a apresentada pelo provador de teoremas do KEMS [6], nesta solução as fórmulas são armazenadas através de uma lista (objeto List no Java), são criadas através de uma Factory FormulaFactory e o conectivo possui a sua aridade representada por um objeto da classe Arity. Uma fórmula composta (CompositeFormula) possui um conectivo e uma lista de fórmulas (FormulaList), e herda de uma classe abstrata Formula.

Figura 4. Diagrama de classes da Solução 4

A solução 5 (diagrama de classes representado na Figura 5) tem por base a solução 4 e a solução 2, a interface IFormula é especificada em 4 outras interfaces, a interface IFormulaUnaria, IFormulaBinaria, IFormulaAtomica e IFormulaZeroaria, que eliminam a necessidade de uma lista para armazenar as subfórmulas como na solução 4 e solução 1, diminuindo-se desta forma o consumo de memória. A classe e interface de conectivos foram suprimidas e no seu lugar os conectivos são representados através de enums (localizados na classe EnumsConectivos).

Figura 5. Diagrama de classes da Solução 5

Para comparação das soluções através do software perf [7] e de consumo de memória, cada solução submetida tinha por objetivo criar 1 milhão de fórmulas como representado na Figura 6.

Desta forma além da criação de fórmulas básicas através do procedimento „criacaoFormulas()‟, a solução deveria criar duas fórmulas atômicas para vet[0] e vet[1] e fórmulas compostas para as demais posições dos vetores, assim se vet[0] = “A0” e vet[1] = “A1”, a fórmula composta em vet[2] seria composta por vet[0] vet[1], ou seja, “A0” & “A1”, e assim sucessivamente.

public static void main(String[] args) {

System.out.println("-(i)------------------------"); IFormula vet[] = new IFormula[1000000]; for (int i = 0; i < vet.length; i++){ if (i < 2){ vet[i] = new FormulaAtomica("A" + i); } else { vet[i] = new FormulaBinaria(Conectivo.AND, vet[i-1], vet[i-2]); } criacaoFormulas(); }

private static void criacaoFormulas(){

IFormula v[] = new IFormula[9]; v[0] = new FormulaAtomica("A1"); v[1] = new FormulaAtomica("A2"); v[2] = new FormulaUnaria(Conectivo.NEGATION, v[0]); //!A1 v[3] = new FormulaUnaria(Conectivo.NEGATION, new FormulaUnaria(Conectivo.NEGATION, v[1])); //!!A2 v[4] = new FormulaBinaria(Conectivo.AND, v[0], v[1]); //A1&A2 v[5] = new FormulaBinaria(Conectivo.AND, v[2], v[1]); //!A1&A2 v[6] = new FormulaBinaria(Conectivo.OR, v[0], v[3]);//A1||!!A2 v[7] = new FormulaBinaria(Conectivo.IMPLIES, v[4], v[1]);//(A1&A2)->A2

IFormula f1 = new FormulaBinaria(Conectivo.OR, v[2], new FormulaUnaria(Conectivo.NEGATION, v[1])); v[8] = new FormulaBinaria(Conectivo.IMPLIES, v[4], f1); //(A1&A2)- >(!A1||!A2) }

Figura 6 – Arquivo main.java da Solução 5

Para cada solução foi criado um arquivo .jar executável para análise de tempo de execução através do software perf [7], através do comando: perf stat java -jar ARQJAR.jar.

O resultado das comparações feitas através do perf [7] esta na Tabela 1 e na

Figura 7. A solução 4 apresentada pelo software KEMS [6] não conseguiu terminar sua execução e o tempo tomado foi o de 2,83263 segundos pelo software perf [7].

A análise de memória consumida foi feita através da criação diferentes quantidades de fórmulas pelas estruturas sugeridas em cada solução, inicialmente para 1, 5, 30, 50, 2000, 10000, 200000 e 1000000 de fórmulas. A criação destas fórmulas é igual à criação das fórmulas apresentadas na Figura 6, a única diferença é o número de fórmulas criadas.

O resultado desta análise esta representada na Figura 8. Observa-se que a solução 4 conseguiu executar até a criação de 30 fórmulas e usou uma quantidade de 7,69E+007 bytes de memória nesta tarefa.

Tabela 1. Comparações das soluções através do perf [7] *

Soluções Sol1 Sol2 Sol3 Sol 4* Sol 5 Tempo de Execução 2,508751868 0,806576171 1,36524 2,83263 0,570379 Tarefas de Relógio 2400,326848 762,173346 1232,037 21133,91 517,474 Trocas de Contexto 499 238 537 11622 262 Migração de CPU 0 0 0 0 0 Faltas de Página 41987 13682 18133 82811 10437 Ciclos 0 0 0 0 0 Instruções 0 0 0 0 0

Referências à cache 0 0 0 0 0 *solução 4 não chegou a terminar a execução;

Figura 7. Gráfico dos tempos de execução * *obs: a solução 4 não foi adicionada ao gráfico devido ao seu tempo de execução, que foi muito superior aos demais, de forma à prejudicar a comparação das soluções 1,2,3 e 5;

(Parte 1 de 2)

Comentários