Resumo Técnico: Aprendendo Heurísticas de Divisão para Solvers de Strings Paralelos

Declaração do Problema

Solvers de restrições de strings são essenciais para verificar programas que manipulam strings em domínios como imposição de políticas de segurança e execução simbólica. No entanto, muitas restrições de strings práticas são indecidíveis, e os solvers existentes frequentemente enfrentam dificuldades com escalabilidade e instâncias complexas do mundo real. Embora as arquiteturas multi-core ofereçam uma oportunidade para a resolução paralela, a eficácia das estratégias de divisão e conquista (especificamente o cube-and-conquer) depende fortemente da qualidade das heurísticas de divisão. Essas heurísticas determinam em qual átomo (restrição) realizar o branching para particionar o espaço de busca em subproblemas.

As heurísticas de divisão atuais são tipicamente projetadas manualmente e estáticas. Elas frequentemente falham em se adaptar às características estruturais específicas de instâncias de restrições individuais. Além disso, abordagens automatizadas existentes no domínio SAT, como a classificação por pares, sofrem de limitações significativas quando aplicadas ao solving de SMT de strings:

1. Perda de Informação Quantitativa: Reduzir tempos de resolução a rótulos binários descarta dados de custo refinados.
2. Erros em Cascata: Comparações seriais na classificação por pares levam ao acúmulo de erros, degradando a qualidade da predição.
3. Escalabilidade: Métodos de pares exigem varreduras lineares (ou piores) sobre pares candidatos, o que é computacionalmente caro.
4. Aplicabilidade ao Domínio: Métodos automatizados anteriores foram validados primariamente em SAT, com aplicabilidade não comprovada para teorias SMT como strings.

Metodologia

Os autores introduzem o Owl, um framework orientado a dados que gera automaticamente heurísticas de divisão para solvers de strings paralelos. A inovação central é reformular o problema de seleção de átomos de uma tarefa de classificação para uma tarefa de regressão.

1. Formulação do Problema como Regressão

Em vez de comparar dois átomos para determinar qual é "melhor" (classificação), o Owl prevê o tempo de resolução contínuo ($Time(\varphi, p)$) necessário para resolver os subproblemas induzidos pela divisão em um átomo específico $p$.

• Definição de Custo: A variável alvo é definida com base no resultado da execução paralela dos dois ramos ($\varphi \land p$ e $\varphi \land \neg p$). Por exemplo, se ambos os ramos forem satisfatíveis, o custo é o mínimo de seus tempos de resolução; se ambos forem insatisfatíveis, o custo é o máximo.
• Vantagem: Esta abordagem preserva a continuidade das métricas de desempenho, evita os erros de discretização da classificação e elimina a necessidade de comparações exaustivas por pares, reduzindo assim o overhead de inferência.

2. Engenharia de Características (Feature Engineering)

Para suportar o modelo de regressão, os autores projetaram um conjunto abrangente de 77 características para cada átomo candidato, dividido em duas categorias:

• Características Estáticas (66 características): Derivadas da estrutura da fórmula sem a execução do solver. Estas incluem distribuições de operadores (ex: contagens de str.increment, re.union), tamanhos de cláusulas e propriedades de grafos (ex: graus de variável-cláusula).
• Características Dinâmicas (11 características): Capturadas via heurísticas de lookahead (antecipação) e lookback (retrospectiva) de curto prazo durante a execução do solver.
  • Lookback: Rastreia estados históricos do solver, como o número de vezes que um átomo apareceu em cláusulas de conflito ou lemmas aprendidos.
  • Lookahead: Simula propagação de restrições limitada (tipicamente limitada a ~600 conflitos) para observar consequências imediatas, como o número de novas atribuições ou cláusulas aprendidas.

3. Seleção e Treinamento do Modelo

• Algoritmo: O sistema emprega Random Forest Regression como o modelo preditivo central. Esta escolha equilibra precisão preditiva com velocidade de inferência e robustez a rótulos ruidosos (variações nos tempos de resolução).
• Dados de Treinamento: Um conjunto de dados é construído executando o solver em diversas fórmulas de benchmark, dividindo em vários átomos e registrando os tempos de resolução e vetores de características resultantes.
• Implantação: O modelo treinado é integrado ao solver (Z3seq e Z3str4). Em cada ponto de decisão, o solver constrói uma matriz de características para os átomos candidatos, envia-a para um processo worker paralelo via IPC e recebe o átomo previsto com o menor tempo de resolução estimado.

Principais Contribuições

1. Formulação Inovadora: O artigo propõe recascar o design de heurísticas de divisão para o solving de strings paralelo como um problema de regressão, em vez de um problema de classificação por pares.
2. Framework de Aprendizado Prático: Introduz um framework que gera automaticamente heurísticas usando um conjunto rico de 77 características dedicadas à instância (estáticas e dinâmicas).
3. Implementação e Avaliação: A abordagem é implementada e avaliada em dois solvers de strings de última geração, Z3seq e Z3str4, demonstrando ganhos significativos de desempenho sobre heurísticas projetadas manualmente.

Resultados Experimentais

Os autores avaliaram o Owl em 1.024 fórmulas QF_SLIA do repositório SMT-LIB usando 4, 8, 16 e 32 threads.

• Capacidade de Resolução: Com 4 threads, o Z3seq(Owl) resolveu 46 fórmulas a mais (um aumento de 4,8%) que o baseline, e o Z3str4(Owl) resolveu 9 fórmulas a mais. Esses melhorias foram sustentadas em todas as configurações de threads.
• Desempenho de Tempo de Execução:
  • O Z3seq(Owl) alcançou um speedup médio de 1.44× com 32 threads.
  • O Z3str4(Owl) alcançou um speedup médio de 1.59× com 32 threads.
• Precisão de Predição: Os modelos de regressão superaram significativamente as heurísticas de lookahead padrão e o baseline de classificação por pares. Para o Z3seq, o modelo identificou corretamente os top 20% de átomos em quase 45% dos casos, comparado ao desempenho aleatório do baseline.
• Overhead: O overhead computacional da extração de características e inferência do modelo foi mínimo, representando apenas 23,6% do tempo total de resolução, o que é comparável ou inferior ao overhead da heurística de lookahead padrão.
• Importância das Características: A análise revelou que, embora os rankings específicos de características variem entre os solvers (indicando necessidades de otimização específicas do solver), características críticas como "número de atribuições", "score de lookahead" e contagens de operações de string específicas permanecem consistentemente importantes.

Significância e Alegações

O artigo afirma que o Owl proporciona um avanço significativo no solving de restrições de strings paralelo ao automatizar o design de heurísticas de divisão. Ao mudar de heurísticas manuais e estáticas para modelos de regressão orientados a dados, a abordagem se adapta efetivamente às características específicas de restrições de strings complexas.

Os autores enfatizam que seu método:

• Supera as heurísticas criadas manualmente em termos de número de instâncias resolvidas e tempo médio de resolução.
• Mitiga os problemas de acúmulo de erro e perda de informação inerentes às abordagens de classificação por pares.
• Demonstra que heurísticas aprendidas podem ser integradas eficientemente em solvers baseados em CDCL($T$) existentes (Z3seq e Z3str4) para desbloquear o potencial de arquiteturas paralelas.

O trabalho conclui que, embora a eficiência do solver sequencial limite o speedup global, as heurísticas aprendidas maximizam efetivamente o paralelismo ao criar subproblemas bem balanceados, levando a melhorias práticas substanciais na capacidade de resolução.