Path: DBAI > Research > Projects > D-FLAT Project > Software > D-FLAT System > Practice > Secure Set
Tools: Print
Secure Set
%dflat: -e vertex -e edge -d td -n semi --depth 2 --default-join
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% TASK
% Find all secure sets in a graph G. A subset S of a graph G is secure
% if, for each subset X⊆S , |N[X]∩S|≥|N[X]\S| holds.
% Here, N[X] denotes the closed neighbourhood of X in G , i.e., the set
% X together with all vertices adjacent to some vertex in X .
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PREPARATION
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Set depth of the item tree to two levels.
length(2).
% Set type of the nodes on level 0 to 'or'.
% This statement is used to allow the enumeration of all solutions.
or(0).
% Set type of the nodes on level 1 to 'and'.
% This statement ensures that none of the extended rows on level 2
% contains the fact 'reject'. If only a single row fails this
% check, the whole row on the top level is rejected.
and(1).
% Ensure that all the edges are undirected.
edge(Y,X) :- current(X;Y), edge(X,Y).
edge(Y,X) :- current(X), removed(Y), edge(X,Y).
edge(Y,X) :- current(Y), removed(X), edge(X,Y).
edge(Y,X) :- removed(X), removed(Y), edge(X,Y).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% GUESS
% Guess a branch of each child's semantic tree such that the branch
% contains no "invalid" or "bad" vertices. Then guess a subset of
% introduced input graph vertices (inS) as part of the potentially secure
% set on level 1. Afterwards, guess a subset of the newly introduced
% vertices which are part of inS to form a sub-subset (inX). Retain the
% information from the guessed branch that concerns still-current input
% graph vertices, and set individual and update all the important values
% for the checking part.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Guess one row for each child node which should be extended on level 0.
1 { extend(0,R) : rootOf(R,N) } 1 :- childNode(N).
% Guess exactly one row which should be extended for each level.
1 { extend(L+1,S) : sub(R,S) } 1 :- extend(L,R), sub(R,_).
% Guess a subset of the newly introduced vertices which extend
% the potentially secure set S which we want to check if it is
% really secure.
{ item(1,inS(V)) } :- introduced(V).
% Guess a subset of the newly introduced extensions to inS which
% extends the subset X which we want to investigate on level 2
% of the item tree.
{ item(2,inX(V)) } :- introduced(V), item(1,inS(V)).
% Retain the information about the subsets under investigation.
item(1,inS(V)) :- extend(1,R), current(V), childItem(R,inS(V)).
item(2,inX(V)) :- extend(2,R), current(V), childItem(R,inX(V)).
% Retain the information about attackers and defenders.
auxItem(2,globalDefender(V)) :- extend(2,R), current(V),
childAuxItem(R,globalDefender(V)).
auxItem(2,globalAttacker(V)) :- extend(2,R), current(V),
childAuxItem(R,globalAttacker(V)).
% Each vertex in X defends itself and is defended by its neighbors in S.
auxItem(2,globalDefender(V)) :- current(V), item(2,inX(V)).
auxItem(2,globalDefender(Y)) :- current(Y), item(2,inX(X)), edge(X,Y),
item(1,inS(Y)).
% Each vertex in X is attacked by neighbors which are not elements of S.
auxItem(2,globalAttacker(Y)) :- current(Y), item(2,inX(X)), edge(X,Y),
not item(1,inS(Y)).
% Initialize the fitness counter for introduced vertices in S.
counter(fitness(V),0) :- introduced(V), item(1,inS(V)).
% Initialize the global fitness counter to 0 when we are in a leaf node of
% the tree decomposition. To determine if the current node is really a
% leaf node, we check if the count of child nodes is 0.
counter(globalFitness,0) :- 0 #count { CN : childNode(CN) } 0.
% When the current node is an exchange node (the number of extended rows
% is 1 in this case), then we have to increase the counters by the number
% of attackers and decrease it by the number of defenders accordingly.
defender(X,Y) :- extend(R), item(inX(X)), edge(X,Y), childItem(R,inS(Y)).
attacker(X,Y) :- extend(R), item(inX(X)), edge(X,Y),
not childItem(R,inS(Y)).
counter(fitness(V),CF + NF) :- current(V), extend(2,R),
childCounter(R,fitness(V),CF),
NF = #sum { 1,V,X : defender(V,X), removed(X);
-1,V,X : attacker(V,X), removed(X) }.
counter(globalFitness,CF + NF) :- extend(2,R),
childCounter(R,globalFitness,CF),
NF = #sum { 1,V : childAuxItem(R,globalDefender(V)), removed(V);
-1,V : childAuxItem(R,globalAttacker(V)), removed(V) }.
%Remove fitness counter when its corresponding vertex was removed.
counterRem(fitness(V)) :- removed(V).
% Initialize current counters for fitness and the one for global fitness.
currentCounter(fitness(V),0) :- counter(fitness(V),_).
currentCounter(globalFitness,0).
% Initialize cardinality of a leaf node to 0.
counter(cardinality,0) :- 0 #count { CN : childNode(CN) } 0.
% The cardinality of a exchange node is simply the sum of the child costs
% and the count of introduced input graph vertices which are part of S.
counter(cardinality,CC + C) :- extend(2,R), childCounter(R,cardinality,CC),
C = #count { V : item(1,inS(V)), introduced(V) }.
% Define the cardinality current counter as being the count of current
% input graph vertices which are part of S.
currentCounter(cardinality,LC) :- LC = #count { V : item(1,inS(V)),
current(V) }.
% Define the cost as being equivalent to the cardinality.
counter(cost,C) :- counter(cardinality,C).
currentCounter(cost,C) :- currentCounter(cardinality,C).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% CHECK
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Add the fact 'reject' to the resulting row on level 2 if the condition
% of a secure set - The number of attackers must be less or equal to the
% number of defenders. - is violated in order to ensure that the
% corresponding solution candidate on level 0 (the potentially secure
% set S) is deleted. This rule can be checked only in the final tree
% decomposition node.
reject :- final, counter(globalFitness,F), F < 0.
% Add the fact '_reject' to the resulting row on level 2 if the condition
% of a secure set - The number of attackers must be less or equal to the
% number of defenders. - is violated in order to ensure that the
% corresponding solution candidate on level 0 (the potentially secure set
% S) is deleted. This rule can be checked in all tree decomposition nodes.
reject :- extend(2,R), removed(V),
childItem(R,inX(V)),
childCounter(R,fitness(V),CF),
NF = #sum { 1,V,X : defender(V,X), current(X);
1,V,X : defender(V,X), removed(X);
-1,V,X : attacker(V,X), current(X);
-1,V,X : attacker(V,X), removed(X) },
CF + NF + 1 < 0.
% Add the fact '_reject' to the resulting row on level 2 if S is empty
% This rule can be checked only in the final tree decomposition node.
reject :- final, childCounter(R,cardinality,0), extend(2,R).
% Add the fact '_accept' to the resulting row on level 2 if we are in the
% final tree decomposition node and the fact 'reject' has not been added.
accept :- final, not reject.
#show item/2. #show auxItem/2. #show counter/2. #show extend/2.
#show length/1. #show or/1. #show and/1. #show accept/0. #show reject/0.
Reference
Bliem, B. and Woltran, S. Complexity of Secure Sets.CoRR, abs/1411.6549, 2014.
Last updated: 2017-09-05 19:08