Un théorème de somme directe pour la complexité de l'espace de la clause Resolution?

La résolution est un schéma pour prouver l'insatisfiabilité des CNF. Une preuve en résolution est une déduction logique de la clause vide pour les clauses initiales du CNF. En particulier, toute clause initiale peut être déduite, et de deux clauses $A \lor x$ et la clause peut également être déduite. Une réfutation est une séquence de déductions qui se termine par une clause vide. $B \lor \neg{x}$ $A \lor B$

Si une telle réfutation est implémentée, nous pouvons envisager une procédure qui garde certaines clauses en mémoire. Dans le cas où une clause non initiale doit être utilisée à nouveau et qu'elle n'est plus en mémoire, l'algorithme doit la refaire à partir de zéro ou de celles en mémoire.

Soit le plus petit nombre de clauses à conserver en mémoire pour atteindre les clauses vides. On appelle cela l' espace clause complexité de . Nous disons que est est satisfiable. $Sp(F)$ $F$ $Sp(F)=\infty$ $F$

Le problème que je suggère est le suivant: considérez deux CNF et , et laissez le CNF $A=\bigwedge_{i=1}^m A_i$ $B=\bigwedge_{j=1}^n B_j$

A \lor B = ⋀_{i = 1}^{m} ⋀_{j = 1}^{n} A_{i} \lor B_{j}

$A \lor B = \bigwedge_{i=1}^m \bigwedge_{j=1}^n A_i \lor B_j$

Quelle est la relation de avec et ? $Sp(A \lor B)$ $Sp(A)$ $Sp(B)$

La borne supérieure évidente est . C'est serré? $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$

cc.complexity-theory lo.logic proof-complexity proof-search MassimoLauria
la source

Bonne question! Connaissez-vous la réponse à la taille de la somme directe? Je suppose que le pire des cas est lorsque les A et B n'ont pas de variables partagées. Un cas intéressant pourrait être lorsque A et B sont les mêmes jusqu'à renommer la variable. Btw, je ne vois pas comment vous obtenez cette limite supérieure, c'est comme si cela pouvait être bien pire.

Kaveh

Je vois maintenant la limite supérieure, vous pouvez copier la réfutation de pour pour pour obtenir un par un pour chaque , puis faire la réfutation pour . La taille sera d'environ .

B

$B$

A_{i} \lor B_{j}

$A_i \lor B_j$

1 \leq j \leq n

$1 \leq j \leq n$

A_{i}

$A_i$

1 \leq i \leq m

$1 \leq i \leq m$

A

$A$

m . (S i z e (B) + O (1)) + S i z e (A)

$m.(Size(B)+O(1))+Size(A)$

Kaveh

Tu as raison. J'ai oublié de le mentionner, mais bien sûr, le cas le plus intéressant en termes de borne inférieure est lorsque A et B ne partagent pas de variables. C'est exactement le cas , je suis vraiment intéressé par. Compte tenu de différents A et B vaut mieux obtenir un résultat inductivement pour

où

sont des copies variables disjoints du même

F_{1} \lor F_{2} \lor \dots F_{k}

$F_1 \lor F_2 \lor \ldots F_k$

F_{i}

$F_i$

F

$F$

MassimoLauria

Notez qu'en ce qui concerne la longueur de réfutation, vous avez facilement

L e n g t h (A \lor B) \leq L e n g t h (B) | A | + L e n g t h (A)

$Length(A \lor B) \leq Length(B)|A|+Length(A)$

MassimoLauria

La borne supérieure de l'espace trivial nécessite en fait une clause de moins en mémoire. J'ai édité en conséquence.

MassimoLauria

Réponses:

Je voulais poster ceci en tant que commentaire, mais comme je ne sais pas vraiment comment le faire, je suppose que ce sera plutôt une "réponse".

Je suis d'accord que la question est agréable. Bien sûr, la même question peut également être posée sur la durée des réfutations de résolution (c'est-à-dire le nombre de clauses se produisant dans la réfutation, compté avec des répétitions) et la largeur de la réfutation (c'est-à-dire la taille ou le nombre de littéraux se produisant dans , la plus grande clause de la réfutation).

Dans tous ces cas, il existe des limites supérieures "évidentes", mais il n'est pas clair pour moi si l'on doit s'attendre à ce que les limites inférieures correspondent ou non. Par conséquent, je voulais ajouter une question et un commentaire.

La question concerne la durée de réfutation. Il semble raisonnable de croire que la limite de longueur indiquée dans le commentaire de Massimo est serrée, mais le savons-nous?

$A$ $B_i$ $w_A$ $B$ $B$ $w_B$ $\max (w_A, w_B)$

C'est bien sûr une observation facile, mais le fait est que cela pourrait indiquer que la question de l'espace pourrait être délicate. Il en est ainsi puisque presque toutes les bornes inférieures de l'espace en réfutation que nous connaissons passent par des bornes inférieures de largeur. (C'est-à-dire que les limites inférieures de l'espace ont été dérivées indépendamment, mais avec le recul, elles suivent toutes comme corollaire du magnifique document "A Combinatorial Characterization of Resolution Width" d'Atserias et Dalmau.) Mais s'il existe un théorème de somme directe pour la clause de résolution l'espace, il ne suivra pas les limites inférieures de largeur mais doit être argumenté directement, ce qui au moins jusqu'à présent a semblé être beaucoup plus difficile. Mais bien sûr, il pourrait y avoir un argument simple selon lequel je manque.

Jakob Nordstrom
la source

Bienvenue, Jakob!

arnab

Les commentaires sont malheureusement limités aux personnes ayant une réputation d'au moins 50 - c'est une bizarrerie du logiciel et concerne la prévention du spam. Je suis sûr que vous franchirez rapidement ce seuil.

Suresh Venkat

Salut Jakob, je suis ravi de vous voir ici. (ps: je pense que vous avez franchi le seuil.)

Kaveh

Bonjour Jakob, je me demande si ce genre de déclaration a des conséquences sur les compromis. En tant que technique de limite inférieure, ce ne serait pas un outil très puissant: la longueur de la formule au carré tandis que l'espace augmente linéairement. Quoi qu'il en soit, cette propriété pourrait conduire à une formule avec une petite largeur et un grand espace (notez que la largeur augmente également si un nombre non constant de répétitions est effectué).

MassimoLauria