PLANEJAMENTO COMO SATISFATIBILIDADE DE FÓRMULAS HORN-MISTAS
Ao longo da última década, houveram diversas melhorias no desempenho dos resolvedores de Satisfabilidade Booleana (SAT), mas poucos trabalhos em Planejamento como Satisfabilidade exploraram essas novas estratégias. Este artigo explora uma nova maneira de modelar uma instância de planejamento do BLACKBOX e SATPLAN06. Esta nova abordagem é transformar a codificação padrão em uma fórmula Horn-Mista (MHF), que pode ser separada como uma conjunção de uma fórmula de Horn e uma fórmula 2-CNF. A complexidade teórica para resolver uma MHF é . A complexidade teórica da MHF combinada com as melhorias dos resolvedores SAT leva a uma abordagem promissora, conforme observamos nos benchmarks, quando comparada com a formulação padrão utilizando os mesmos resolvedores SAT
PLANEJAMENTO COMO SATISFATIBILIDADE DE FÓRMULAS HORN-MISTAS
-
DOI: 10.22533/at.ed.4302130091
-
Palavras-chave: Planejamento, Satisfatibilidade, Fórmula Horn-Mista, Satplan
-
Keywords: Planning, Satisfiability, Mixed-horn formula, Satplan
-
Abstract:
Over the course of the last decade, there have been several improvements in the performance of Boolean Satisfiability (SAT) but just a few works focused on Planning as Satisfiability recently. This paper explores a new way to model a planning instance from BLACKBOX and SATPLAN06. This new approach is a mixed-horn formula (MHF) where it can be seen as a conjunction of a Horn formula and a 2-CNF formula. The theoretical complexity to solve an MHF is . With the theoretical complexity combined with improvements of SAT solvers, it is a promising approach to model Planning as Mixed-Horn Formulas Satisfiability. It is observed that this formulation has some improvements with current state-of-the-art SAT solvers.
-
Número de páginas: 19
- Bruno César Ribas
- Razer Anthom Nizer Rojas Montaño
