Efficient instantiation techniques in SMT: work in progress

Página do item simplificado
dc.creatorHaniel Moreira Barbosa
dc.date.accessioned2021-09-22T16:32:09Z
dc.date.accessioned2025-09-09T01:33:03Z
dc.date.available2021-09-22T16:32:09Z
dc.date.issued2016
dc.description.abstractNa solução SMT, geralmente se aplica a instanciação heurística para lidar com fórmulas quantificadas. Isso tem o efeito colateral de produzir muitas ocorrências espúrias e pode levar à perda de desempenho. Portanto, derivar menos e mais instâncias significativas, bem como eliminar ou descartar, ou seja, manter, mas ignorar, aquelas não significativas para a resolução são características desejáveis para lidar com problemas de primeira ordem. Este artigo apresenta um trabalho preliminar em duas abordagens: a implementação de um framework de instanciação eficiente com uma busca orientada a objetivos incompletos; e a introdução de critérios de dispensa para instâncias heurísticas. Nossos experimentos mostram que enquanto o primeiro melhora o desempenho em geral, o último é altamente dependente da estrutura do problema, mas sua combinação com a estratégia clássica leva a resultados competitivos w.r.t. Solucionadores SMT de última geração em várias bibliotecas de referência.
dc.format.mimetypepdf
dc.identifier.issnhttps://hal.inria.fr/hal-01388976v1
dc.identifier.urihttps://hdl.handle.net/1843/38132
dc.languageeng
dc.publisherUniversidade Federal de Minas Gerais
dc.relation.ispartofWorkshop on Practical Aspects of Automated Reasoning: PAAR 2016 ; International Joint Conference on Automated Reasoning: IJCAR 2016.
dc.rightsAcesso Aberto
dc.subjectTeorias do Módulo de Satisfabilidade
dc.subjectLógica de primeira ordem
dc.subjectLogica simbolica e matematica
dc.subject.otherSatisfiability Modulo Theories
dc.subject.otherSMT solving
dc.subject.otherQuantifier instantiation
dc.subject.otherArtificial intelligence
dc.titleEfficient instantiation techniques in SMT: work in progress
dc.title.alternativeTécnicas de instanciação eficientes em SMT: trabalho em andamento
dc.typeArtigo de evento
local.citation.epage10
local.citation.issue8
local.citation.spage1
local.description.resumoIn SMT solving one generally applies heuristic instantiation to handle quantified formulas. This has the side effect of producing many spurious instances and may lead to loss of performance. Therefore deriving both fewer and more meaningful instances as well as eliminating or dismissing , i.e., keeping but ignoring, those not significant for the solving are desirable features for dealing with first-order problems. This paper presents preliminary work on two approaches: the implementation of an efficient instantiation framework with an incomplete goal-oriented search; and the introduction of dismissing criteria for heuristic instances. Our experiments show that while the former improves performance in general the latter is highly dependent on the problem structure, but its combination with the classic strategy leads to competitive results w.r.t. state-of-the-art SMT solvers in several benchmark libraries.
local.identifier.orcidhttps://orcid.org/0000-0003-0188-2300
local.publisher.countryBrasil
local.publisher.departmentICX - DEPARTAMENTO DE CIÊNCIA DA COMPUTAÇÃO
local.publisher.initialsUFMG

Arquivos

Pacote original

Agora exibindo 1 - 1 de 1
Imagem de Miniatura
Nome:
DCC _Barbosa Haniel Gabriel _Efficient Instantiation Techniques in SMT _Artigo de evento016.pdf
Tamanho:
776.4 KB
Formato:
Adobe Portable Document Format
Baixar

Licença do pacote

Agora exibindo 1 - 1 de 1
Imagem de Miniatura
Nome:
license.txt
Tamanho:
2.07 KB
Formato:
Plain Text
Descrição:
Baixar

Coleções

Artigo de Evento

Logo UFMG