2SAT

RNO-Wiki

Opis problemu

2SAT to problem spełnialności formuł postaci 2CNF. Na przykład 

 (x0 v x1) ^ (x1 v NOT(x2)) ^ (NOT(x1) v x0) ^ (x2 v NOT(x3)) ^ (x0 v x3) ^ (NOT(x0) v NOT(x1)) ^ (x3 v NOT(x2))

Na pierwszy rzut oka nie jest łatwo odpowiedzieć, czy da się tak podstawić wartości logiczne pod zmienne x0, x1, x2, x3, aby spełnić powyższą formułę. Można sprawdzić, że wartościowanie 

x0 = true
x1 = x2 = x3 = false

spełnia podaną formułę.

Rozwiązanie i algorytm

Problem 2SAT można rozwiązać za pomocą algorytmów grafowych. Najpierw należy każdą klauzulę 

p v q

zamienić na implikację 

NOT(p) => q

Mamy już strzałki w grafie :-) Wierzchołkami będą więc zmienne x0, x1, ..., x_{n-1} oraz ich zanegowane odpowiedniki. Mamy więc 2n wierzchołków. Dla każdej klauzuli 

p v q

dodajemy jednak dwie krawędzie: 

NOT(p) => q   oraz   NOT(q) => p

Teraz należy zauważyć, że jeśli w grafie jest cykl zawierający literały 

x oraz NOT(x)

to takiej formuły nie da się spełnić.

Okazuje się, że zachodzi również twierdzenie odwrotne (spróbuj udowodnić), tzn. 

Jeśli w grafie G (graf implikacji) nie ma cyklu zawierającego  x i NOT(x), to istnieje wartościowanie zmiennych spełniające formułę 2CNF

Algorytm rozwiązywania można zapisać w następujący sposób:

  • Posortuj topologicznie wierzchołki w grafie implikacji G
  • Znajdź silnie spójne składowe grafu G
  • Odwiedzaj silnie spójne składowe w kolejności malejących numerów z topologicznego sortowania
    • jeśli wierzchołki w tej silnie spójnej składowej nie mają jeszcze wartości logicznej, to nadaj im wartość false, a ich negacjom wartość true. Następnie wywnioskuj z jedynek jak najwięcej się da, tzn. jeśli true => q to nadaj wierzchołkowi q również wartość true. Postępuj tak np. za pomocą algorytmu DFS. Jeśli w trakcie robienie tego dochodzisz gdzieś do konfliktu, tzn. true => false, to zakończ algorytm z odpowiedzią, że nie da się spełnić formuły 2CNF
  • Po nadaniu wartości logicznych wszystkim wierzchołkom wypisz rozwiązanie.

Implementacja w C++

Poniższy kod można polepszyć pamięciowo:

  1. nie trzeba pamiętać grafu revG
  2. nie trzeba pamiętać 2n wartości logicznych 
/*	Rafał Nowak
 
	2SAT
	G - graf implikacji
	na wejściu podane są implikacje (pojedyncze)
	parzysty numer 2k to zmienna x_k
	nieparzysty  2k+1 to jej negacja NOT(x_k)
 
	Na przykład
 
	(x0 v x1) ^ (x1 v NOT(x2)) ^ (NOT(x1) v x0) ^ (x2 v NOT(x3)) ^ (x0 v x3) ^ (NOT(x0) v NOT(x1)) ^ (x3 v NOT(x2))
 
4 7   //   4 zmienne 7 koniunkcji
1 2   //   (x0 v x1)
3 5   //   itd.
2 0
5 7
1 6
0 3
7 5	
*/
#include<cstdio>
#include<vector>
#include<list>
#include<stack>
using namespace std;
 
typedef vector<int> VI;
typedef list<int> LI;
 
void print(const LI &L); // funkcja drukuje listę
 
struct Graph
{
	int n, m;
 
	VI color; // kolory wierzcholkow
	vector< VI > adj;
 
	Graph(int nn, int mm) : n(nn), m(mm), adj(nn) { }
	void insert(int u, int v) { adj[u].push_back(v); }
 
	LI dfs_list; // drzewo DFS - lista wierzcholkow przetworzonych przez DFS'a
	void dfs_init()
	{
		dfs_list.clear(); // kasujemy drzewo dfs
		color.clear(); color.resize(n, 0); // malujemy wszystkie wierzchołki na biało
	}
 
	void dfs_visit(int u) // rekurencyjny dfs
	{
		color[u] = 1;
		for (int i=0; i<adj[u].size(); i++) if (color[adj[u][i]] == 0) dfs_visit(adj[u][i]);
		color[u] = 2; dfs_list.push_back(u); // dodajemy 'u' do listy przetworzonych wierzcholkow
	}
};
 
// inline int neg(int a) {  return a^1; }// to samo co (a%2==1) ? a-1 : a+1;
#define neg(a) (a)^1
 
vector<bool> czyMa, value;
 
bool setFalse(int a)
{
	if (czyMa[a] && value[a]==true) return false;
	czyMa[a] = true;
	value[a] = false; // printf("setFalse(%d)\n", a);
	return true;
}
 
bool setTrue(Graph &G, int a)
{
	int i,j;
	if (czyMa[a] && value[a]==false) return false;
 
	czyMa[a] = true; if (value[a] == true) return true;
	value[a] = true; // printf("setTrue(%d)\n", a);
	for (i=0; i<G.adj[a].size(); i++)
	{
		j = G.adj[a][i];
		if (value[j]==false)
			if (!setFalse(neg(j)) || !setTrue(G,j)) return false;
	}
	return true;
}
 
bool solve(Graph &G, Graph &revG) // G -> implikacje
{
	int u,v;
	G.dfs_init(); for (u=0; u<G.n; u++) if (G.color[u]==0) G.dfs_visit(u); // dfs na grafie G
 
	value.clear(); value.resize(G.n, false); 
	czyMa.clear(); czyMa.resize(G.n, false);
 
	revG.dfs_init();
	for (LI::const_reverse_iterator it = G.dfs_list.rbegin(); it!=G.dfs_list.rend(); it++)
	{
		u = *it;
		if (revG.color[u]==0)
		{
			revG.dfs_list.clear();
			revG.dfs_visit(u); // print(revG.dfs_list);
 
			v = revG.dfs_list.front(); // reprezentant silnie spójnej składowej
 
			if (!czyMa[v]) // jesli jeszcze nie ma on wartosci logicznej, to ...
			{
				if (!setFalse(v) || !setTrue(G, neg(v))) return false;
			}
//			else if (value[v] == false) return false;
		}
	}
	return true;
}
 
 
int main(void)
{
	int a,b, n,m;
	scanf("%d %d", &n, &m); // n - liczba zmiennych , m - liczba implikacji
//
//       2k    :  x_k
//       2k+1  :  NOT(x_k)
//
	Graph G(2*n,2*m), revG(2*n,2*m); // wierzcholkow jest 2n , a krawedzi 2m
	for (int i=0; i<m; i++)
	{
		scanf("%d %d", &a, &b);
		G.insert(a,b);           revG.insert(b,a);
		G.insert(neg(b),neg(a)); revG.insert(neg(a),neg(b));
	}
 
	if (!solve(G,revG)) printf("No solution");
	else for (int i=0; i<n; i++) printf("x[%d]=%d\n", i, (bool) value[2*i]);
	printf("\n");
	return 0;
}
 
void print(const LI &L)
{
	for (LI::const_iterator i=L.begin(); i!=L.end(); i++) printf("%d,", *i);
	printf("\n");
}

Źródło: "http://www.rafalnowak.pl/wiki/index.php?title=2SAT"