From f5d9a67f3688ec9bb08dd3add05614552e082555 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Mon, 1 Jan 2024 10:26:42 +0100 Subject: [PATCH] ENHANCED: Suspend propagation during filtering in global_cardinality/2. This allows subsequently invoked constraints to take the entire filtering results into account, instead of being invoked when the obtained information is not yet entirely used. The SICStus-style attributed variables mechanism of Scryer Prolog automatically prevents very subtle interaction problems that can arise in systems that do not give all variables that are involved in a unification an opportunity to schedule their propagators. An example of such a subtle interaction is: ?- tuples_in([[A,C,B]], [[3,1,3],[4,2,4]]), global_cardinality([A,B,D], [3-1,4-2]), A = 4. A = 4 causes pgcc_check/1 and pgcc/2 to be queued in the fast and slow queue, respectively. In the fast queue, there is also rel_tuple/2, which is worked off after gcc_check/1 and simultaneously instantiates both C and B (to 2 and 4, respectively). Instantiation of C schedules do_queue//0 from verify_attributes/3. Note that C does not participate in the global_cardinality/2 constraint. Critically, B also gets an opportunity to schedule its propagators in this case, so another gcc_check/1 is run before gcc_global/2! --- src/lib/clpz.pl | 100 ++++++++++++++++++++++++++---------------------- 1 file changed, 54 insertions(+), 46 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index a26e1e42..9ac73745 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -3,7 +3,7 @@ Author: Markus Triska E-mail: triska@metalevel.at WWW: https://www.metalevel.at - Copyright (C): 2016-2023 Markus Triska + Copyright (C): 2016-2024 Markus Triska This library provides CLP(ℤ): @@ -2750,20 +2750,24 @@ propagator_init_trigger(Vs, P) :- prop_init(Prop, V) :- init_propagator(V, Prop). geq(A, B) :- - ( fd_get(A, AD, APs) -> - domain_infimum(AD, AI), - ( fd_get(B, BD, _) -> - domain_supremum(BD, BS), - ( AI cis_geq BS -> true + new_queue(Q), + phrase((geq(A, B),do_queue), [Q], _). + +geq(A, B) --> + ( { fd_get(A, AD, APs) } -> + { domain_infimum(AD, AI) }, + ( { fd_get(B, BD, _) } -> + { domain_supremum(BD, BS) }, + ( { AI cis_geq BS } -> true ; propagator_init_trigger(pgeq(A,B)) ) - ; ( AI cis_geq n(B) -> true - ; domain_remove_smaller_than(AD, B, AD1), + ; ( { AI cis_geq n(B) } -> true + ; { domain_remove_smaller_than(AD, B, AD1) }, fd_put(A, AD1, APs) ) ) - ; fd_get(B, BD, BPs) -> - domain_remove_greater_than(BD, A, BD1), + ; { fd_get(B, BD, BPs) } -> + { domain_remove_greater_than(BD, A, BD1) }, fd_put(B, BD1, BPs) ; A >= B ). @@ -4224,9 +4228,6 @@ activate_propagator(propagator(P,State)) --> ) ). -enable_queue :- true. % NOP -disable_queue :- true. % NOP - %do_queue --> print_queue, { false }. do_queue --> ( queue_enabled -> @@ -4510,13 +4511,13 @@ run_propagator(pelement(N, Is, V), MState) --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -run_propagator(pgcc_single(Vs, Pairs), _) --> { gcc_global(Vs, Pairs) }. +run_propagator(pgcc_single(Vs, Pairs), _) --> gcc_global(Vs, Pairs). -run_propagator(pgcc_check_single(Pairs), _) --> { gcc_check(Pairs) }. +run_propagator(pgcc_check_single(Pairs), _) --> gcc_check(Pairs). -run_propagator(pgcc_check(Pairs), _) --> { gcc_check(Pairs) }. +run_propagator(pgcc_check(Pairs), _) --> gcc_check(Pairs). -run_propagator(pgcc(Vs, _, Pairs), _) --> { gcc_global(Vs, Pairs) }. +run_propagator(pgcc(Vs, _, Pairs), _) --> gcc_global(Vs, Pairs). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -6791,13 +6792,20 @@ gcc_pairs([Key-Num0|KNs], Vs, [Key-Num|Rest]) :- Constraint", AAAI-96 Portland, OR, USA, pp 209--215, 1996 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ -gcc_global(Vs, KNs) :- - gcc_check(KNs), - % previously: call do_queue/0 (now a NOP) here to reach a - % fix-point: all elements of clpz_gcc_vs must be variables. We - % must ensure this holds if gcc_check/1 is later rewritten to - % actually disable the queue. - with_local_attributes(Vs, +gcc_global(Vs, KNs) --> + % at this point, all elements of clpz_gcc_vs must be + % variables, which a previously scheduled and called + % gcc_check//1 ensures. Note that gcc_check//1 disables the + % queue and accumulates constraints in the queue. Do we need + % to insert a call of do_queue//0 here to reach a fixpoint? I + % think not, because verify_attributes/3 gives each variable + % that is involved in a unification an opportunity to schedule + % its propagators, even if the unifications happen + % simultaneously (such as [A,B] = [0,1], which can happen in + % the propagator of tuples_in/2). Hence: We need this only if + % an example shows it, ideally found by a systematic search + % that can be used to test the implementation. + { with_local_attributes(Vs, (gcc_arcs(KNs, S, Vals), variables_with_num_occurrences(Vs, VNs), maplist(target_to_v(T), VNs), @@ -6808,9 +6816,9 @@ gcc_global(Vs, KNs) :- gcc_consistent(T), scc(Vals, gcc_successors), phrase(gcc_goals(Vals), Gs) - ; Gs = [] )), Gs), + ; Gs = [] )), Gs) }, disable_queue, - maplist(call, Gs), + neq_nums(Gs), enable_queue. gcc_consistent(T) :- @@ -6837,7 +6845,7 @@ gcc_edge_goal(arc_to(_,_,V,F), Val) --> get_attr(Val, lowlink, L2), L1 =\= L2, get_attr(Val, value, Value) } -> - [clpz:neq_num(V, Value)] + [neq_num(V, Value)] ; [] ). @@ -7007,7 +7015,7 @@ gcc_succ_edge(arc_from(_,_,V,F)) --> consistency. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ -gcc_check(Pairs) :- +gcc_check(Pairs) --> disable_queue, gcc_check_(Pairs), enable_queue. @@ -7017,36 +7025,36 @@ gcc_done(Num) :- del_attr(Num, clpz_gcc_num), del_attr(Num, clpz_gcc_occurred). -gcc_check_([]). -gcc_check_([Key-Num0|KNs]) :- - ( get_attr(Num0, clpz_gcc_vs, Vs) -> - get_attr(Num0, clpz_gcc_num, Num), - get_attr(Num0, clpz_gcc_occurred, Occ0), - vs_key_min_others(Vs, Key, 0, Min, Os), - put_attr(Num0, clpz_gcc_vs, Os), - put_attr(Num0, clpz_gcc_occurred, Occ1), - Occ1 is Occ0 + Min, +gcc_check_([]) --> []. +gcc_check_([Key-Num0|KNs]) --> + ( { get_attr(Num0, clpz_gcc_vs, Vs) } -> + { get_attr(Num0, clpz_gcc_num, Num), + get_attr(Num0, clpz_gcc_occurred, Occ0), + vs_key_min_others(Vs, Key, 0, Min, Os), + put_attr(Num0, clpz_gcc_vs, Os), + put_attr(Num0, clpz_gcc_occurred, Occ1), + Occ1 is Occ0 + Min }, geq(Num, Occ1), % The queue is disabled for efficiency here in any case. % If it were enabled, make sure to retain the invariant % that gcc_global is never triggered during an % inconsistent state (after gcc_done/1 but before all % relevant constraints are posted). - ( Occ1 == Num -> all_neq(Os, Key), gcc_done(Num0) - ; Os == [] -> gcc_done(Num0), Num = Occ1 - ; length(Os, L), - Max is Occ1 + L, + ( Occ1 == Num -> all_neq(Os, Key), { gcc_done(Num0) } + ; Os == [] -> { gcc_done(Num0) }, Num = Occ1 + ; { length(Os, L), + Max is Occ1 + L }, geq(Max, Num), - ( nonvar(Num) -> Diff is Num - Occ1 - ; fd_get(Num, ND, _), - domain_infimum(ND, n(NInf)), + ( { nonvar(Num) } -> Diff is Num - Occ1 + ; { fd_get(Num, ND, _), + domain_infimum(ND, n(NInf)) }, Diff is NInf - Occ1 ), L >= Diff, ( L =:= Diff -> Num is Occ1 + Diff, - maplist(=(Key), Os), - gcc_done(Num0) + { maplist(=(Key), Os), + gcc_done(Num0) } ; true ) ) -- 2.54.0