Resumen

Presentamos un solucionador novedoso para resolver el problema de las fórmulas booleanas cuantificadas (QBF). Con el fin de mejorar el rendimiento, introducimos algunas reglas de razonamiento en el algoritmo de paso de mensajes para resolver QBF. Al preprocesar las fórmulas, el solucionador incorpora la reducción de igualdad y la resolución hiperbinaria. Además, el solucionador emplea el método de paso de mensajes para obtener más información a la hora de seleccionar ramas. Mediante la propagación de unidades, el aprendizaje basado en conflictos y la implicación y el aprendizaje dirigidos a la satisfacción, el solucionador gestiona las ramas. Los resultados experimentales también muestran que el solucionador puede resolver eficientemente el problema QBF.

• Materias:Análisis Matemático Álgebra Ingeniería Matemática aplicada Lógica matemática
• Subjects:Mathematical Analysis Algebra Engineering Applied Mathematics Mathematical logic
• Palabras claves:solucionador, problema de fórmulas booleanas, qbf, ramas, aprendizaje, mensaje, problema qbf, reducción de igualdad, resultados experimentales, resolución hiperbinaria
• Keywords:solver, boolean formulae problem, qbf, branches, learning, message, qbf problem, equality reduction, experimental results, hyperbinary resolution