ENHANCED: CLP(ℤ): Reduce redundant propagator invocations during all_distinct/1 filtering

First, the current propagator is now logged and not re-triggered
during filtering. Second, and more significantly, all neq_num/2
constraints are scheduled and processed before more global constraints
are invoked. In this way, all the distilled information can be taken
into account by subsequently invoked global constraints.

These changes yield a 3-fold improvement in several Sudoku instances,
and a significant runtime reduction in social golfer instance 8-4-9.
This commit is contained in:
Markus Triska
2022-07-25 20:08:54 +02:00
committed by Mark Thom
parent 4422ffe39f
commit c7caf6b7a9

View File

@@ -123,6 +123,8 @@
:- use_module(library(si)). :- use_module(library(si)).
:- use_module(library(freeze)). :- use_module(library(freeze)).
:- use_module(library(arithmetic)). :- use_module(library(arithmetic)).
:- use_module(library(debug)).
:- use_module(library(format)).
% :- use_module(library(types)). % :- use_module(library(types)).
@@ -2241,8 +2243,8 @@ all_distinct(Ls) :-
fd_must_be_list(Ls, all_distinct(Ls)-1), fd_must_be_list(Ls, all_distinct(Ls)-1),
maplist(fd_variable, Ls), maplist(fd_variable, Ls),
make_propagator(pdistinct(Ls), Prop), make_propagator(pdistinct(Ls), Prop),
distinct_attach(Ls, Prop, []), new_queue(Q0),
trigger_once(Prop). phrase((distinct_attach(Ls, Prop, []),trigger_prop(Prop),do_queue), [Q0], _).
%% nvalue(?N, +Vars). %% nvalue(?N, +Vars).
% %
@@ -4050,12 +4052,13 @@ trigger_props(fd_props(Gs,Bs,Os)) -->
trigger_props_([]) --> []. trigger_props_([]) --> [].
trigger_props_([P|Ps]) --> trigger_prop(P), trigger_props_(Ps). trigger_props_([P|Ps]) --> trigger_prop(P), trigger_props_(Ps).
trigger_prop(_P) :- true. % TODO: What to do? trigger_prop(P) :- trigger_once(P).
trigger_prop(Propagator) --> trigger_prop(Propagator) -->
{ propagator_state(Propagator, State) }, { propagator_state(Propagator, State) },
( { State == dead } -> [] ( { State == dead } -> []
; { get_attr(State, clpz_aux, queued) } -> [] ; { get_attr(State, clpz_aux, queued) } -> []
; { bb_get('$clpz_current_propagator', C), C == State } -> []
; % passive ; % passive
%{ format("triggering: ~w\n", [Propagator]) }, %{ format("triggering: ~w\n", [Propagator]) },
{ put_attr(State, clpz_aux, queued) }, { put_attr(State, clpz_aux, queued) },
@@ -4148,12 +4151,13 @@ no_reactivation(pgcc_single(_,_)).
%no_reactivation(scalar_product(_,_,_,_)). %no_reactivation(scalar_product(_,_,_,_)).
activate_propagator(propagator(P,State)) --> activate_propagator(propagator(P,State)) -->
% { portray_clause(running(P)) },
( State == dead -> [] ( State == dead -> []
; { del_attr(State, clpz_aux) }, ; { del_attr(State, clpz_aux) },
( { no_reactivation(P) } -> ( { no_reactivation(P) } ->
%b_setval('$clpz_current_propagator', State), TODO { bb_b_put('$clpz_current_propagator', State) },
run_propagator(P, State) run_propagator(P, State),
%b_setval('$clpz_current_propagator', []) { bb_b_put('$clpz_current_propagator', []) }
; run_propagator(P, State) ; run_propagator(P, State)
) )
). ).
@@ -4199,7 +4203,8 @@ queue_get_arg_(Queue, Which, Element) :-
). ).
queue_enabled --> state(queue(_,_,_,Aux)), { \+ get_atts(Aux, +enabled(false)) }. queue_enabled --> state(queue(_,_,_,Aux)), { \+ get_atts(Aux, +enabled(false)) }.
disable_queue --> state(queue(_,_,_,Aux)), { put_atts(Aux, +enabled(false)) }.
enable_queue --> state(queue(_,_,_,Aux)), { put_atts(Aux, +enabled(true)) }.
portray_propagator(propagator(P,_), F) :- functor(P, F, _). portray_propagator(propagator(P,_), F) :- functor(P, F, _).
@@ -4394,14 +4399,14 @@ run_propagator(pdifferent(Left,Right,X,_), MState) -->
run_propagator(pexclude(Left,Right,X), MState). run_propagator(pexclude(Left,Right,X), MState).
run_propagator(pexclude(Left,Right,X), _) --> run_propagator(pexclude(Left,Right,X), _) -->
{ ( ground(X) -> ( ground(X) ->
disable_queue, disable_queue,
exclude_fire(Left, Right, X), exclude_fire(Left, Right, X),
enable_queue enable_queue
; true ; true
) }. ).
run_propagator(pdistinct(Ls), _MState) --> { distinct(Ls) }. run_propagator(pdistinct(Ls), _MState) --> distinct(Ls).
run_propagator(pnvalue(N, Vars), _MState) --> { propagate_nvalue(N, Vars) }. run_propagator(pnvalue(N, Vars), _MState) --> { propagate_nvalue(N, Vars) }.
@@ -4435,8 +4440,8 @@ run_propagator(pgcc(Vs, _, Pairs), _) --> { gcc_global(Vs, Pairs) }.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
run_propagator(pcircuit(Vs), _MState) --> run_propagator(pcircuit(Vs), _MState) -->
{ distinct(Vs), distinct(Vs),
propagate_circuit(Vs) }. { propagate_circuit(Vs) }.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -5933,12 +5938,12 @@ max_factor(L1, U1, L2, U2, Max) :-
CSPs", AAAI-94, Seattle, WA, USA, pp 362--367, 1994 CSPs", AAAI-94, Seattle, WA, USA, pp 362--367, 1994
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
distinct_attach([], _, _). distinct_attach([], _, _) --> [].
distinct_attach([X|Xs], Prop, Right) :- distinct_attach([X|Xs], Prop, Right) -->
( var(X) -> ( var(X) ->
init_propagator(X, Prop), { init_propagator(X, Prop),
make_propagator(pexclude(Xs,Right,X), P1), make_propagator(pexclude(Xs,Right,X), P1),
init_propagator(X, P1), init_propagator(X, P1) },
trigger_prop(P1) trigger_prop(P1)
; exclude_fire(Xs, Right, X) ; exclude_fire(Xs, Right, X)
), ),
@@ -6158,8 +6163,8 @@ with_local_attributes(Vars, Goal, Result) :-
local_attributes(Result,Vars), local_attributes(Result,Vars),
true). true).
distinct(Vars) :- distinct(Vars) -->
with_local_attributes(Vars, { with_local_attributes(Vars,
( difference_arcs(Vars, FreeLeft, FreeRight0), ( difference_arcs(Vars, FreeLeft, FreeRight0),
length(FreeLeft, LFL), length(FreeLeft, LFL),
length(FreeRight0, LFR), length(FreeRight0, LFR),
@@ -6170,11 +6175,16 @@ distinct(Vars) :-
maplist(g_g0, FreeLeft), maplist(g_g0, FreeLeft),
scc(FreeLeft, g0_successors), scc(FreeLeft, g0_successors),
maplist(dfs_used, FreeRight), maplist(dfs_used, FreeRight),
phrase(distinct_goals(FreeLeft), Gs)), Gs), phrase(distinct_goals(FreeLeft), Gs)), Gs) },
disable_queue, disable_queue,
maplist(call, Gs), neq_nums(Gs),
enable_queue. enable_queue.
neq_nums([]) --> [].
neq_nums([neq_num(V,N)|VNs]) -->
% { portray_clause(neq_num(V, N)) },
neq_num(V, N), neq_nums(VNs).
distinct_goals([]) --> []. distinct_goals([]) --> [].
distinct_goals([V|Vs]) --> distinct_goals([V|Vs]) -->
{ get_attr(V, edges, Es) }, { get_attr(V, edges, Es) },
@@ -6189,7 +6199,7 @@ distinct_goals_([flow_to(F,To)|Es], V) -->
get_attr(To, lowlink, L2), get_attr(To, lowlink, L2),
L1 =\= L2 } -> L1 =\= L2 } ->
{ get_attr(To, value, N) }, { get_attr(To, value, N) },
[clpz:neq_num(V, N)] [neq_num(V, N)]
; [] ; []
), ),
distinct_goals_(Es, V). distinct_goals_(Es, V).
@@ -6381,6 +6391,10 @@ exclude_fire(Left, Right, E) :-
all_neq(Left, E), all_neq(Left, E),
all_neq(Right, E). all_neq(Right, E).
exclude_fire(Left, Right, E) -->
all_neq(Left, E),
all_neq(Right, E).
list_contains([X|Xs], Y) :- list_contains([X|Xs], Y) :-
( X == Y -> true ( X == Y -> true
; list_contains(Xs, Y) ; list_contains(Xs, Y)
@@ -6942,6 +6956,11 @@ vs_key_min_others([V|Vs], Key, Min0, Min, Others) :-
) )
). ).
all_neq([], _) --> [].
all_neq([X|Xs], C) -->
neq_num(X, C),
all_neq(Xs, C).
all_neq([], _). all_neq([], _).
all_neq([X|Xs], C) :- all_neq([X|Xs], C) :-
neq_num(X, C), neq_num(X, C),
@@ -6973,8 +6992,8 @@ circuit(Vs) :-
( L =:= 1 -> true ( L =:= 1 -> true
; neq_index(Vs, 1), ; neq_index(Vs, 1),
make_propagator(pcircuit(Vs), Prop), make_propagator(pcircuit(Vs), Prop),
distinct_attach(Vs, Prop, []), new_queue(Q0),
trigger_once(Prop) phrase((distinct_attach(Vs, Prop, []),trigger_prop(Prop),do_queue), [Q0], _)
). ).
neq_index([], _). neq_index([], _).