variations de SAT

J'ai recherché sur Internet, mais je n'ai trouvé aucune «grande liste» de variantes du problème SAT.

Mis à part le (commun)

• SAM,
• k-SAT,
• MAX-kSAT,
• Half-SAT,
• XOR-SAT,
• NAE-SAT

Quelles sont les autres variantes?

(cela sera également très utile si des classes de complexité sont données (si possible))

(Faire du commentaire une réponse comme demandé et développer un peu.)

"Un esprit curieux" devrait lire le théorème de dichotomie de Schaefer et la généralisation d' Allender et al. cela montre que chaque variante SAT possible est soit triviale, soit dans l'une des six classes de complexité bien connues:

1. NP-complet
2. P-complet
3. NL-complet
4. L-complet
5. ⊕L-complet
6. co-NLOGTIME

Cette liste sera très longue;) Voici quelques-unes de mes variantes préférées (NP-complètes) de SAT:

• PLANAIRE ( $\le 3, 3$ ) -SAT (chaque clause contient au moins deux et au plus trois littéraux, chaque variable apparaît dans exactement trois clauses; deux fois dans sa forme non niée, et une fois dans sa forme niée, et le graphique d'incidence bipartite est plan.)

  Voir: Dahlhaus, Johnson, Papadimitriou, Seymour, Yannakakis, La complexité des coupes multiterminales, SIAM Journal of Computing 23 (1994) 864-894

• 4S BOUNDED PLANAR 3-CONNECTED 3SAT (chaque clause contient exactement 3 variables distinctes, chaque variable apparaît dans au plus 4 clauses, le graphique incident bipatite est planaire et 3-connecté)

  Voir: Kratochvíl, Un problème de satisfiabilité planaire spécial et une conséquence de son exhaustivité NP, Discrete Applied Math. 52 (1994) 233-252

• MONOTONE CUBIC 1-IN-3SAT (MONOTONE-1-IN-3SAT dans lequel chaque variable apparaît exactement 3 fois)

  Voir: Moore et Robsen, Problème de pavage dur avec des carreaux simples, Calcul discret. Geom. 26 (2001) 573-590

• $k$$k$ .

  Voir cet article .

Du "côté NP-complet", je suis tombé sur ces variantes (j'ai aussi posé une question similaire sur cs.stackexchange):

• Planar 3-SAT;
• SAT plan 1 en 3 et SAT plan 1 en 3 positif (voir Mulzer et Rote );
• NAE 3-SAT;
• 2/2/4-SAT (voir Trouver une solution la plus courte pour l'extension NxN du 15-Puzzle est intraitable par D. Ratner et M. Warmuth (1986) );
• XSAT, NAE-SAT pour les formules linéaires monotones, XSAT pour les formules linéaires exactes (voir le beau travail d'Ewald Speckenmeyer sur les problèmes linéaires XSAT: Complexité computationnelle de SAT, XSAT et NAE-SAT pour les formules CNF Horn linéaires et mixtes );
• k-colorable Monotone NAE-3SAT (voir P Jain, On a variant of Monotone NAE-3SAT and the Triangle-Free Cut problem, 2010 ).

$\mathrm{SAT}(k)$$\mathrm{SAT}$$k$$\mathrm{SAT}(2)$$\mathsf{L}$$\mathrm{SAT}(k)$$k\geq 3$

Outre la liste ci-dessus, il existe également:

• #SAT: comptage de modèles
• All-SAT: modèle énumérant

Il existe un lien très classique entre la logique et l'algèbre, qui remonte à l'origine de la logique moderne et du travail de George Boole. Une formule en logique propositionnelle peut être interprétée comme un élément d'une algèbre booléenne. Les constantes logiques vrai et faux deviennent les notions algébriques de l'élément supérieur et inférieur d'un réseau. Les opérations logiques de conjonction, de disjonction et de négation deviendront les opérations algébriques de rencontre, de jonction et de complémentation dans l'algèbre booléenne. Ce lien est moins souligné dans les traitements modernes de la logique, mais il est particulièrement intéressant dans le contexte de votre question. L'algèbre nous permet de nous éloigner de nombreux détails spécifiques à un problème et de trouver des généralisations d'un problème qui s'appliqueront à de nombreuses situations différentes.

Dans le cas spécifique de SAT, la question algébrique que l'on peut se poser est de savoir ce qui se passe lorsque nous interprétons des formules en réseaux plus généraux que les algèbres de Boole. Du côté logique, vous pouvez généraliser le problème de satisfiabilité de la logique propositionnelle à la logique intuitionniste. Plus généralement, vous pouvez généraliser le problème de satisfiabilité propositionnelle à celui de déterminer si une formule, lorsqu'elle est interprétée sur un réseau borné (un avec top et botto), définit l'élément inférieur du réseau. Cette généralisation vous permet de traiter les problèmes dans l'analyse de programme comme des problèmes de satisfiabilité.

Une autre généralisation est celle de la logique du premier ordre sans quantificateur, où vous obtenez la question de la Modulo de Satisfaction d'une Théorie. Cela signifie qu'en plus d'avoir des variables booléennes, vous avez également des variables de premier ordre et des symboles de fonction et vous voulez savoir si une formule est satisfaisable. À ce stade, vous pouvez poser des questions sur les formules en arithmétique, les théories des chaînes ou des tableaux, etc. Nous obtenons donc une généralisation stricte et très utile de SAT qui a beaucoup d'applications dans les systèmes, la sécurité informatique, les langages de programmation, la vérification de programme, la planification , intelligence artificielle, etc.