Resumo Técnico: Tableaux CEGAR Modal com RECAR e Atalhos de Resolução baseados em SAT

Declaração do Problema

O artigo aborda o desafio de decidir eficientemente a satisfatibilidade na lógica multimodal $K_n$ (também conhecida como ALC). Embora os tableaux de Counter-Example Guided Abstraction Refinement (CEGAR) tenham se mostrado altamente eficazes para problemas insatisfatíveis e muitos satisfatíveis, eles enfrentam dificuldades com instâncias satisfatíveis de grande escala. Especificamente, a implementação anterior dos autores, o CEGARBox, superou outros solvers nos benchmarks padrão, mas perdeu para o provador de resolução modal KSP no conjunto de benchmarks MQBF. O problema central identificado é que os tableaux-CEGAR constroem explicitamente modelos satisfatíveis; para problemas com altos fatores de ramificação, isso pode levar à geração de modelos exponencialmente grandes, causando timeouts. Diferente dos métodos baseados em resolução (como o KSP), que podem determinar a satisfatibilidade via saturação sem construir explicitamente um modelo completo, os tableaux-CEGAR carecem de um "atalho ESAT" eficaz (um mecanismo para confirmar rapidamente a satisfatibilidade sem a construção total do modelo).

Metodologia

Os autores investigam duas abordagens distintas para integrar atalhos ESAT em tableaux-CEGAR, implementadas em um novo sistema C++ chamado CEGARBox++. Ambas as abordagens utilizam uma estrutura de dados Trie para armazenar cláusulas modais em Forma Normal Clausal Modal Separada (SNFmc).

1. A Abordagem RECAR (RECARTAB)

Este método adapta o framework RECAR (Recursive Explore and Check Abstraction Refinement), originalmente proposto por Lagniez et al. para CEGAR geral.

• Mecanismo: Em vez de criar um mundo separado para cada cláusula diamante disparada (o que leva à ramificação exponencial), o RECARTAB tenta agrupar múltipls cláusulas diamante em um único mundo sucessor usando uma sobre-aproximação. Ele anota as cláusulas diamante com rótulos e tenta satisfazer uma conjunção de seus alvos em um único mundo.
• Refinamento: Se um conflito ocorrer envolvendo múltiplos diamantes, o algoritmo os separa atribuindo novos rótulos e reinicia a busca.
• Objetivo: Encontrar um modelo menor (menos mundos) do que a abordagem CEGAR padrão, evitando assim o blowup exponencial na geração de mundos.

2. A Abordagem de Oráculo Baseada em Resolução (CEGARBox++(KSP))

Esta abordagem inovadora integra o provador de teoremas de resolução modal KSP como um oráculo para detectar "pontos fixos" (fixpoints) na busca CEGAR.

• M mecanismo: O sistema executa o CEGARBox++ e o KSP em paralelo (multithreaded). O KSP opera em uma Trie linear (SNFml) e realiza a resolução da camada modal mais profunda até a raiz.
• Detecção de Ponto Fixo: Quando o KSP satura completamente uma camada modal $l$ em relação à camada $l+1$, ele produz cláusulas clássicas aprendidas. O CEGARBox++ importa essas cláusulas. Se uma camada estiver saturada (um "ponto fixo" é alcançado), o CEGARBox++ infere que nenhum refinamento adicional (aprendizado de novas cláusulas) é possível para aquela camada.
• Atalho: Ao detectar um ponto fixo, o CEGARBox++ pula o processo custoso de gerar mundos sucessores (a regra "jump") para aquela camada e retorna imediatamente Satisfatível, baseando-se no lema de que, se a sub-aproximação é um ponto fixo, a fórmula modal completa é satisfatível.

Principais Contribuições

1. Implementação do CEGARBox++: Uma nova implementação em C++ de tableaux-CEGAR que serve como baseline para os experimentos.
2. Algoritmo RECARTAB: Uma extensão sonora e completa de tableaux-CEGAR incorporando atalhos ESAT do tipo RECAR para tentar a minimização de modelos.
3. Integração CEGARBox++(KSP): A primeira integração efetiva de métodos de SAT, tableaux e resolução para satisfatibilidade modal. Utiliza o KSP não apenas como um parceiro de portfólio, mas como um oráculo interno para detectar pontos fixos e disparar a terminação antecipada para problemas satisfatíveis.
4. Análise Teórica: Provas formais de correção (soundness), completude e terminação para ambas as abordagens baseadas em RECAR e em Resolução.

Resultados Experimentais

Os autores avaliaram suas abordagens nos benchmarks padrão K (LWB-K, 3CNF e MQBF) usando uma CPU Intel i7-11700F.

• Desempenho RECAR: A abordagem RECARTAB (RECARBox) mostrou-se não competitiva. Geralmente, teve um desempenho pior que o CEGARBox++ padrão. Os autores atribuem isso ao overhead de buscar por modelos menores; se um modelo menor não existe ou é difícil de encontrar, o cálculo extra é desperdiçado.
• Desempenho Baseado em Resolução: O CEGARBox++(KSP) demonstrou desempenho superior:
  • Superou significativamente tanto o CEGARBox++ independente quanto o KSP independente nos benchmarks MQBF (que são dominados por problemas satisfatíveis).
  • Alcançou acelerações de até 100x em certas instâncias satisfatíveis comparado ao KSP sozinho.
  • Nos benchmarks 3CNF, teve desempenho equivalente ao CEGARBox++.
  • Nos benchmarks LWB-K, foi ligeiramente superado pelo próprio CEGARBox++, provavelmente devido ao overhead da geração da forma normal do KSP, que produz mais cláusulas para fórmulas massivas.
• Sinergia vs. Paralelismo: Os autores descartaram a possibilidade de os ganhos de desempenho serem meramente devidos ao paralelismo (dobra de recursos). O CEGARBox++(KSP) resolveu problemas satisfatíveis que o KSP sozinho não conseguiu, provando que o componente CEGAR contribuiu ativamente para a solução ao fornecer o contexto necessário ao provador de resolução ou ao podar o espaço de busca via detecção de ponto fixo.

Significância e Alegações

O artigo afirma que o CEGARBox++(KSP) representa a primeira integração efetiva de métodos de SAT, tableaux e resolução para satisfatibilidade modal que performa melhor que seus componentes individuais.

• Superação de Limitações: O trabalho aborda a fraqueza fundamental dos tableaux-CEGAR ao lidar com grandes problemas satisfatíveis, introduzindo um mecanismo para detectar quando um modelo existe sem construí-lo explicitamente.
• Forças Complementares: Os resultados destacam que, embora solvers baseados em SAT, tableaux e resolução tenham tradicionalmente sido métodos concorrentes com diferentes forças (ex: tableaux para insatisfatíveis, resolução para satisfatíveis), sua integração pode resultar em um solver que é "maior que a soma de suas partes".
• Perspectivas Futuras: Os autores observam modestamente que sua implementação atual é ingênua (usando E/S de arquivo para comunicação e a forma normal específica do KSP). Eles sugerem que uma integração mais polida, potencialmente usando a própria geração de forma normal do CEGAR e melhores protocolos de comunicação, poderia permitir que esta abordagem híbrida supere os solvers existentes em todos os conjuntos de benchmarks, incluindo os benchmarks LWB-K, onde atualmente fica ligeiramente atrás.

O artigo conclui que, embora a abordagem RECAR não tenha sido bem-sucedida neste contexto, a estratégia de detecção de ponto fixo usando um oráculo de resolução é uma direção promissora para algoritmos CEGAR recursivos, particularmente aqueles que envolvem ramificação.