Propiedades expresables en 2-CNF o 2-SAT

¿Cómo se demuestra que una determinada propiedad no se puede expresar en 2-CNF (2-SAT)? ¿Hay algún juego, como los juegos de guijarros? Parece que el clásico juego de guijarros negros y el juego de guijarros blanco y negro no son adecuados para esto (son completos para PSPACE, según Hertel y Pitassi, SIAM J de Computing, 2010).

¿O alguna técnica distinta de los juegos?

Editar : Estaba pensando en propiedades que implican contar (o cardinalidad) de un predicado desconocido ( predicado SO , como dirían los teóricos de modelos finitos). Por ejemplo, como en Clique o Matching no ponderado. (a) Clique : ¿Hay una camarilla en el gráfico dado que algún número dado ? (b) Coincidencia : ¿Hay una coincidente en tal que ? $C$ $G$ $|C| \ge$ $K$ $~$ $M$ $G$ $|M| \ge K$

¿Puede contar 2-SAT? ¿Tiene un mecanismo de conteo? Parece dudoso

sat lower-bounds combinatorial-game-theory Sameer Gupta
fuente

Entiendo que hay un juego Ehrenfeucht – Fraïssé (para FO) y un juego Ajtai-Fagin (para SO monádico) en la teoría de modelos finitos. Pero no estoy seguro si son suficientes aquí. También los juegos en FMT se complican con estructuras ordenadas, ¿verdad?

Sameer Gupta

@Marzio parece una prueba de que no todas las funciones booleanas se pueden expresar en 2CNF, ya que usted respondería la pregunta (en realidad no estoy seguro de eso, no lo veo como obvio). ¿Cuál es esa prueba? ¿Se publica en alguna parte?

vzn

@vzn: una función booleana trivial que no es expresable en 2-CNF es:

(x_{1} \lor x_{2} \lor x_{3})

$(x_1 \lor x_2 \lor x_3)$

Marzio De Biasi

@SameerGupta: después de la reformulación, perhpas la pregunta se vuelve difícil :-); de hecho

, donde

se limita a las cláusulas con dos variables (SO-Krom) captura NL sobre ordenó estructuras, mientras que las capturas de SO existencial NP. Obviamente limitado a FO 2-SAT no puede contar (y el juego Ehrenfeucht – Fraïssé o las técnicas de compacidad son lo suficientemente grandes, porque puedes usarlas para demostrar que PARITY no es FO definible).

\exists P_{1} . . . \exists P_{n} \forall \bar{z} φ (P_{1}, . . ., P_{n}, \bar{z})

$\exists P_1...\exists P_n \forall \bar{z} \varphi( P_1,...,P_n, \bar{z})$

φ

$\varphi$

Marzio De Biasi

Okay. parece haber alguna teoría general de que

-SAT no puede expresar todas las funciones booleanas para

constante . ¿Cuál es esa teoría? Esta pregunta se refiere al caso especial

. tenga en cuenta que existe un concepto de "reducir"

-SAT a 3-SAT a través de la transformación Tseitin . También he visto aparecer un concepto similar en las pruebas de límites inferiores del circuito monótono (Razborov).

k

$k$

k

$k$

k = 2

$k=2$

n

$n$

vzn

Respuestas:

Una familia de vectores de bits es la clase de soluciones para un problema de 2-SAT si y solo si tiene la propiedad mediana: si aplica la función de mayoría de bits a cualquiera de las tres soluciones, obtiene otra solución. Ver, por ejemplo, https://en.wikipedia.org/wiki/Median_graph#2-satisfiability y sus referencias. Entonces, si puede encontrar tres soluciones para las cuales esto no es cierto, entonces sabe que no puede expresarse en 2-CNF.

David Eppstein
fuente

David, gracias, buscará esto. @vzn - ¿La respuesta de David está relacionada con lo que comentaste hace 2 días en el sitio de chat, que las fórmulas 3SAT existen para todos los conjuntos de vectores de bits, y buscando un resultado para las fórmulas 2SAT relacionadas con los conjuntos de vectores de bits?

Sameer Gupta

David, Yuval - Ciertamente, tus pruebas funcionarán si uno usa el mismo conjunto de variables. Pero, ¿qué pasa si el conjunto de variables utilizadas puede ser completamente diferente? Eche un vistazo a la respuesta de Martin Seymour aquí: cstheory.stackexchange.com/questions/200/… - Para demostrar que no hay una reducción equi-satisfactoria (preferiblemente espacio de registro) de K-Clique o K-Matching a 2SAT requeriría una prueba diferente . Pensamientos?

Sameer Gupta

Agregar variables auxiliares y luego proyectarlas no ayudará, porque si la propiedad mediana es verdadera para el sistema aumentado de variables, entonces todavía es cierto en la proyección.

David Eppstein

Otra forma de decirlo es que la mediana (o mayoría) es un polimorfismo para las restricciones 2SAT. De hecho, se sabe que cualquier CSP (incluso no booleano) que tenga mayoría como polimorfismo está en

(Dalmau-Krokhin '08).

N L \subseteq P

$\mathsf{NL} \subseteq \mathsf{P}$

arnab

Sea una propiedad de variables. Suponga que hay una fórmula 2CNF tal que $P(x_1,\ldots,x_n)$ $n$ $\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$ Afirmamos que es equivalente a una fórmula 2CNF involucra solo . Para probar esto, es suficiente mostrar cómo eliminar . Escribe

P (x_{1}, \dots, x_{n}) \Leftrightarrow \exists y_{1} \dots \exists y_{m} φ (x_{1}, \dots, x_{n}, y_{1}, \dots, y_{m}) .

$P(x_1,\ldots,x_n) \Leftrightarrow \exists y_1 \cdots \exists y_m \varphi(x_1,\ldots,x_n,y_1,\ldots,y_m).$

φ

$\varphi$

ψ

$\psi$

x_{1}, \dots, x_{n}

$x_1,\ldots,x_n$

y_{m}

$y_m$

donde

son literales y

no involucra a

. La fórmula

es equivalente a

φ = χ \land ⋀_{k = 1}^{s} (y_{m} \lor U_{k}) \land ⋀_{ℓ = 1}^{t} (\bar{y_{m}} \lor V_{ℓ}),

$\varphi = \chi \land \bigwedge_{k=1}^s (y_m \lor U_k) \land \bigwedge_{\ell=1}^t (\overline{y_m} \lor V_\ell),$

U_{k}, V_{ℓ}

$U_k,V_\ell$

χ

$\chi$

y_{m}

$y_m$

φ

$\varphi$

Esto prueba la afirmación cuando

no aparece en una cláusula unitaria; si lo hace, podemos eliminarlo directamente.

χ \land (\bar{y_{m}} \Rightarrow ⋀_{k = 1}^{s} U_{k}) \land (y_{m} \Rightarrow ⋀_{ℓ = 1}^{t} V_{ℓ}) ⟺ χ \land (⋀_{k = 1}^{s} U_{k} \lor ⋀_{ℓ = 1}^{t} V_{ℓ}) ⟺ χ \land ⋀_{k = 1}^{s} ⋀_{ℓ = 1}^{t} (U_{k} \lor V_{ℓ})

$\chi \land (\overline{y_m} \Rightarrow \bigwedge_{k=1}^s U_k) \land (y_m \Rightarrow \bigwedge_{\ell=1}^t V_\ell) \\ \Longleftrightarrow \\ \chi \land (\bigwedge_{k=1}^s U_k \lor \bigwedge_{\ell=1}^t V_\ell) \\ \Longleftrightarrow \\ \chi \land \bigwedge_{k=1}^s \bigwedge_{\ell=1}^t (U_k \lor V_\ell)$

y_{m}

$y_m$

$P(x_1,\ldots,x_n)$ $\psi(x_1,\ldots,x_n)$ $P$ $P$ $K$ $K$ $n$

Yuval Filmus
fuente

y_{i}

$y_i$

ψ

$\psi$

x_{1}

$x_1$

x_{2}

$x_2$

\dots

$\cdots$

x_{n}

$x_n$

ϕ_{1}

$\phi_1$

ϕ_{2}

$\phi_2$

ϕ_{2}

$\phi_2$

y_{i}

$y_i$

y_{i}

$y_i$

$L$ $-$ $L$

(Sí, sé que las funciones de cálculo de suma, multiplicación y conteo, pero es fácil convertirlas en versiones de decisión de sus respectivos problemas).

$L \subseteq NL$ $NL$ $AC^0$ $AC^0$

(c) Por lo tanto, para contar , aunque no pueda obtener una expresión equivalente en 2-CNF, utilizando el método descrito en (b), puede obtener una expresión de 2-CNF equisatisfactable .

Entonces sí, 2-SAT puede contar.

$NL$ $|M|$ $NL$

Martin Seymour
fuente

Re (c), si cree en mi respuesta, una expresión equisatisfactable de 2-CNF puede convertirse en una expresión de 2-CNF de buena fe equivalente.

Yuval Filmus

-

$-$

$~$

Puedes leer mi respuesta y ver por ti mismo. Tenga en cuenta que no hay límites de tiempo / espacio en este caso.

Yuval Filmus

L

$L$

{A C}^{0}

$\mathrm{AC}^0$

f

$f$

x \in L

$x\in L$

f (x)

$f(x)$

ϕ

$\phi$

x_{i}

$x_i$

ϕ

$\phi$

-

$-$

x_{i}

$x_i$

$~$