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/