[PPL-devel] MIP or PIP for testing satisfiability of linear arithmetic constraints over the integers

[Fred Mesnard]

Hi all,

I plan to use PPL for testing satisfiability of linear arithmetic constraints over the integers.
I'm using PPL 0.11.2 with the latest SWI-Prolog. I found two unexpected results, see below,
and I'm stuck! I'd like to have your feedback. Thanks in advance!

Fred


With MIP, here's my Prolog code:

z_MIP_satisfiable(Cs) :-
	user:my_term_variables(Cs,Vars),
	length(Vars,Dim),
	user:ppl_new_MIP_Problem_from_space_dimension(Dim,Handle),
	translate_constraints_BT_ppl(Vars,Cs,PPL_Cs,PPL_Vs),
	user:ppl_MIP_Problem_add_constraints(Handle,PPL_Cs),
	user:ppl_MIP_Problem_add_to_integer_space_dimensions(Handle,PPL_Vs),
	(   user:ppl_MIP_Problem_is_satisfiable(Handle)
	->  user:ppl_delete_MIP_Problem(Handle)
	;   user:ppl_delete_MIP_Problem(Handle),
	    fail).

In general, it  works well but
trying 
	z_MIP_satisfiable([X=2*Z, X=2*Y+1]).
ie find X both even and odd does not seem to terminate.

By  the way, which kind of algorithm did you implement for MIP?



With PIP, here's my Prolog code, quite similar to the previous one:

z_PIP_satisfiable(Cs) :-
	user:my_term_variables(Cs,Vars),
	length(Vars,Dim),
	user:ppl_new_PIP_Problem_from_space_dimension(Dim,Handle),
	translate_constraints_BT_ppl(Vars,Cs,PPL_Cs,_PPL_Vs),
	user:ppl_PIP_Problem_add_constraints(Handle,PPL_Cs),
	(   user:ppl_PIP_Problem_is_satisfiable(Handle)
	->  user:ppl_delete_PIP_Problem(Handle)
	;   user:ppl_delete_PIP_Problem(Handle),
	    fail).

Trying
	z_PIP_satisfiable([ X =< -1]).
ie find X less than -1 fails. Idem for -2, -3, ...
So for PIP, variables are all implicitly >= 0?







Cordialement,
Fred Mesnard
http://personnel.univ-reunion.fr/fred/