1		:- module(sat_symmetry_breaking, [get_symmetry_breaking_predicates/3]).
2
3		:- use_module(library(lists)).
4		:- use_module(library(samsort)).
5		:- use_module(extension('bliss/bliss_interface')).
6		:- use_module(cdclt_solver(cdclt_pred_to_sat),[next_sat_var_name/1]).
7
8		% Foundation: "Symmetry-breaking predicates for search problems" by Crawford et al.
9		% Improvement: "Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetry" by Aloul et al.
10
11		%% get_symmetry_breaking_predicates(+CNF, -SBPs, -NewSatVars).
12		get_symmetry_breaking_predicates(CNF, SBPs, NewSatVars) :-
13		bliss_interface:init_bliss_interface,
14		bliss_interface:init_undirected_graph,
15		cnf_to_colored_graph(CNF),
16		bliss_interface:find_automorphisms(Generators),
17		nl, write('Generators: '), write(Generators),nl,
18		get_sbps_from_generators(Generators, TSBPs, NewSatVars),
19		!,
20		SBPs = TSBPs.
21
22		get_sbps_from_generators(Generators, SBPs, NewSatVars) :-
23		add_sbps_from_generators(Generators, [], SBPs, [], NewSatVars).
24
25		add_sbps_from_generators([], Acc, Acc, SAcc, SAcc).
26		add_sbps_from_generators([Generator|T], Acc, SBPs, SAcc, NewSatVars) :-
27		add_sbps_from_generator(Generator, Acc , NAcc, SAcc, NSAcc),
28		add_sbps_from_generators(T, NAcc, SBPs, NSAcc, NewSatVars).
29
30		get_sbps_from_cycle([Id1,Id2], SBPConj) :-
31		% not(Id1) or Id2
32		get_clause_from_node_id_atom(Id1, Clause1),
33		get_clause_from_node_id_atom(Id2, Clause2),
34		negate_clause_to_conj(Clause1, NegConj1),
35		( NegConj1 = [Clause2]
36		-> SBPConj = [Clause2]
37		; maplist(append(Clause2), NegConj1, SBPConj)
38		).
39		get_sbps_from_cycle([Id1,Id2,Id3], SBPConj) :-
40		get_sbps_from_cycle([Id1,Id2], SBPConj1),
41		get_sbps_from_cycle([Id2,Id3], SBPConj2),
42		append(SBPConj1, SBPConj2, SBPConj).
43
44		% only considers two-cycles and three-cycles
45		add_sbps_from_generator([[Id1,Id2]], Acc , NAcc, SAcc, SAcc) :-
46		get_sbps_from_cycle([Id1,Id2], SBPConj),
47		append(SBPConj, Acc, NAcc).
48		add_sbps_from_generator([[Id1,Id2,Id3]], Acc , NAcc, SAcc, SAcc) :-
49		add_sbps_from_generator([[Id1,Id2]], Acc, NAcc1, _, _),
50		add_sbps_from_generator([[Id2,Id3]], NAcc1, NAcc, _, _).
51		add_sbps_from_generator([Cycle1,Cycle2|T], Acc, NAcc, SAcc, NSAcc) :-
52		% e.g., (ab)(cd)(ef) -> (not(a) or b) & (a=b)=>(not(c) or d) & ((a=b) & (c=d))=>(not(e) or f)
53		get_equality_from_cycle(Cycle1, Acc, NAcc1, SAcc, SAcc1, NegEqNodeTriple),
54		add_sbps_from_generator([Cycle1], NAcc1, NAcc2, _, _),
55		add_sbps_from_generator_multi([Cycle2|T], [NegEqNodeTriple], NAcc2, NAcc, SAcc1, NSAcc).
56
57		add_sbps_from_generator_multi([], _, NAcc, NAcc, SAcc, SAcc).
58		add_sbps_from_generator_multi([Cycle|T], NegEqNodeTriples, Acc, NAcc, SAcc, NSAcc) :-
59		get_sbps_from_cycle(Cycle, SBPsCycle),
60		% not(EqNodeTriples) or SBPsCycle
61		maplist(append(NegEqNodeTriples), SBPsCycle, ImplCNF),
62		append(ImplCNF, Acc, NAcc1),
63		( T == []
64		-> NNegEqNodeTriples = NegEqNodeTriples,
65		NAcc2 = NAcc1,
66		SAcc1 = SAcc
67		; get_equality_from_cycle(Cycle, NAcc1, NAcc2, SAcc, SAcc1, NegEqNodeTriple),
68		NNegEqNodeTriples = [NegEqNodeTriple|NegEqNodeTriples]
69		),
70		add_sbps_from_generator_multi(T, NNegEqNodeTriples, NAcc2, NAcc, SAcc1, NSAcc).
71
72		get_equality_from_cycle(Cycle, Acc, NAcc, SAcc, [SatVarName-EqClauses|SAcc], NegEqNodeTriple) :-
73		next_sat_var_name(SatVarName),
74		PosEqNodeTriple = pred_true-_-SatVarName,
75		NegEqNodeTriple = pred_false-_-SatVarName,
76		get_equality_from_cycle_cnf(Cycle, PosEqNodeTriple, NegEqNodeTriple, EqCNF),
77		get_clauses_from_bliss_cycle(Cycle, EqClauses),
78		append(EqCNF, Acc, NAcc).
79
80		get_clauses_from_bliss_cycle(Cycle, EqSatVarNames) :-
81		get_clauses_from_bliss_cycle(Cycle, [], EqSatVarNames).
82
83		get_clauses_from_bliss_cycle([], Acc, Acc).
84		get_clauses_from_bliss_cycle([IdA|T], Acc, EqSatVarNames) :-
85		get_clause_from_node_id_atom(IdA, Clause),
86		get_clauses_from_bliss_cycle(T, [Clause|Acc], EqSatVarNames).
87
88		get_equality_from_cycle_cnf([Id1,Id2], PosEqNodeTriple, NegEqNodeTriple, EqCNF) :-
89		% the new SAT variable eq is equivalent to the equality of Id1 & Id2
90		% note that non unit clauses might be referenced to ids which requires some rewriting
91		disjunct_ids_to_cnf(Id1, not(Id2), TCNF1),
92		maplist(append([NegEqNodeTriple]), TCNF1, CNF1),
93		disjunct_ids_to_cnf(not(Id1), Id2, TCNF2),
94		maplist(append([NegEqNodeTriple]), TCNF2, CNF2),
95		append(CNF1, CNF2, CNFLhsImpl),
96		disjunct_ids_to_cnf(not(Id1), not(Id2), TCNF3),
97		maplist(append([PosEqNodeTriple]), TCNF3, CNF3),
98		disjunct_ids_to_cnf(Id1, Id2, TCNF4),
99		maplist(append([PosEqNodeTriple]), TCNF4, CNF4),
100		append(CNF3, CNF4, CNFRhsImpl),
101		append(CNFLhsImpl, CNFRhsImpl, EqCNF). % TO DO: falsity of eq
102		get_equality_from_cycle_cnf([Id1,Id2,Id3], PosEqNodeTriple, NegEqNodeTriple, EqCNF) :-
103		% the new SAT variable eq is equivalent to the equality of Id1 & Id2 & Id3
104		disjunct_ids_to_cnf(not(Id1), Id3, TCNF1),
105		maplist(append([NegEqNodeTriple]), TCNF1, CNF1),
106		disjunct_ids_to_cnf(Id1, not(Id2), TCNF2),
107		maplist(append([NegEqNodeTriple]), TCNF2, CNF2),
108		disjunct_ids_to_cnf(Id2, not(Id3), TCNF3),
109		maplist(append([NegEqNodeTriple]), TCNF3, CNF3),
110		append([CNF1,CNF2,CNF3], CNFLhsImpl),
111		disjunct_ids_to_cnf(not(Id1), not(Id2), TCNF4),
112		maplist(append([PosEqNodeTriple]), TCNF4, TTCNF4),
113		get_clause_from_node_id_atom(Id3, Clause3),
114		negate_clause_to_conj(Clause3, NegConj3),
115		append(TTCNF4, NegConj3, CNF4),
116		disjunct_ids_to_cnf(Id1, Id2, TCNF5),
117		maplist(append([PosEqNodeTriple]), TCNF5, TTCNF5),
118		maplist(append(Clause3), TTCNF5, CNF5),
119		append(CNF4, CNF5, CNFRhsImpl),
120		append(CNFLhsImpl, CNFRhsImpl, EqCNF).
121
122		disjunct_ids_to_cnf(not(Id1), not(Id2), CNF) :-
123		!,
124		get_clause_from_node_id_atom(Id1, Clause1),
125		get_clause_from_node_id_atom(Id2, Clause2),
126		negate_clause_to_conj(Clause1, Id1Conj),
127		negate_clause_to_conj(Clause2, Id2Conj),
128		disjunct_cnfs_to_cnf(Id1Conj, Id2Conj, CNF).
129		disjunct_ids_to_cnf(not(Id1), Id2, CNF) :-
130		!,
131		get_clause_from_node_id_atom(Id1, Clause1),
132		get_clause_from_node_id_atom(Id2, Clause2),
133		negate_clause_to_conj(Clause1, Id1Conj),
134		maplist(append(Clause2), Id1Conj, CNF).
135		disjunct_ids_to_cnf(Id1, not(Id2), CNF) :-
136		!,
137		get_clause_from_node_id_atom(Id1, Clause1),
138		get_clause_from_node_id_atom(Id2, Clause2),
139		negate_clause_to_conj(Clause2, Id2Conj),
140		maplist(append(Clause1), Id2Conj, CNF).
141		disjunct_ids_to_cnf(Id1, Id2, CNF) :-
142		get_clause_from_node_id_atom(Id1, Clause1),
143		get_clause_from_node_id_atom(Id2, Clause2),
144		append(Clause1, Clause2, NewClause),
145		CNF = [NewClause].
146
147		disjunct_cnfs_to_cnf(Id1Conj, [], Id1Conj) :- !.
148		disjunct_cnfs_to_cnf([], Id2Conj, Id2Conj) :- !.
149		disjunct_cnfs_to_cnf(Id1Conj, Id2Conj, CNF) :-
150		disjunct_cnfs_to_cnf_acc(Id1Conj, Id2Conj, [], CNF).
151
152		disjunct_cnfs_to_cnf_acc([], _, Acc, Acc).
153		disjunct_cnfs_to_cnf_acc([Clause1|T1], Id2Conj, Acc, CNF) :-
154		maplist(append(Clause1), Id2Conj, TConj),
155		append(TConj, Acc, NAcc),
156		disjunct_cnfs_to_cnf_acc(T1, Id2Conj, NAcc, CNF).
157
158		negate_clause_to_conj(Clause, NegConj) :-
159		negate_clause_to_conj(Clause, [], NegConj).
160
161		negate_clause_to_conj([], Acc, Acc).
162		negate_clause_to_conj([Pol-_-SatVarName|T], Acc, NegConj) :-
163		negate_polarity(Pol, NegPol),
164		negate_clause_to_conj(T, [[NegPol-_-SatVarName]|Acc], NegConj).
165
166		negate_polarity(pred_true, pred_false).
167		negate_polarity(pred_false, pred_true).
168
169		get_clause_from_node_id_atom(IdAtom, Clause) :-
170		number_to_atom(NId, IdAtom),
171		get_clause_from_node_id(NId, Clause).
172
173		get_clause_from_node_id(Id, Clause) :-
174		sat_clause(Id, TClause),
175		!,
176		Clause = TClause.
177		get_clause_from_node_id(Id, Clause) :-
178		seen(SatVarName,Pol,Id), % TO DO: improve search by Id
179		Clause = [Pol-_-SatVarName].
180
181		:- dynamic seen/3, sat_clause/2.
182		:- volatile seen/3, sat_clause/2.
183
184		cnf_to_colored_graph(CNF) :-
185		retractall(seen(_,_,_)),
186		retractall(sat_clause(_,_)),
187		cnf_to_colored_graph_init(CNF).
188
189		lit_compare(_-_-A1, _-_-A2) :- A1@<A2.
190
191		cnf_to_colored_graph_init([]).
192		cnf_to_colored_graph_init([Clause|T]) :-
193		samsort(lit_compare, Clause, SClause),
194		\+ sat_clause(_, SClause),
195		clause_to_colored_graph(SClause),
196		cnf_to_colored_graph_init(T).
197		cnf_to_colored_graph_init([_|T]) :-
198		cnf_to_colored_graph_init(T).
199
200		%% clause_to_colored_graph(+Clause, +ClauseBlissId).
201		% Removes true clauses and false literals.
202		clause_to_colored_graph([Pol-Pol-_]) :-
203		% CNF has already been unit propagated so all unit clauses are true
204		!.
205		clause_to_colored_graph([Pol1-Var1-Lit1,Pol2-Var2-Lit2]) :-
206		( (Pol1 == Var1; Pol2 == Var2)
207		-> true
208		; % edge without clause node for binary clause
209		register_var_node(Lit1, Lit1IdPos, Lit1IdNeg),
210		register_var_node(Lit2, Lit2IdPos, Lit2IdNeg),
211		( Pol1 == pred_true
212		-> ELit1 = Lit1IdPos
213		; ELit1 = Lit1IdNeg
214		),
215		( Pol2 == pred_true
216		-> ELit2 = Lit2IdPos
217		; ELit2 = Lit2IdNeg
218		),
219		bliss_interface:add_edge(ELit1, ELit2)
220		),
221		!.
222		clause_to_colored_graph(Clause) :-
223		member(Pol-Var-_, Clause),
224		Pol == Var,
225		!.
226		clause_to_colored_graph(Clause) :-
227		Clause \= [_],
228		bliss_interface:add_node(1, ClauseBlissId),
229		asserta(sat_clause(ClauseBlissId,Clause)),
230		clause_to_colored_graph_non_binary(Clause, ClauseBlissId).
231
232		clause_to_colored_graph_non_binary([], _).
233		clause_to_colored_graph_non_binary([Pol-Var-Lit|T], ClauseBlissId) :-
234		negate_polarity(Pol, NegPol),
235		Var \== NegPol, % remove false literals
236		!,
237		register_var_node(Lit, LitIdPos, LitIdNeg),
238		( Pol == pred_true
239		-> ELit = LitIdPos
240		; ELit = LitIdNeg
241		),
242		bliss_interface:add_edge(ELit, ClauseBlissId),
243		clause_to_colored_graph_non_binary(T, ClauseBlissId).
244		clause_to_colored_graph_non_binary([_|T], ClauseBlissId) :-
245		clause_to_colored_graph_non_binary(T, ClauseBlissId).
246
247		%% register_var_node(+Lit, -LitIdPos, -LitIdNeg).
248		% Two nodes for a SAT variable for the two polarities and one edge between both nodes.
249		register_var_node(Lit, LitIdPos, LitIdNeg) :-
250		seen(Lit,pred_true,TLitIdPos),
251		seen(Lit,pred_false,TLitIdNeg),
252		!,
253		LitIdPos = TLitIdPos,
254		LitIdNeg = TLitIdNeg.
255		register_var_node(Lit, LitIdPos, LitIdNeg) :-
256		bliss_interface:add_node(2, LitIdPos),
257		bliss_interface:add_node(2, LitIdNeg),
258		asserta(seen(Lit,pred_true,LitIdPos)),
259		asserta(seen(Lit,pred_false,LitIdNeg)),
260		bliss_interface:add_edge(LitIdPos, LitIdNeg).
261
262		number_to_atom(Number, Atom) :-
263		number(Number),
264		number_codes(Number, Codes),
265		atom_codes(Atom, Codes),!.
266		number_to_atom(Number, Atom) :-
267		atom(Atom),
268		atom_codes(Atom, Codes),
269		number_codes(Number, Codes),!.