Propriétés exprimables en 2-CNF ou 2-SAT

Comment montrer qu'une certaine propriété ne peut pas être exprimée en 2-CNF (2-SAT)? Existe-t-il des jeux, tels que des jeux de galets? Il semble que le jeu de galets noir classique et le jeu de galets noir et blanc ne conviennent pas à cela (ils sont complets sur PSPACE, selon Hertel et Pitassi, SIAM J of Computing, 2010).

Ou d'autres techniques que les jeux?

Edit : je pensais aux propriétés qui impliquent le comptage (ou la cardinalité) d'un prédicat inconnu ( prédicat SO , comme diraient les théoriciens des modèles finis). Par exemple, comme dans Clique ou Matching non pondéré. (a) Clique : Y a-t-il une clique dans le graphe donné telle que un nombre donné ? (b) Correspondance : Y a-t-il un correspondant dans tel que ? $C$ $G$ $|C| \ge$ $K$ $~$ $M$ $G$ $|M| \ge K$

Le 2-SAT peut-il compter? At-il un mécanisme de comptage? Semble douteux.

sat lower-bounds combinatorial-game-theory Sameer Gupta
la source

Je comprends qu'il existe un jeu Ehrenfeucht – Fraïssé (pour FO) et un jeu Ajtai-Fagin (pour SO monadique) dans la théorie des modèles finis. Mais je ne sais pas s'ils sont suffisants ici. De plus, les jeux dans FMT se compliquent avec des structures ordonnées, non?

Sameer Gupta

@Marzio, cela semble être une preuve que toutes les fonctions booléennes ne sont pas exprimables dans 2CNF, comme vous le dites, répondrait à la question (pas vraiment sûr de cela, ne le voyez pas comme évident). quelle est cette preuve? est-il publié quelque part?

vzn

@vzn: une fonction booléenne triviale qui n'est pas exprimable en 2-CNF est:

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

$(x_1 \lor x_2 \lor x_3)$

Marzio De Biasi

@SameerGupta: après la reformulation, la question devient difficile :-); en effet

, où

est limité aux clauses à deux variables (SO-Kroms) capture NL sur des structures ordonnées, tandis que la capture de SO existentielle NP. Évidemment limité à FO 2-SAT ne peut pas compter (et les techniques de jeu ou de compacité Ehrenfeucht – Fraïssé sont assez loin, car vous pouvez les utiliser pour prouver que PARITY n'est pas définissable FO).

\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

D'accord. il semble exister une théorie générale selon laquelle

-SAT ne peut pas exprimer toutes les fonctions booléennes pour la constante

. quelle est cette théorie? cette question concerne le cas spécial

. notons qu'il existe un concept de "réduction" de

-SAT en 3-SAT via la transformée de Tseitin . ont également vu un concept similaire apparaître dans les preuves de limites inférieures de circuit monotone (Razborov).

k

$k$

k

$k$

k = 2

$k=2$

n

$n$

vzn

Réponses:

Une famille de vecteurs de bits est la classe de solutions à un problème 2-SAT si et seulement si elle a la propriété médiane: si vous appliquez la fonction de majorité au niveau du bit à trois solutions, vous obtenez une autre solution. Voir par exemple https://en.wikipedia.org/wiki/Median_graph#2-satisfiability et ses références. Donc, si vous pouvez trouver trois solutions pour lesquelles ce n'est pas vrai, vous savez que cela ne peut pas être exprimé en 2-CNF.

David Eppstein
la source

David, merci, va chercher ça. @vzn - La réponse de David est-elle liée à ce que vous avez commenté il y a 2 jours sur le site de discussion, à savoir que les formules 3SAT existent pour tous les ensembles de vecteurs de bits et à la recherche d'un résultat pour les formules 2SAT concernant les ensembles de vecteurs à bits?

Sameer Gupta

David, Yuval - Certes, vos preuves fonctionneront si l'on utilise le même ensemble de variables. Mais que faire si l'ensemble des variables utilisées peut être complètement différent? Jetez un œil à la réponse de Martin Seymour ici: cstheory.stackexchange.com/questions/200/… - Pour montrer qu'il n'y a pas de réduction équi-satisfaisante (de préférence logspace) de K-Clique ou K-Matching à 2SAT, il faudrait une preuve différente . Pensées?

Sameer Gupta

Ajouter des variables auxiliaires puis les projeter n'aidera pas, car si la propriété médiane est vraie pour le système augmenté de variables, alors c'est toujours vrai dans la projection.

David Eppstein

Une autre façon de le dire est que la médiane (ou la majorité) est un polymorphisme pour les contraintes 2SAT. En fait, on sait que tout CSP (même non booléen) qui a la majorité comme polymorphisme est en

(Dalmau-Krokhin '08).

N L \subseteq P

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

arnab

$P(x_1,\ldots,x_n)$ $n$ $\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$

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$

φ = χ \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$

χ \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
la source

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$

(Oui, je connais ces fonctions de calcul d'addition, de multiplication et de comptage, mais il est facile de les convertir en versions décisionnelles de leurs problèmes respectifs.)

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

(c) Donc, pour le comptage , même si vous ne parvenez pas à obtenir une expression équivalente en 2-CNF, en utilisant la méthode décrite en (b), vous pouvez obtenir une expression 2-CNF équitable .

Alors oui, le 2-SAT peut compter.

$NL$ $|M|$ $NL$

Martin Seymour
la source

Concernant (c), si vous croyez ma réponse, une expression 2-CNF non satisfaisante peut être convertie en une expression 2-CNF équivalente de bonne foi.

Yuval Filmus

-

$-$

$~$

Vous pouvez lire ma réponse et voir par vous-même. Notez qu'il n'y a pas de limites de temps / espace dans ce cas.

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$

$~$