Réduction directe SAT à 3-SAT

Ici, l'objectif est de réduire un problème SAT arbitraire à 3-SAT en temps polynomial en utilisant le moins de clauses et de variables. Ma question est motivée par la curiosité. Moins formellement, j'aimerais savoir: "Quelle est la réduction" la plus naturelle "du SAT au 3-SAT?"

Maintenant, la réduction que j'ai toujours vue dans les manuels se présente comme suit:

1. Prenez d'abord votre instance de SAT et appliquez le théorème de Cook-Levin pour le réduire au circuit SAT.

2. Ensuite, vous terminez le travail par la réduction standard du circuit SAT en 3-SAT en remplaçant les portes par des clauses.

Bien que cela fonctionne, les clauses 3-SAT résultantes finissent par ne ressembler presque pas aux clauses SAT avec lesquelles vous avez commencé, en raison de l'application initiale du théorème de Cook-Levin.

Quelqu'un peut-il voir comment faire la réduction plus directement, en sautant l'étape du circuit intermédiaire et en passant directement à 3-SAT? Je serais même satisfait d'une réduction directe du cas particulier de n-SAT.

(Je suppose qu'il y a des compromis entre le temps de calcul et la taille de la sortie. De toute évidence, une solution dégénérée - bien que heureusement inadmissible à moins que P = NP - serait de simplement résoudre le problème SAT, puis d'émettre un trivial 3 -Instance SAM ...)

EDIT: Sur la base de la réponse de Ratchet, il est clair maintenant que la réduction en n-SAT est quelque peu triviale (et que j'aurais vraiment dû y penser un peu plus attentivement avant de poster). Je laisse cette question ouverte un peu au cas où quelqu'un connaît la réponse à la situation plus générale, sinon j'accepterai simplement la réponse de Ratchet.

Chaque clause SAT a 1, 2, 3 variables ou plus. La clause 3 variables peut être copiée sans problème

Les clauses variables 1 et 2 {a1}et {a1,a2}peuvent être étendues à {a1,a1,a1}et {a1,a2,a1}respectivement.

La clause avec plus de 3 variables {a1,a2,a3,a4,a5}peut être étendue à {a1,a2,s1}{!s1,a3,s2}{!s2,a4,a5}avec s1et de s2nouvelles variables dont la valeur dépendra de la variable de la clause d'origine qui est vraie

$n'$$n$

Si vous avez besoin d'une réduction de k-SAT à 3-SAT, la réponse de cliquet fonctionne très bien.

Si vous voulez une réduction directe de la formule propositionnelle générique à CNF (et à 3-SAT), alors - du moins du point de vue des "solveurs SAT" - je pense que la réponse à votre question Quelle est la réduction "la plus naturelle" ... ? , c'est: Il n'y a pas de réduction «naturelle» !.

D'après les conclusions du chapitre 2 - "Encodages CNF" du (très bon) livre: Manuel de satisfaction :

...
Il existe généralement de nombreuses façons de modéliser un problème donné dans CNF, et peu de directives sont connues pour en choisir un. Il existe souvent un choix de caractéristiques du problème à modéliser en tant que variables, et certaines pourraient prendre beaucoup de temps à découvrir. Les codages de la tséitine sont compacts et mécanisables mais dans la pratique ne conduisent pas toujours au meilleur modèle, et certaines sous-formules pourraient être mieux développées. Certaines clauses peuvent être omises par des considérations de polarité et des clauses implicites de rupture de symétrie ou bloquées peuvent être ajoutées. Différents codages peuvent avoir différents avantages et inconvénients tels que la taille ou la densité de solution, et ce qui est un avantage pour un solveur SAT peut être un inconvénient pour un autre. Bref, la modélisation CNF est un art et il faut souvent procéder par intuition et expérimentation.
...

L'algorithme le plus connu est l' algorithme de Tseitin (G. Tseitin. Sur la complexité de la dérivation dans le calcul propositionnel. Automation of Reasoning: Classical Papers in Computational Logic, 2: 466–483, 1983. Springer-Verlag.)

Pour une bonne introduction aux encodages CNF, lisez le livre suggéré Manuel de satisfaction . Vous pouvez également lire quelques travaux récents et consulter les références; par exemple:

• P. Jackson et D. Sheridan. Clauses de conversion de forme pour les circuits booléens. Dans HH Hoos et DG Mitchell, éditeurs, Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004 , volume 3542 of LNCS, pages 183–198. Springer, 2004. (qui vise à réduire le nombre de clauses)
• P. Manolios, D. Vroon, Conversion de circuit efficace en CNF. Dans Théorie et applications des tests de satisfaction - SAT 2007 (2007), pp. 4-9

Permettez-moi de poster une autre solution similaire à Ratchel mais quelque peu différente. Ceci est directement tiré du chapitre 9 de la 2e édition du "The Algorithm Design Manual" de Steven Skiena

• Si la clause n'a qu'un seul littéral C = {z1}, créez deux nouvelles variables v1 et v2 et quatre nouvelles clauses à 3 littéraux: {v1, v2, z1}, {! V1, v2, z1}, {v1,! v2, z1} et {! v1,! v2, z1}. Notez que la seule façon dont les quatre clauses peuvent être satisfaites simultanément est si z1 = T, ce qui signifie également que le C d'origine sera satisfait
• Si la clause a deux littéraux, C = {z1, z2}, créez une nouvelle variable v1 et deux nouvelles clauses: {v1, z1, z2} et {! V1, z1, z2}. Encore une fois, la seule façon de satisfaire à ces deux clauses est d'avoir au moins un de z1 et z2 vrai, satisfaisant ainsi C
• Si la clause a trois littéraux, C = {z1, z2, z3}, copiez simplement C dans l'instance 3-SAT sans changement
• Si la clause a plus de 3 littéraux C = {z1, z2, ..., zn}, alors créez n-3 nouvelles variables et n-2 nouvelles clauses dans une chaîne, où pour 2 <= j <= n-2 , Cij = {v1, j-1, zj + 1,! Vi, j}, Ci1 = {z1, z2,! Vi, 1} et Ci, n-2 = {vi, n-3, zn-1, zn}