Efficient instantiation techniques in SMT: work in progress
Carregando...
Data
Autor(es)
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal de Minas Gerais
Descrição
Tipo
Artigo de evento
Título alternativo
Técnicas de instanciação eficientes em SMT: trabalho em andamento
Primeiro orientador
Membros da banca
Resumo
In 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.
Abstract
Na 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.
Assunto
Teorias do Módulo de Satisfabilidade, Lógica de primeira ordem, Logica simbolica e matematica
Palavras-chave
Satisfiability Modulo Theories, SMT solving, Quantifier instantiation, Artificial intelligence