shared proc_num;
shared length;
shared answer;
shared formula[1..1024,0..2];
shared assignment[0..4096];
// robocza pamięć dzielona
shared step;
shared sh_var_count;
shared emptys[0..511,1..1024];
shared formulas[0..511,1..1024,0..2];
shared work2do[0..511];
shared assignments[0..511,0..4096];
// pamięć podręczna
// klauzula "robocza"
local cl_assign[1..4096];
local cl_set[1..1024,0..2];
local cl_empty[1..1024];
local cl_length;
local cannonical;
local var_count;
local proc;
local i;
//----------------------------------
// funkcje podstawowe
function X(l)
begin
return abs(l);
end;
function V(l)
begin
return sgn(l);
end;
//----------------------------------
// funkcja do "odzyskiwania" wartościowania (wymagane z powodu Identify)
function transform_assignment()
local i; local j;
local b;
local pom;
begin
do
begin
pom:=0;
for i:=2 to var_count do
begin
b:=cl_assign[i];
if abs(b)>1 then
if abs(cl_assign[abs(b)])=1 then
cl_assign[i]:=cl_assign[abs(b)]*V(b);
else if abs(cl_assign[abs(b)])=0 then
begin
cl_assign[abs(b)]:=1;
cl_assign[i]:=cl_assign[abs(b)]*V(b);
end;
else pom:=1;
end;
end;
while pom>0;
for i:=1 to var_count-1 do cl_assign[i]:=cl_assign[i+1];
cl_assign[var_count]:=0;
end;
//----------------------------------
// funkcja sprawdzająca czy formuła jest pusta
function empty()
local i;
begin
for i:=1 to cl_length do
if cl_empty[i]>0 then return 0;
return 1;
end;
//----------------------------------
// pomocnicza funkcja ustawiająca zmienne w klauzuli
// w porządku rosnącym
function sort(i)
local pom;
begin
if (cl_set[i,0]>cl_set[i,1] and cl_set[i,1]<>0) or cl_set[i,0]=0 then
begin
pom:=cl_set[i,1];
cl_set[i,1]:=cl_set[i,0];
cl_set[i,0]:=pom;
end;
if (cl_set[i,1]>cl_set[i,2] and cl_set[i,2]<>0) or cl_set[i,1]=0 then
begin
pom:=cl_set[i,2];
cl_set[i,2]:=cl_set[i,1];
cl_set[i,1]:=pom;
end;
if (cl_set[i,0]>cl_set[i,1] and cl_set[i,1]<>0) or cl_set[i,0]=0 then
begin
pom:=cl_set[i,1];
cl_set[i,1]:=cl_set[i,0];
cl_set[i,0]:=pom;
end;
cl_empty[i]:=0;
if cl_set[i,0]<>0 then cl_empty[i]:=1;
if cl_set[i,1]<>0 then cl_empty[i]:=2;
if cl_set[i,2]<>0 then cl_empty[i]:=3;
end;
//----------------------------------
// funkcja "układająca" klauzule w zdaniu
function cleanup()
local i;
begin
for i:=1 to cl_length do
if cl_empty[i]>0 then sort(i);
end;
//----------------------------------
// po wykonaniu Fix klauzula nie zawiera już wystąpień danego literału
function Fix(x,b)
local i; local j;
local pom;
local sat[1..cl_length];
local q[1..var_count];
local qs; local qe;
local xp; local bp;
begin
for i:=1 to cl_length do sat[i]:=0;
// zapisanie wartościowania
cl_assign[x]:=b;
// zainicjowanie bufora
qs:=1;
qe:=qs+1;
q[qs]:=x;
while qe>qs do
begin
x:=q[qs]; b:=cl_assign[x]; qs:=qs+1;
// usunięcie zanegowanych literałów
// jeśli literał jest pojedynczy w klauzuli - błąd
for i:=1 to cl_length do
for j:=0 to cl_empty[i]-1 do
if X(cl_set[i,j])=x and V(cl_set[i,j])=-b then
if cl_empty[i]=1 and sat[i]=0 then return 0;
else cl_set[i,j]:=0;
// sprzątanie
cleanup();
for i:=1 to cl_length do
if cl_empty[i]>0 then
begin
pom:=-1;
if X(cl_set[i,0])=x then pom:=0;
else if X(cl_set[i,1])=x then pom:=1;
else if X(cl_set[i,2])=x then pom:=2;
if pom>cl_empty[i]-1 then pom:=-1;
if pom>-1 then
begin
sat[i]:=1;
for j:=0 to cl_empty[i]-1 do
if j=pom then cl_set[i,j]:=0;
else
begin
xp:=X(cl_set[i,j]);
bp:=-V(cl_set[i,j]);
if cl_assign[xp]=0 then
begin
cl_assign[xp]:=bp;
q[qe]:=xp;
qe:=qe+1;
end;
else if cl_assign[xp]=-bp then return 0;
end;
end;
end;
cleanup();
end;
// i już
return 1;
end;
//----------------------------------
function FixTrue(l)
begin
return Fix(X(l),V(l));
end;
//----------------------------------
function FixFalse(l)
begin
return Fix(X(l),-V(l));
end;
//----------------------------------
function Identify(l1,l2)
local i;
local j;
begin
// zapamiętanie podstawienia
cl_assign[X(l2)]:=V(l2)*l1;
// zastąpienie wystąpień l2 przez odpowiednie l1
for i:=1 to cl_length do
for j:=0 to cl_empty[i]-1 do
if X(cl_set[i,j])=X(l2) then
cl_set[i,j]:=V(l2)*V(cl_set[i,j])*l1;
cleanup();
end;
//----------------------------------
// klauzule jednoelementowe (a)
function rouleA()
local i; local j;
begin
for i:=1 to cl_length-1 do
if cl_empty[i]=1 then
for j:=i+1 to cl_length do
if cl_empty[j]=1 then
if cl_set[i,0]=cl_set[j,0] then cl_empty[j]:=0;
for i:=1 to cl_length do
if cl_empty[i]=1 then
begin
cannonical:=1;
if FixTrue(cl_set[i,0])=0 then return 0;
end;
return 1;
end;
//----------------------------------
// klauzule dwuelementowe (b)
function rouleB()
local i; local j;
begin
for i:=1 to cl_length-1 do
if cl_empty[i]=2 then
for j:=i+1 to cl_length do
if cl_empty[j]=2 then
if cl_set[i,0]=cl_set[j,0] and cl_set[i,1]=cl_set[j,1] then
cl_empty[j]:=0;
for i:=1 to cl_length do
if cl_empty[i]=2 then
begin
cannonical:=1;
if cl_set[i,0]=cl_set[i,1] then return 0;
if cl_set[i,0]<>-cl_set[i,1] then
Identify(-cl_set[i,0],cl_set[i,1]);
cl_empty[i]:=0;
end;
return 1;
end;
//----------------------------------
// klauzule trójelementowe (c)
function rouleC()
local i; local j;
begin
for i:=1 to cl_length-1 do
if cl_empty[i]=3 then
for j:=i+1 to cl_length do
if cl_empty[j]=3 then
if cl_set[i,0]=cl_set[j,0] and
cl_set[i,1]=cl_set[j,1] and
cl_set[i,2]=cl_set[j,2] then cl_empty[j]:=0;
for i:=1 to cl_length do
if cl_empty[i]=3 then
case
cl_set[i,0]=cl_set[i,1] and cl_set[i,0]=cl_set[i,2] :
return 0;
cl_set[i,0]=cl_set[i,1] :
begin
cannonical:=1;
if FixFalse(cl_set[i,0])=0 then return 0;
end;
cl_set[i,0]=-cl_set[i,1] :
begin
cannonical:=1;
if FixFalse(cl_set[i,2])=0 then return 0;
end;
cl_set[i,1]=cl_set[i,2] :
begin
cannonical:=1;
if FixFalse(cl_set[i,1])=0 then return 0;
end;
cl_set[i,1]=-cl_set[i,2] :
begin
cannonical:=1;
if FixFalse(cl_set[i,0])=0 then return 0;
end;
cl_set[i,0]=-cl_set[i,2] :
begin
cannonical:=1;
if FixFalse(cl_set[i,1])=0 then return 0;
end;
end;
return 1;
end;
//----------------------------------
// klauzule z dwoma lub trzema singletonami (d)
function rouleD()
local i; local j;
local pom;
local vars[1..var_count];
begin
for i:=1 to var_count do vars[i]:=0;
for i:=1 to cl_length do
for j:=0 to cl_empty[i]-1 do
begin
pom:=X(cl_set[i,j]);
vars[pom]:=vars[pom]+1;
end;
for i:=1 to cl_length do
begin
pom:=0;
for j:=0 to cl_empty[i]-1 do
if vars[X(cl_set[i,j])]=1 then pom:=pom+1;
if pom=3 then // stwierdzenie 6
begin
cannonical:=1;
cl_assign[X(cl_set[i,0])]:=-V(cl_set[i,0]);
cl_assign[X(cl_set[i,1])]:=-V(cl_set[i,1]);
cl_assign[X(cl_set[i,2])]:=V(cl_set[i,2]);
cl_empty[i]:=0;
end;
else if pom=2 then
begin
cannonical:=1;
if vars[X(cl_set[i,2])]=1 then FixFalse(cl_set[i,2]);
else if vars[X(cl_set[i,1])]=1 then
FixFalse(cl_set[i,1]);
else if vars[X(cl_set[i,0])]=1 then
FixFalse(cl_set[i,0]);
Identify(cl_set[i,0],-cl_set[i,1]);
cl_empty[i]:=0;
return 1;
end;
end;
return 1;
end;
//----------------------------------
// dwie klauzule z więcej niż jedną wspólną zmienną (e)
// (zmienne w klauzuli się nie powtarzają)
function rouleE()
local i; local j;
local x; local y; local z;
local similar[0..2];
local pom;
local pom1; local pom2;
begin
for i:=1 to cl_length-1 do
if cl_empty[i]=3 then
for j:=i+1 to cl_length do
if cl_empty[j]=3 then
begin
pom:=0;
for x:=0 to 2 do
begin
similar[x]:=-1;
for y:=0 to 2 do
if X(cl_set[i,x])=X(cl_set[j,y]) then
begin
pom:=pom+1;
similar[x]:=y;
end;
end;
if pom=3 then
begin
cannonical:=1;
if cl_set[i,0]=cl_set[j,similar[0]] and
cl_set[i,1]=cl_set[j,similar[1]] and
cl_set[i,2]=cl_set[j,similar[2]] then
begin
cl_empty[j]:=0;
return 1;
end;
// stwierdzenie 4
else if cl_set[i,0]=-cl_set[j,similar[0]] and
cl_set[i,1]=-cl_set[j,similar[1]] and
cl_set[i,2]=cl_set[j,similar[2]] then
begin
if FixFalse(cl_set[i,2])=0 then return 0;
cl_empty[j]:=0;
return 1;
end;
else if cl_set[i,0]=-cl_set[j,similar[0]] and
cl_set[i,1]=cl_set[j,similar[1]] and
cl_set[i,2]=-cl_set[j,similar[2]] then
begin
if FixFalse(cl_set[i,1])=0 then return 0;
cl_empty[j]:=0;
return 1;
end;
else if cl_set[i,0]=cl_set[j,similar[0]] and
cl_set[i,1]=-cl_set[j,similar[1]] and
cl_set[i,2]=-cl_set[j,similar[2]] then
begin
if FixFalse(cl_set[i,0])=0 then return 0;
cl_empty[j]:=0;
return 1;
end;
else return 0;
end;
else if pom=2 then
begin
cannonical:=1;
// stwierdzenie 5
case
similar[0]=-1 :
begin x:=1; y:=2; z:=0; end;
similar[1]=-1 :
begin x:=0; y:=2; z:=1; end;
similar[2]=-1 :
begin x:=0; y:=1; z:=2; end;
end;
pom1:=0;
if similar[x]=pom1 or similar[y]=pom1 then pom1:=1;
if similar[x]=pom1 or similar[y]=pom1 then pom1:=2;
case
cl_set[i,x]=cl_set[j,similar[x]] and
cl_set[i,y]=cl_set[j,similar[y]] :
begin
Identify(cl_set[i,z],cl_set[j,pom1]);
cl_empty[j]:=0;
return 1;
end;
cl_set[i,x]=cl_set[j,similar[x]] and
cl_set[i,y]=-cl_set[j,similar[y]] :
if FixFalse(cl_set[i,x])=0 then return 0;
else return 1;
cl_set[i,x]=-cl_set[j,similar[x]] and
cl_set[i,y]=cl_set[j,similar[y]] :
if FixFalse(cl_set[i,y])=0 then return 0;
else return 1;
cl_set[i,x]=-cl_set[j,similar[x]] and
cl_set[i,y]=-cl_set[j,similar[y]] :
begin
pom2:=cl_set[j,pom1];
pom1:=cl_set[i,z];
Identify(cl_set[i,x],-cl_set[i,y]);
if FixFalse(pom1)=0 then return 0;
if FixFalse(pom2)=0 then return 0;
cl_empty[i]:=0;
cl_empty[j]:=0;
return 1;
end;
end;
end;
end;
return 1;
end;
//----------------------------------
// sprowadzenie do postaci kanonicznej
function CannonizeX3SAT()
local i;
local j;
local vars[1..var_count];
begin
do
begin
cannonical:=0;
if rouleA()=0 then return 0;
if cannonical=0 then if rouleB()=0 then return 0;
if cannonical=0 then if rouleC()=0 then return 0;
// jeśli cannonical=0 to w zdaniu są teraz tylko
// klauzule trójelementowe
if cannonical=0 then if rouleD()=0 then return 0;
if cannonical=0 then if rouleE()=0 then return 0;
end;
while cannonical>0;
return 1;
end;
//----------------------------------
function Test(x,b)
begin
if Fix(x,b)=0 then return 0;
if CannonizeX3SAT()=0 then return 0;
if empty()=1 then return 1;
return X3SAT();
end;
//----------------------------------
// warunek 1, formuła jest już w postaci kanonicznej
function cond1()
local i; local j;
local pom;
local v[1..var_count];
local l[-var_count..var_count];
begin
for i:=1 to var_count do v[i]:=0;
for i:=-var_count to var_count do l[i]:=0;
for i:=1 to cl_length do
if cl_empty[i]>0 then
for j:=0 to 2 do
begin
pom:=cl_set[i,j];
v[X(pom)]:=v[X(pom)]+1;
l[pom]:=l[pom]+1;
end;
for i:=1 to cl_length do
if cl_empty[i]>0 then
begin
if v[X(cl_set[i,0])]<>1 and
v[X(cl_set[i,1])]<>1 and
v[X(cl_set[i,2])]<>1 then return 0;
if l[-cl_set[i,0]]<>0 or
l[-cl_set[i,1]]<>0 or
l[-cl_set[i,2]]<>0 then return 0;
end;
// jest OK, znajdź wartościowanie
for i:=1 to cl_length do
if cl_empty[i]>0 then
for j:=0 to 2 do
if v[X(cl_set[i,j])]=1 then
cl_assign[X(cl_set[i,j])]:=V(cl_set[i,j]);
else
cl_assign[X(cl_set[i,j])]:=-V(cl_set[i,j]);
return 1;
end;
//----------------------------------
// krok 2, formuła jest w postaci kanonicznej
function find_variable()
local i; local j;
local l[-var_count..var_count];
begin
for i:=-var_count to var_count do l[i]:=0;
for i:=1 to cl_length do
if cl_empty[i]>0 then
for j:=0 to 2 do
l[cl_set[i,j]]:=l[cl_set[i,j]]+1;
for i:=2 to var_count do
if l[i]>0 and l[-i]>0 then return i;
for i:=1 to cl_length do
if cl_empty[i]>0 then
if (l[cl_set[i,0]]>1 or l[-cl_set[i,0]]>1) and
(l[cl_set[i,1]]>1 or l[-cl_set[i,1]]>1) and
(l[cl_set[i,2]]>1 or l[-cl_set[i,2]]>1) then
return X(cl_set[i,0]);
return 0;
end;
//----------------------------------
// część główna algorytmu (nie programu)
function X3SAT()
local x;
local l_cl_set[1..cl_length,0..2];
local l_cl_empty[1..cl_length];
local l_cl_assign[1..var_count];
begin
// każda klauzula zawiera singleton i wszystkie zmienne są stałe (1)
if cond1()=1 then return 1;
// znalezienie zmiennej (2)
x:=find_variable();
if x=0 then exit;
// zachowanie dotychczasowego stanu ("stos" rekursji)
memcopy(cl_set,l_cl_set,3*cl_length);
memcopy(cl_empty,l_cl_empty,cl_length);
memcopy(cl_assign,l_cl_assign,var_count);
// krok indukcyjny
if Test(x,1)=1 then return 1;
// odtworzenie stanu
memcopy(l_cl_set,cl_set,3*cl_length);
memcopy(l_cl_empty,cl_empty,cl_length);
memcopy(l_cl_assign,cl_assign,var_count);
// kolejny krok
return Test(x,-1);
end;
//----------------------------------
// równoległa funkcja analogiczna do pary Test+X3SAT
function parX3SAT(step)
local x;
local l_cl_set[1..cl_length,0..2];
local l_cl_empty[1..cl_length];
local l_cl_assign[1..var_count];
begin
// każda klauzula zawiera singleton i wszystkie zmienne są stałe (1)
if cond1()=1 then return 1;
// znalezienie zmiennej (2)
x:=find_variable();
if x=0 then exit;
// zachowanie dotychczasowego stanu ("stos" rekursji)
memcopy(cl_set,l_cl_set,3*cl_length);
memcopy(cl_empty,l_cl_empty,cl_length);
memcopy(cl_assign,l_cl_assign,var_count);
// jeden krok Test()
work2do[proc]:=0;
if Fix(x,1)<>0 then
if CannonizeX3SAT()<>0 then
if empty()=1 then return 1;
else
begin
work2do[proc]:=1;
blockwrite(cl_set,formulas[proc],3*cl_length);
blockwrite(cl_empty,emptys[proc],cl_length);
blockwrite(cl_assign,assignments[proc],var_count);
end;
// odtworzenie stanu
memcopy(l_cl_set,cl_set,3*cl_length);
memcopy(l_cl_empty,cl_empty,cl_length);
memcopy(l_cl_assign,cl_assign,var_count);
// drugi krok Test()
work2do[proc+step]:=0;
if Fix(x,-1)<>0 then
if CannonizeX3SAT()<>0 then
if empty()=1 then return 1;
else
begin
work2do[proc+step]:=1;
blockwrite(cl_set,formulas[proc+step],3*cl_length);
blockwrite(cl_empty,emptys[proc+step],cl_length);
blockwrite(cl_assign,assignments[proc+step],var_count);
end;
return 0;
end;
//----------------------------------
// funkcja znajdująca wartościowanie
function parCalculate()
local i; local j;
local break;
begin
for i:=0 to log(proc_num) do
begin
step:=pow2(i);
//jeden równoległy krok algorytmu
for proc:=0 to pow2(i)-1 pardo
if work2do[proc]<>0 then
begin
// najpierw pobranie z pamięci dzielonej formuły
cl_length:=length;
var_count:=sh_var_count;
blockread(formulas[proc],cl_set,3*cl_length);
blockread(assignments[proc],cl_assign,var_count);
blockread(emptys[proc],cl_empty,cl_length);
if step=proc_num then
begin
if X3SAT()=1 then
begin
answer:=1;
transform_assignment();
blockwrite(cl_assign,assignment,var_count);
exit;
end;
end;
else
if parX3SAT(step)=1 then
begin
answer:=1;
transform_assignment();
blockwrite(cl_assign,assignment,var_count);
exit;
end;
end;
// sprawdzenie czy jeszcze jest coś do zrobienia
break:=1;
for j:=0 to pow2(i)-1 do if work2do[j]<>0 then break:=0;
if break=1 then exit;
end;
end;
//----------------------------------
// funkcja przygotowująca dane od obróbki
function prepare_data()
local i; local j;
local pom;
begin
var_count:=0;
for i:=1 to length do
begin
cl_empty[i]:=3;
for j:=0 to 2 do
begin
pom:=formula[i,j];
formula[i,j]:=pom+V(pom);
pom:=formula[i,j];
if var_count<X(pom) then var_count:=X(pom);
end;
end;
cl_length:=length;
blockread(formula,cl_set,3*cl_length);
cleanup();
for i:=1 to var_count do cl_assign[i]:=0;
if CannonizeX3SAT()=0 then exit;
if empty()=1 then
begin
answer:=1;
transform_assignment();
blockwrite(cl_assign,assignment,var_count);
exit;
end;
sh_var_count:=var_count;
for i:=0 to proc_num-1 do
begin
work2do[i]:=0;
for j:=0 to var_count do assignments[i,j]:=0;
end;
return 1;
end;
//----------------------------------
// część główna programu
begin
proc_num:=pow2(log(proc_num));
answer:=0;
prepare_data();
blockwrite(cl_set,formulas[0],3*cl_length);
blockwrite(cl_empty,emptys[0],cl_length);
blockwrite(cl_assign,assignments[0],var_count);
work2do[0]:=1;
parCalculate();
end.