Puntos de referencia únicos

16

Esta pregunta probablemente esté en el límite entre el tema y fuera del tema, sin embargo, he visto preguntas similares aquí, por lo tanto, lo haré.


Estoy implementando un solucionador Unique -SAT, cuya entrada es una fórmula -CNF que tiene como máximo asignación satisfactoria. Para probar su comportamiento práctico, necesito un conjunto de tales fórmulas. Los busqué en la web y no encontré nada (mientras que, por otro lado, es muy fácil encontrar conjuntos de fórmulas ordinarias CNF).kk1k

¿Dónde puedo encontrar instancias únicas de -SAT?k

Alternativamente, me contentaría también con conocer cualquier procedimiento para generar instancias satisfactoriamente únicas. El único enfoque que conozco es bajo el nombre de generación de instancias SAT plantadas : genera aleatoriamente una asignación de variables, luego genera solo aquellas cláusulas que coinciden con dicha asignación. Este enfoque no es satisfactorio para mis propósitos, por las siguientes razones:n

  • La fórmula obtenida puede tener otras tareas satisfactorias no deseadas.
  • Para asegurarse de que la fórmula se satisface de manera única con la asignación deseada, debe introducir todas las cláusulas posibles que estén de acuerdo con ella. Esto produciría fórmulas con demasiadas cláusulas, que probablemente serán fáciles de resolver y, por lo tanto, no representativas del peor de los casos del solucionador. No es obvio para mí cómo podemos forzar eficientemente la unicidad mientras mantenemos razonable el número de cláusulas.

¿Cómo podemos generar fórmulas únicas y satisfactorias con un número razonable de cláusulas? Por razonable me refiero lejos del máximo 2k(nk) .

Giorgio Camerani
fuente
Dada una fórmula SAT con variables y cláusulas. Si el número de cláusulas está entre y entonces la fórmula es satisfactoria o no satisfactoria. .. También elaboré las ecuaciones para k-SAT. Te lo haré saber si lo encuentro. n m 3 n - 2 n 3 n - 2 n - 2 n - 1 FFnm3n2n3n2n2n1F
Tayfun paga el
Si tiene suficiente tiempo libre (y las instancias son lo suficientemente pequeñas), puede generar instancias en la transición de fase y probarlas con un solucionador SAT. Si una fórmula no tiene solución, deséchela. Si tiene una solución X, agregue una cláusula que insista en que la solución no es X y ejecute el solucionador nuevamente. Esto es básico pero lento.
Andrew D. King

Respuestas:

7

Aquí hay una forma de generar una instancia Unique -SAT, dada una instancia SAT que usted sabe que es satisfactoria. Considere la fórmula dada porφ ψ ( x )kφψ(x)

φ(x)h(x)=y,

donde es una función hash que asigna una asignación a un valor de bits (para algún valor pequeño de ), e es un valor aleatorio de bits. Si tiene alrededor de asignaciones satisfactorias, entonces (heurísticamente) asumimos que tendrá exactamente una asignación satisfactoria (con probabilidad constante). Podemos probar si este es el caso usando un solucionador SAT (es decir, probar si es satisfactoria; si lo es, y es una asignación satisfactoria, probar si es satisfactoria). Six k k y k φ 2 k ψ ψ x 0 ψ ( x ) x x 0 k k k = 1 , 2 , , n n xhxkkykφ2kψψx0ψ(x)xx0kno se conoce, puede encontrar utilizando la búsqueda binaria o simplemente iterando sobre cada valor candidato (donde es el número de variables booleanas en ).kk=1,2,,nnx

Puede elegir la función hash libremente. Probablemente quieras hacerlo lo más simple posible. Una construcción extremadamente simple es hacer que seleccione un subconjunto aleatorio de bits de . Una construcción un poco más sofisticada es hacer que el ésimo bit de sea ​​el xor de dos bits elegidos al azar de (eligiendo un par separado de posiciones de bit para cada , independientemente). Mantener simple mantendrá relativamente simple.k x i h ( x ) x i h ψhkxih(x)xihψ

Este tipo de transformación a veces se usa / sugiere, como parte de un esquema para estimar el número de asignaciones satisfactorias a una fórmula ; Lo he adaptado a tu necesidad particular.φ

Puede encontrar muchos bancos de pruebas de instancias SAT en Internet, y puede aplicar esta transformación a todos ellos, para obtener una colección de instancias Unique -SAT.k


Otra posibilidad sería generar instancias únicas de -SAT a partir de la criptografía. Por ejemplo, supongamos que es una permutación unidireccional criptográfica. Sea un elemento elegido aleatoriamente de , y sea . Entonces la fórmula dada por es una instancia -SAT única . Como otro ejemplo, elija dos números primos grandes al azar, y deje . Entonces la fórmula dada porkf:{0,1}n{0,1}nx{0,1}ny=f(x)φ(x)f(x)=ykp,qn=pqφ(x,y)xy=nx>1y>1xy(con la correspondencia obvia entre cadenas de bits y enteros) es una instancia -SAT única . Sin embargo, estas construcciones no parecen ser una forma útil de comparar u optimizar su solucionador. Todos tienen una estructura especial, y no hay razón para creer que esta estructura sea representativa de problemas del mundo real. En particular, se sabe que las instancias SAT extraídas de problemas criptográficos son extremadamente difíciles, mucho más difíciles que las instancias SAT extraídas de muchas otras aplicaciones del mundo real de solucionadores SAT, por lo que no son una muy buena base para comparar su solucionador.k


En general, todas las técnicas mencionadas en esta respuesta tienen el inconveniente de que generan instancias Unique -SAT con una estructura particular, por lo que pueden no ser lo que está buscando, o, al menos, es posible que no desee confiar únicamente sobre fórmulas generadas de esta manera. Un mejor enfoque sería identificar aplicaciones de Unique k -SAT (¿quién cree que va a usar su solucionador y con qué propósito?), Y luego tratar de obtener algunos ejemplos realistas de esos dominios de aplicación.kk

Para un tema relacionado, vea también Generar interesantes problemas de optimización combinatoria

DW
fuente
La primera parte de su párrafo criptográfico es incorrecta, ya que (si existen funciones unidireccionales entonces) existen funciones unidireccionales que no son inyectivas.
Gracias, @RickyDemer! Me refería a la permutación unidireccional, pero eso no fue lo que escribí. Fijo.
DW
6

Puede considerar los algoritmos que se usan para generar rompecabezas de Sudoku, presumiblemente generalizados a , ya que (generalmente) se supone que los rompecabezas de Sudoku tienen una solución única. Por otro lado, los rompecabezas de Sudoku son también por lo general garantizada a tener al menos una solución ... Pero encontrar una solución que todavía podría ser un buen punto de referencia para su solucionador.n×n

Puede usar un generador de Sudoku junto con una reducción a SAT, o puede pensar en cómo aplicar las técnicas utilizadas en la generación de Sudoku para generar más directamente instancias únicas de SAT. Para el primero, obviamente, sus instancias SAT tendrán cierta estructura, pero no me queda claro si es más o menos estructura que, por ejemplo, plantar una solución o utilizar la técnica de aislamiento de testigos. Probablemente depende de sus necesidades y su solucionador.

La única referencia que conozco aquí es: Sudoku Puzzles Generating: de Easy a Evil .

Joshua Grochow
fuente
4

Creo que un buen caso de prueba sería generar instancias aleatorias y únicas de 3XOR (instancias plantadas) con restricciones y luego convertirlas en instancias 3SAT.Θ(n)

Ryan O'Donnell
fuente
2

En mi opinión, una de las mejores formas de crear instancias SAT "presumiblemente duras" mientras se controla el número de soluciones es a partir de instancias / circuitos de factorización enteros codificados en binario. el código no es muy complejo, utiliza principalmente circuitos de adición EE y no conduce a instancias SAT "grandes". el número de soluciones es igual al número de factores (incluidas las "permutaciones" de los factores). por lo tanto, los números primos generan exactamente dos soluciones, . se puede garantizar una única solución con una restricción adicional de "comparación" que restringe los factores a un <(1,p),(p,1)a<ba1 .bp

También con este enfoque es relativamente fácil encontrar números con aproximadamente todos los factores / soluciones que se deseen. cuanto más "suave" sea el número, más factores.

Varios investigadores a lo largo de los años han creado este código SAT de factorización (por ejemplo, para la competencia / arcada DIMACS que ha almacenado algunas instancias de factorización en el pasado) pero desafortunadamente no parece haber una versión disponible públicamente. vea también el primer enlace a continuación para una referencia donde el código fue escrito / implementado aparentemente para un curso de posgrado.

Otro enfoque empírico / iterativo que puede ser útil para algunos, para crear más instancias "no estructuradas": crear instancias SAT aleatorias cerca del punto de transición (la región donde la ecuación tiene una probabilidad del 50% entre "solucionable e insoluble"), y luego resuelve la ecuación. Si no tiene solución, bótelo y reinicie. si es solucionable, agregue cláusulas que restrinjan la solución "no" como la solución encontrada, obteniendo e n + 1 , y resuelva. repita si es necesario. cuando la ecuación e n + 1 ya no es solucionable, el e n debe haber tenido una solución única / única.enen+1en+1en

vzn
fuente
Mencioné el enfoque de factorización en mi respuesta anteriormente, pero también expliqué por qué podría no ser un banco de pruebas ideal: "Sin embargo, estas construcciones no parecen ser una forma útil de comparar u optimizar su solucionador. Todas tienen una estructura especial, y no hay razón para creer que esta estructura sea representativa de problemas del mundo real. En particular, se sabe que las instancias de SAT extraídas de problemas criptográficos son extremadamente difíciles, mucho más difíciles que las instancias de SAT extraídas de muchas otras aplicaciones de solucionadores de SAT del mundo real, por lo que no son una muy buena base para evaluar su solucionador ".
DW
así que lo anterior es un punto de vista diferente que si uno quiere instancias muy difíciles, obviamente un caso de prueba natural para cualquier solucionador, entonces el factoring es de hecho un camino prometedor. dudo seriamente que pueda encontrar alguna opinión publicada que refleje la suya Para repetir, los investigadores serios han puesto instancias de factorización en los archivos de desafío DIMACS desde hace muchos años. de todos modos, tu opinión contraria ni siquiera se expresa de manera coherente. la criptografía es un problema principal / aplicado en el mundo real, incluso más que muchos problemas abstractos / abstractos / académicos utilizados para las instancias de SAT ...
vzn
2

Puede generar fácilmente directamente fórmulas SAT únicas con un tamaño razonable (|F|<n+2k)

Sea el modelo único; digamos que m contiene solo "0" s (cambie el nombre de las variables más adelante si es necesario). Sea F una fórmula k -SAT satisfecha solo por m : el tamaño máximo de F es el número total de cláusulas satisfechas por m es decir ( 2 k - 1 ) ( nmm
FkmFm .(2k1)(nk)

Toma la (k1)x1,x2xk
(¬x1,x2xk)(x1,¬x2xk)(x1,x2¬xk)

Toma la ((k2)x1,x2xk
(¬x1,¬x2,x3xk)(¬x1,x2,¬x3xk)(x1,x2¬xk1¬xk)

(kk)x1,x2xk

x1,x2xkmnkxi(k<in)0k1x1,x2xk
(¬xk+1,x1,xk1)(¬xn,x1xk1)

|F|=i=1k(ki)+nk=2k1+nk

k

Xavier Labouze
fuente
Hay un problema en su respuesta: tenemos n variables y esto significa que y no k
Elaqqad