Eu obtive várias estatísticas de corridas de Z3. Eu preciso entender o que isso significa. Eu estou bastante enferrujado e não atualizado para os recentes desenvolvimentos de sat e SMT resolvendo, por esse motivo eu tentei encontrar explicações eu mesmo e eu poderia estar completamente errado. Então minhas perguntas são principalmente:

1) O que significam os nomes das medidas?

2) Se errado, você pode me dar dicas para entender melhor o que eles se referem?

Outras observações são feitas abaixo e conceitualmente pertencem às duas perguntas acima. Desde já, obrigado!

Minha interpretação segue.

DPLL. Todas as métricas abaixo se referem ao jargão do algoritmo DPLL, que é a base da maioria dos solucionadores.

: decisõesNúmero de decisões: propagaçõesNúmero de propagações (eu acho que propagações de unidade): propagações binárias, :propagações ternáriasPropagações de dois e três literais de uma só vez: conflitosNúmero de conflitos

RESOLUÇÃO. As operações fizeram cláusulas de interpretação como conjuntos, grosso modo falando; técnicas tomadas de resolução, que é outro paradigma para resolver SAT.

: subsumed: resolução de subsunçãoQual é a diferença entre os dois acima?: resolução dyn-subsumptionDeve ser descrito aqui: Learning for Dynamic Subsumption, por Hamadi et al.

OUTRAS TÉCNICAS

: lits minimizadosNenhuma ideia clara. Está provavelmente relacionado com a aprendizagem de cláusulas?: sondagem atribuídaEu acho que conta o número de tarefas feitas quando "sondar", o que eu acho que é uma espécie de técnica de lookahead.: del-cláusulaNúmero de cláusulas excluídas (por que motivo? Redundante?):elim-liters :cláusulas-elim :elim-bool-vars :cláusulas elim-bloqueadasNúmero de entidades após oelimi- eliminado. Estas métricas referem-se a técnicas particulares de solução de SAT (ver referência para Eliminação de Cláusulas Bloqueadas, por M.Järvisalo et al.): reiniciaNúmero de reinicializações.

OUTROS ASPECTOS

: mk-bool-var :mk-binary-clause :mk-ternary-clause :cláusula mkNúmero de variáveis ​​booleanas e cláusulas binárias, ternárias e genéricas criadas.:memóriaQuantidade máxima de memória usada.: cláusula gcCláusulas colecionadas de lixo ...?Esta interpretação é plausível de acordo com minhas experiências, já que é sempre o caso:cláusula gc <=:del-cláusula ; no meu caso, a desigualdade é estrita.Nem sempre é o caso:cláusula gc<=:cláusulas-elim; também pode ser:cláusula gc >:cláusulas-elim