sat_symmetry_breaking

add_sbps_from_generator([[Id1,Id2]], Acc , NAcc, SAcc, SAcc) :-
    get_sbps_from_cycle([Id1,Id2], SBPConj),
    append(SBPConj, Acc, NAcc).

add_sbps_from_generator([[Id1,Id2,Id3]], Acc , NAcc, SAcc, SAcc) :-
    add_sbps_from_generator([[Id1,Id2]], Acc, NAcc1, _, _),
    add_sbps_from_generator([[Id2,Id3]], NAcc1, NAcc, _, _).

add_sbps_from_generator([Cycle1,Cycle2|T], Acc, NAcc, SAcc, NSAcc) :-
    % e.g., (ab)(cd)(ef) -> (not(a) or b) & (a=b)=>(not(c) or d) & ((a=b) & (c=d))=>(not(e) or f)
    get_equality_from_cycle(Cycle1, Acc, NAcc1, SAcc, SAcc1, NegEqNodeTriple),
    add_sbps_from_generator([Cycle1], NAcc1, NAcc2, _, _),
    add_sbps_from_generator_multi([Cycle2|T], [NegEqNodeTriple], NAcc2, NAcc, SAcc1, NSAcc).

add_sbps_from_generator_multi([], _, NAcc, NAcc, SAcc, SAcc).

add_sbps_from_generator_multi([Cycle|T], NegEqNodeTriples, Acc, NAcc, SAcc, NSAcc) :-
    get_sbps_from_cycle(Cycle, SBPsCycle),
    % not(EqNodeTriples) or SBPsCycle
    maplist(append(NegEqNodeTriples), SBPsCycle, ImplCNF),
    append(ImplCNF, Acc, NAcc1),
    ( T == []
    -> NNegEqNodeTriples = NegEqNodeTriples,
    NAcc2 = NAcc1,
    SAcc1 = SAcc
    ; get_equality_from_cycle(Cycle, NAcc1, NAcc2, SAcc, SAcc1, NegEqNodeTriple),
    NNegEqNodeTriples = [NegEqNodeTriple|NegEqNodeTriples]
    ),
    add_sbps_from_generator_multi(T, NNegEqNodeTriples, NAcc2, NAcc, SAcc1, NSAcc).

add_sbps_from_generators([], Acc, Acc, SAcc, SAcc).

add_sbps_from_generators([Generator|T], Acc, SBPs, SAcc, NewSatVars) :-
    add_sbps_from_generator(Generator, Acc , NAcc, SAcc, NSAcc),
    add_sbps_from_generators(T, NAcc, SBPs, NSAcc, NewSatVars).

clause_to_colored_graph([Pol-Pol-_]) :-
    % CNF has already been unit propagated so all unit clauses are true
    !.

clause_to_colored_graph([Pol1-Var1-Lit1,Pol2-Var2-Lit2]) :-
    ( (Pol1 == Var1; Pol2 == Var2)
    -> true
    ; % edge without clause node for binary clause
    register_var_node(Lit1, Lit1IdPos, Lit1IdNeg),
    register_var_node(Lit2, Lit2IdPos, Lit2IdNeg),
    ( Pol1 == pred_true
    -> ELit1 = Lit1IdPos
    ; ELit1 = Lit1IdNeg
    ),
    ( Pol2 == pred_true
    -> ELit2 = Lit2IdPos
    ; ELit2 = Lit2IdNeg
    ),
    bliss_interface:add_edge(ELit1, ELit2)
    ),
    !.

clause_to_colored_graph(Clause) :-
    member(Pol-Var-_, Clause),
    Pol == Var,
    !.

clause_to_colored_graph(Clause) :-
    Clause \= [_],
    bliss_interface:add_node(1, ClauseBlissId),
    asserta(sat_clause(ClauseBlissId,Clause)),
    clause_to_colored_graph_non_binary(Clause, ClauseBlissId).

clause_to_colored_graph_non_binary([], _).

clause_to_colored_graph_non_binary([Pol-Var-Lit|T], ClauseBlissId) :-
    negate_polarity(Pol, NegPol),
    Var \== NegPol, % remove false literals
    !,
    register_var_node(Lit, LitIdPos, LitIdNeg),
    ( Pol == pred_true
    -> ELit = LitIdPos
    ; ELit = LitIdNeg
    ),
    bliss_interface:add_edge(ELit, ClauseBlissId),
    clause_to_colored_graph_non_binary(T, ClauseBlissId).

clause_to_colored_graph_non_binary([_|T], ClauseBlissId) :-
    clause_to_colored_graph_non_binary(T, ClauseBlissId).

cnf_to_colored_graph(CNF) :-
    retractall(seen(_,_,_)),
    retractall(sat_clause(_,_)),
    cnf_to_colored_graph_init(CNF).

cnf_to_colored_graph_init([]).

cnf_to_colored_graph_init([Clause|T]) :-
    samsort(lit_compare, Clause, SClause),
    \+ sat_clause(_, SClause),
    clause_to_colored_graph(SClause),
    cnf_to_colored_graph_init(T).

cnf_to_colored_graph_init([_|T]) :-
    cnf_to_colored_graph_init(T).

disjunct_cnfs_to_cnf(Id1Conj, [], Id1Conj) :- !.

disjunct_cnfs_to_cnf([], Id2Conj, Id2Conj) :- !.

disjunct_cnfs_to_cnf(Id1Conj, Id2Conj, CNF) :-
    disjunct_cnfs_to_cnf_acc(Id1Conj, Id2Conj, [], CNF).

disjunct_cnfs_to_cnf_acc([], _, Acc, Acc).

disjunct_cnfs_to_cnf_acc([Clause1|T1], Id2Conj, Acc, CNF) :-
    maplist(append(Clause1), Id2Conj, TConj),
    append(TConj, Acc, NAcc),
    disjunct_cnfs_to_cnf_acc(T1, Id2Conj, NAcc, CNF).

disjunct_ids_to_cnf(not(Id1), not(Id2), CNF) :-
    !,
    get_clause_from_node_id_atom(Id1, Clause1),
    get_clause_from_node_id_atom(Id2, Clause2),
    negate_clause_to_conj(Clause1, Id1Conj),
    negate_clause_to_conj(Clause2, Id2Conj),
    disjunct_cnfs_to_cnf(Id1Conj, Id2Conj, CNF).

disjunct_ids_to_cnf(not(Id1), Id2, CNF) :-
    !,
    get_clause_from_node_id_atom(Id1, Clause1),
    get_clause_from_node_id_atom(Id2, Clause2),
    negate_clause_to_conj(Clause1, Id1Conj),
    maplist(append(Clause2), Id1Conj, CNF).

disjunct_ids_to_cnf(Id1, not(Id2), CNF) :-
    !,
    get_clause_from_node_id_atom(Id1, Clause1),
    get_clause_from_node_id_atom(Id2, Clause2),
    negate_clause_to_conj(Clause2, Id2Conj),
    maplist(append(Clause1), Id2Conj, CNF).

disjunct_ids_to_cnf(Id1, Id2, CNF) :-
    get_clause_from_node_id_atom(Id1, Clause1),
    get_clause_from_node_id_atom(Id2, Clause2),
    append(Clause1, Clause2, NewClause),
    CNF = [NewClause].

get_clause_from_node_id(Id, Clause) :-
    sat_clause(Id, TClause),
    !,
    Clause = TClause.

get_clause_from_node_id(Id, Clause) :-
    seen(SatVarName,Pol,Id), % TO DO: improve search by Id
    Clause = [Pol-_-SatVarName].

get_clause_from_node_id_atom(IdAtom, Clause) :-
    number_to_atom(NId, IdAtom),
    get_clause_from_node_id(NId, Clause).

get_clauses_from_bliss_cycle(Cycle, EqSatVarNames) :-
    get_clauses_from_bliss_cycle(Cycle, [], EqSatVarNames).

get_clauses_from_bliss_cycle([], Acc, Acc).

get_clauses_from_bliss_cycle([IdA|T], Acc, EqSatVarNames) :-
    get_clause_from_node_id_atom(IdA, Clause),
    get_clauses_from_bliss_cycle(T, [Clause|Acc], EqSatVarNames).

get_equality_from_cycle(Cycle, Acc, NAcc, SAcc, [SatVarName-EqClauses|SAcc], NegEqNodeTriple) :-
    next_sat_var_name(SatVarName),
    PosEqNodeTriple = pred_true-_-SatVarName,
    NegEqNodeTriple = pred_false-_-SatVarName,
    get_equality_from_cycle_cnf(Cycle, PosEqNodeTriple, NegEqNodeTriple, EqCNF),
    get_clauses_from_bliss_cycle(Cycle, EqClauses),
    append(EqCNF, Acc, NAcc).

get_equality_from_cycle_cnf([Id1,Id2], PosEqNodeTriple, NegEqNodeTriple, EqCNF) :-
    % the new SAT variable eq is equivalent to the equality of Id1 & Id2
    % note that non unit clauses might be referenced to ids which requires some rewriting
    disjunct_ids_to_cnf(Id1, not(Id2), TCNF1),
    maplist(append([NegEqNodeTriple]), TCNF1, CNF1),
    disjunct_ids_to_cnf(not(Id1), Id2, TCNF2),
    maplist(append([NegEqNodeTriple]), TCNF2, CNF2),
    append(CNF1, CNF2, CNFLhsImpl),
    disjunct_ids_to_cnf(not(Id1), not(Id2), TCNF3),
    maplist(append([PosEqNodeTriple]), TCNF3, CNF3),
    disjunct_ids_to_cnf(Id1, Id2, TCNF4),
    maplist(append([PosEqNodeTriple]), TCNF4, CNF4),
    append(CNF3, CNF4, CNFRhsImpl),
    append(CNFLhsImpl, CNFRhsImpl, EqCNF). % TO DO: falsity of eq

get_equality_from_cycle_cnf([Id1,Id2,Id3], PosEqNodeTriple, NegEqNodeTriple, EqCNF) :-
    % the new SAT variable eq is equivalent to the equality of Id1 & Id2 & Id3
    disjunct_ids_to_cnf(not(Id1), Id3, TCNF1),
    maplist(append([NegEqNodeTriple]), TCNF1, CNF1),
    disjunct_ids_to_cnf(Id1, not(Id2), TCNF2),
    maplist(append([NegEqNodeTriple]), TCNF2, CNF2),
    disjunct_ids_to_cnf(Id2, not(Id3), TCNF3),
    maplist(append([NegEqNodeTriple]), TCNF3, CNF3),
    append([CNF1,CNF2,CNF3], CNFLhsImpl),
    disjunct_ids_to_cnf(not(Id1), not(Id2), TCNF4),
    maplist(append([PosEqNodeTriple]), TCNF4, TTCNF4),
    get_clause_from_node_id_atom(Id3, Clause3),
    negate_clause_to_conj(Clause3, NegConj3),
    append(TTCNF4, NegConj3, CNF4),
    disjunct_ids_to_cnf(Id1, Id2, TCNF5),
    maplist(append([PosEqNodeTriple]), TCNF5, TTCNF5),
    maplist(append(Clause3), TTCNF5, CNF5),
    append(CNF4, CNF5, CNFRhsImpl),
    append(CNFLhsImpl, CNFRhsImpl, EqCNF).

get_sbps_from_cycle([Id1,Id2], SBPConj) :-
    % not(Id1) or Id2
    get_clause_from_node_id_atom(Id1, Clause1),
    get_clause_from_node_id_atom(Id2, Clause2),
    negate_clause_to_conj(Clause1, NegConj1),
    ( NegConj1 = [Clause2]
    -> SBPConj = [Clause2]
    ; maplist(append(Clause2), NegConj1, SBPConj)
).

get_sbps_from_cycle([Id1,Id2,Id3], SBPConj) :-
    get_sbps_from_cycle([Id1,Id2], SBPConj1),
    get_sbps_from_cycle([Id2,Id3], SBPConj2),
    append(SBPConj1, SBPConj2, SBPConj).

get_sbps_from_generators(Generators, SBPs, NewSatVars) :-
    add_sbps_from_generators(Generators, [], SBPs, [], NewSatVars).

get_symmetry_breaking_predicates(CNF, SBPs, NewSatVars) :-
    bliss_interface:init_bliss_interface,
    bliss_interface:init_undirected_graph,
    cnf_to_colored_graph(CNF),
    bliss_interface:find_automorphisms(Generators),
    nl, write('Generators: '), write(Generators),nl,
    get_sbps_from_generators(Generators, TSBPs, NewSatVars),
    !,
    SBPs = TSBPs.

lit_compare(_-_-A1, _-_-A2) :- A1@<A2.

negate_clause_to_conj(Clause, NegConj) :-
    negate_clause_to_conj(Clause, [], NegConj).

negate_clause_to_conj([], Acc, Acc).

negate_clause_to_conj([Pol-_-SatVarName|T], Acc, NegConj) :-
    negate_polarity(Pol, NegPol),
    negate_clause_to_conj(T, [[NegPol-_-SatVarName]|Acc], NegConj).

negate_polarity(pred_true, pred_false).

negate_polarity(pred_false, pred_true).

number_to_atom(Number, Atom) :-
    number(Number),
    number_codes(Number, Codes),
    atom_codes(Atom, Codes),!.

number_to_atom(Number, Atom) :-
    atom(Atom),
    atom_codes(Atom, Codes),
    number_codes(Number, Codes),!.

register_var_node(Lit, LitIdPos, LitIdNeg) :-
    seen(Lit,pred_true,TLitIdPos),
    seen(Lit,pred_false,TLitIdNeg),
    !,
    LitIdPos = TLitIdPos,
    LitIdNeg = TLitIdNeg.

register_var_node(Lit, LitIdPos, LitIdNeg) :-
    bliss_interface:add_node(2, LitIdPos),
    bliss_interface:add_node(2, LitIdNeg),
    asserta(seen(Lit,pred_true,LitIdPos)),
    asserta(seen(Lit,pred_false,LitIdNeg)),
    bliss_interface:add_edge(LitIdPos, LitIdNeg).