Si vous avez un algorithme de décision pour détecter s'il existe une validité affectation à 2-SAT, vous pouvez l'utiliser pour trouver l'affectation réelle.
Premier lancement de l'algorithme de décision 2-SAT sur l'ensemble de l'expression. Supposons qu'il indique qu'il existe une affectation valide. Maintenant, si x_1 est un littéral, assignez x_1 à 0. Maintenant, calculez le 2-SAT pour l'expression résultante (vous devrez assigner d'autres littéraux pour cette raison, par exemple si x_1 OU x_3 apparaît, vous aussi besoin de mettre x_3 à 1).
Si l'expresion résultant est 2-Satisfiable, alors vous pouvez prendre à 0 x 1, sinon prenez à 1. x 1
Maintenant, vous pouvez trouver cela sur chaque littéral.
Pour un algorithme plus efficace, je vous suggère d'utiliser l'approche du graphe d'implication.
Vous pouvez trouver plus d'informations ici: http://en.wikipedia.org/wiki/2-satisfiability
La partie pertinente:
une instance 2-satisfiabilité est résoluble si et seulement si chaque variable de l'instance appartient à un différent fortement composant connexe du graphique d'implication que la négation de la même variable. Depuis fortement composants connexes peuvent être trouvés dans temps linéaire par un algorithme basé sur profondeur de la première recherche, la même linéaire liée s'applique également à 2-satisfiability.
Les littéraux dans chaque composante fortement connexe sont soit tous égaux à zéro ou tout 1.
Le papier lié à montre comment résoudre les problèmes de flux de réseau par des appels répétés à 2-Sat – user108088
Je n'ai pas lu la papier, mais Wikipedia dit qu'il énumère un algorithme: "Feder (1994) décrit un algorithme pour répertorier efficacement toutes les solutions à une instance de 2-satisfiabilité donnée, et pour résoudre plusieurs problèmes connexes." –
@ user108088: L'article parle de résoudre 2Sat en utilisant le flux réseau. –