Re: [eclipse-clp-users] Query reformulation to achieve better propagation

From: Marco Gavanelli <marco.gavanelli_at_...17...>
Date: Mon, 20 Feb 2023 12:54:33 +0100
Hi,

On 20/02/2023 11:27, Panagiotis Stamatopoulos wrote:
> Hello Everybody,
> 
> After having loaded libraries ic and ic_global, we give the query:
> 
> ?- N = 4, Count = 0, length(L, N), L #:: 1..N, 
> ic_global:alldifferent(L), L = [X1,X2,X3,X4], (X2 #> X1) + (X3 #> 
> max([X1,X2])) + (X4 #> max([X1,X2,X3])) #= Count.
> 
> N = 4
> Count = 0
> L = [X1{1 .. 4}, X2{1 .. 4}, X3{1 .. 4}, X4{1 .. 4}]
> X1 = X1{1 .. 4}
> X2 = X2{1 .. 4}
> X3 = X3{1 .. 4}
> X4 = X4{1 .. 4}
> There are 6 delayed goals.
> Yes (0.00s cpu)
> 
> As we may see, from the query we can infer that X1 = 4. Is there
> any alternative way to pose the query in order to get this result?
> Note that Count might be anything between 0 and 3 (if we assign it
> the value 3, we get the answer X1 = 1, X2 = 2, X3 = 3, X4 = 4,
> as we might expect). But what if Count is less than 3? How could
> we get the most propagation possible?

With Count=0 the solver infers that
	(X2 #> X1) #= 0
i.e.
	 X2 #=< X1

I guess you would like to combine that information with the alldifferent 
constraint, and obtain the stronger constraint

	X2 #< X1.

One way to achieve this propagation could be to use, instead of the #< 
/3 constraint, a constraint that excludes the possibility of having X2 = 
X1 (i.e., either X1 < X2 or X2 > X1). For example:

:- lib(propia).
mygt(X,Y,B):- mygt1(X,Y,B) infers most.
mygt1(A,B,1):- A #> B.
mygt1(A,B,0):- A #< B.

Now this constraint can be used instead of #< /3 :

?- N=4, Count=0, L = [X1,X2,X3,X4], length(L, N), L #:: 1..N, 
ic_global:alldifferent(L), mygt(X2,X1,B1), M12 #= max([X1,X2]), 
mygt(X3,M12,B2), M123 #= max([X1,X2,X3]), mygt(X4,M123,B3), 
sumlist([B1,B2,B3]) #= Count.

N = 4
Count = 0
L = [4, X2{1 .. 3}, X3{1 .. 3}, X4{1 .. 3}]
X1 = 4
X2 = X2{1 .. 3}
X3 = X3{1 .. 3}
X4 = X4{1 .. 3}
B1 = 0
M12 = 4
B2 = 0
M123 = 4
B3 = 0


Delayed goals:
	mygt1(X2{1 .. 3}, 4, 0) infers most
	mygt1(X3{1 .. 3}, 4, 0) infers most
	mygt1(X4{1 .. 3}, 4, 0) infers most
	alldifferent([X2{1 .. 3}, X3{1 .. 3}, X4{1 .. 3}], 1)
Yes (0.00s cpu)

Cheers,
Marco

-- 
Marco Gavanelli
Coordinator of the courses
-L8 Electronics and Computer Science Engineering
-LM29 Electronics Engineering for ICT
-LM32 Computer Science and Automation Engineering
Associate Professor
Ph.D. in Computer Science Engineering
Dept of Engineering
University of Ferrara
Tel/Fax  +39-0532-97-4833
http://docente.unife.it/marco.gavanelli
Received on Mon Feb 20 2023 - 12:25:22 CET

This archive was generated by hypermail 2.3.0 : Tue Apr 16 2024 - 09:13:20 CEST