MIP or PIP for testing satisfiability of linear arithmetic constraints over the integers
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/
Il 09/07/2011 16:44, Fred Mesnard ha scritto:
Hi all,
Hello Fred.
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?
The MIP_Problem solver is based on a branch&bound strategy and may loop when trying to identify a feasible/optimal solution satisfying the integrality constraints.
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?
Quoting from PIP_Problem documentation:
Note that all problem variables and problem parameters are assumed to take non-negative integer values, so that there is no need to specify non-negativity constraints.
Cheers, Enea.
Cordialement, Fred Mesnard http://personnel.univ-reunion.fr/fred/
PPL-devel mailing list PPL-devel@cs.unipr.it http://www.cs.unipr.it/mailman/listinfo/ppl-devel
participants (2)
-
Enea Zaffanella -
Fred Mesnard