Os solucionadores SMT como Z3 ou Boolector usam um conjunto complexo de heurísticas para resolver problemas. No entanto, isso também dificulta muito a previsão do desempenho de um solucionador para um determinado problema. Minha pergunta é assim:
Questão
Existe uma maneira de entender ou obter informações sobre o desempenho de um solucionador SMT para um específico na teoria dos vetores de bit sem quantificadores (QFBV)?
Isso também inclui todas as ferramentas de visualização que ajudariam a entender onde o solucionador está "preso" / não faz progresso.
Formulários
Entenda de antemão como diferentes codificações do mesmo problema afetam o desempenho do solucionador (o estado da arte aqui não pode ser "apenas tente algumas codificações diferentes e espero que uma seja rápida o suficiente", certo?)
Se um determinado problema não puder ser solucionado por um solucionador SMT devido a restrições de tempo, encontre uma maneira de expressar o problema de maneira diferente para que ele possa ser resolvido.
Evite perder tempo com simplificações de problemas específicos do domínio que não afetarão o desempenho do solucionador, nem mesmo afetem negativamente o desempenho do solucionador.
Pesquisa existente
Tentei encontrar pesquisas sobre esse tópico, mas não consegui encontrar muita coisa. Ainda não tenho muita experiência no campo de solucionadores de SAT / SMT, então peço desculpas se perdi alguma coisa.
SATzilla : prevê o solucionador com melhor desempenho com base em recursos extraídos do problema usando técnicas de aprendizado de máquina.
Isso se aplica apenas ao SAT em vez do SMT e não explica os motivos do desempenho do solucionador.
Perfil de axioma Z3 Uma visualização do gráfico de instanciação Z3 e análise de loops correspondentes
Parece que isso se concentra apenas nas teorias quantificadas.
fonte