Imaginemos que tenemos una fórmula satisfactoria El problema a resolver es "¿Hay una asignación para las variables que hará F insatisfactorio? ". Una forma de resolver es encontrar todas las soluciones para F en términos de variables y si el recuento es < , la solución que falta será la respuesta, pero la complejidad de este algoritmo es enorme, si El número de tales asignaciones es pequeño.
Mis preguntas son:
- ¿Hay alguna manera de resolver el problema con menos llamadas de solucionador SAT?
- ¿Es un problema bien conocido en teoría (lo que debería googlear para leer sobre él)?
logic
satisfiability
sat-solvers
Grigor Aghanyan
fuente
fuente
Respuestas:
Su problema es el problema canónico -completo: Como tal, se cree que es más difícil que SAT (que es ). Resolverlo con unas pocas llamadas al oráculo SAT es similar a resolver el SAT de manera eficiente (la pregunta P vs. NP), aunque podría ser que mientras , por lo que en cierto sentido Hay más esperanza para su problema que para el SAT mismo.ΣP2
fuente
Este es un problema bien conocido: es el problema 2QBF. Desafortunadamente, es significativamente más difícil que el SAT. Hay solucionadores QBF disponibles. Puede intentar encontrar un solucionador QBF (o, mejor aún, un solucionador 2QBF) y ver si puede resolver su fórmula. Sin embargo, los solucionadores QBF no escalan tan bien como los solucionadores SAT; QBF es significativamente más difícil que SAT.
Consulte https://cstheory.stackexchange.com/q/11022/5038 y http://www.qbflib.org/ para obtener algunos recursos que pueden ser útiles.
fuente