Nombre limité d'occurrences variables dans le SAT 1 en 3

Existe-t-il un résultat connu sur la classe de complexité de 1-en-3-SAT avec un nombre restreint d'occurrences variables?

J'ai trouvé la réduction parcimonieuse suivante avec Peter Nightingale, mais je veux citer quelque chose si cela est connu.

Voici l'astuce que nous avons trouvée. Cela montre que 1-en-3-SAT limité à 3 occurrences par variable est NP complet et #P complet (puisque 1-en-3-SAT l'est) , tandis que 3-SAT limité à 3 occurrences est en P

Disons que nous avons plus de trois occurrences de x. Supposons que nous ayons besoin de 6. Ensuite, nous introduirons 5 nouvelles variables x2 à x6 équivalentes à x et deux nouvelles variables d1 et d2 garanties fausses avec les 6 nouvelles clauses suivantes:

x  -x2 d1
x2 -x3 d1
x3 -x4 d1
x4 -x5 d2
x5 -x6 d2
x6 -x  d2

Évidemment, nous remplaçons chaque occurrence de x après la première par xi pour certains i. Cela donne trois occurrences de chaque xi et d.

Ce qui précède définit chaque di à faux et tous les xi à la même valeur. Pour voir cela, x doit être vrai ou faux. Si c'est vrai, la première clause définit x2 true et d1 false, puis cela se propage dans les classes. Si x est faux, la dernière clause définit x6 false et d2 false et elle propage les clauses. C'est évidemment fortement parcimonieux donc préserve le comptage.

À ma connaissance, les "limites" actuelles ont été fixées:

Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer, Andreas Wotzlaw: XSAT et NAE-SAT des classes CNF linéaires. Mathématiques appliquées discrètes 167: 1-14 (2014)

Voir aussi la thèse de Schmidt: Complexité computationnelle de SAT, XSAT et NAE-SAT pour les formules CNF de Horn linéaires et mixtes

Théorème 29 . XSAT reste NP-complet pour - et - , .$k$$CNF^l_+$$k$$CNF^l$$k, l \geq 3$

(XSAT pour - est exactement 1-en-3-SAT où chaque variable apparaît exactement fois)$3$$CNF^3$$l=3$

Notez que le théorème prouve également l'exhaustivité NP du cas monotone plus fort ( )$CNF_+$

(Je comprends que cela doit être une réponse tardive; j'écris pour de futurs lecteurs)

Il y a un résultat toujours plus fort dans la littérature.

Cubic Planar Positive Positive 1-in-3 Satisfiability est prouvé NP-complet dans Moore and Robson, Hard Tiling Problems with Simple Tiles . (Ils disent «monotone» plutôt que «positif». Voir enfin la note ajoutée)

Le résultat mentionné est plus fort que le résultat de la thèse de Schmidt car ici le graphique de la formule est limité à être plan. (La condition est en fait plus forte: ils donnent un type particulier de plongement appelé plongement rectiligne)

Le graphe d'une formule booléenne est défini comme le graphe avec le jeu de sommets et le jeu de bords variable apparaît dans la clause (non niée ni niée) (où est l'ensemble des variables et est l'ensemble des clauses).$G_B$$B=(X,C)$$X\cup C$$E:= \{ x_iC_j\ :\ $$x_i$$C_j$$\}$$X$$C$

Instance de satisfaction cubique planaire positive 1 en 3 : une formule booléenne où est un ensemble de variables, un ensemble de sous-ensembles de 3 éléments sur (clauses), et le graphique de est un graphique planaire cubique. Question: Existe-t-il une affectation de vérité pour telle que chaque clause est a exactement une vraie variable?$B=(X,C)$$X$$C$$X$$G_B$$B$
$X$$C$

Notez que chaque clause contient exactement 3 variables distinctes et chaque variable apparaît dans exactement 3 clauses.

Voir la thèse de Tippenhauer sur le plan 3-SAT et ses variantes (2016) pour les variantes sat qui restreignent le nombre d'occurrences variables.
Remarque: il existe quelques variantes découvertes après la publication de cette thèse.

Note ajoutée: Le résultat de Moore et Robson a prouvé que la satisfaction positive cubique planaire 1 en 3 est NP-complète. (Autrement dit, la formule booléenne n'est pas seulement monotone, elle est positive (c.-à-d., Aucun littéral nié du tout)). Malheureusement, dans de nombreux premiers articles, le terme «monotone» était utilisé pour signifier «positif». La réduction de Moore et Robson n'introduit pas de littéraux niés. Leur réduction provient de la satisfaction planaire «monotone» 1-en-3 dans le papier de Laroche La satisfaction planaire 1-en-3 est NP-complète . Je n'ai pas pu obtenir ce document, mais très probablement Laroche voulait aussi dire positif en disant «monotone». Même s'il ne le pensait pas, nous pouvons utiliser la satisfaction planaire positive 1-en-3 de Mulzer et Rote ' comme problème source à la place.

Voir cette réponse pour une question dans cs.se