Konrad Trifunovic wrote:
Hi all,
the other tip that I give: if I try to resolve the same polyhedron, but if I make it Closed Polyhedron, then the solver 'contains_integer_point' runs out of memory.
Konrad
Hello.
We made a quick test using your data (the higher dimension data).
The test seems to confirm what was said by Roberto: you should use C_Polyhedron instead of NNC_Polyhedron. If you *need* to use NNC_Polyhedron we will have to do something to improve efficiency, but there seem to be no efficiency problem on your example if you stick to C_Polyhedron.
We made the following test (using the C++ interface): - load your ascii dump into a Pointset_Powerset<NNC_Polyhedron> - re-dumping it out (just to be sure we are making no silly mistakes) - extract the singleton NNC_Polyhedron (ph) from the powerset - convert it into a C_Polyhedron (c_ph) - asking if it contains an integer point (just to be sure that it does not depend on the representation given) - build another copy of c_ph, but using generators - asking again if it contains an integer point
On my notebook (a 64 bit machine), the whole thing takes time:
real 0m0.039s user 0m0.011s sys 0m0.014s
Regarding the memory consumption, I tried the example above after setting
# ulimit -S -v 20000
and it runs to completion (it fails with 19000).
I am attaching the source of the test program (containsintegerpoint2.cc), the input ascii-dump (aaa.dat), and the output we obtain (test.out). Note that the test sources assume the PPL test infrastructure ... let us know if you need a self contained test program.
Cheers, Enea Zaffanella.
size 1 space_dim 18 space_dim 18 -ZE -EM +CM +GM +CS +GS -CP -GP +SC -SG con_sys (up-to-date) topology NOT_NECESSARILY_CLOSED 22 x 20 (not_sorted) index_first_pending 22 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 = 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 0 0 0 -8192 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 -8192 0 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 1 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 > 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 >= 0 0 1 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 -1 > 67100672 0 -1 0 -8192 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 >= 8191 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >= gen_sys (up-to-date) topology NOT_NECESSARILY_CLOSED 12 x 20 (not_sorted) index_first_pending 12 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 C 1 0 8191 0 0 0 8191 0 0 8191 0 0 0 8191 0 1 8191 1 8191 0 C 8192 0 67100672 0 67100671 0 67100672 67100671 0 67092480 0 67100672 0 67092480 67100672 8192 549755797504 8192 549755797504 8192 P 8192 0 67100672 0 67092481 0 67100672 67092481 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 8192 P 8192 0 8192 0 67100671 0 8192 67100671 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 8192 P 8192 0 67100672 0 67092481 0 67100672 67092481 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 0 C 1 0 8191 0 8191 0 8191 8191 0 8191 0 8191 0 8191 8191 1 67108863 1 67108863 0 C 8192 0 67100672 0 0 0 67100672 0 0 0 0 8191 0 0 8191 8192 67100672 8192 67100672 0 C 1 0 0 0 8191 0 0 8191 0 0 0 8191 0 0 8191 1 67100672 1 67100672 0 C 8192 0 67100672 0 0 0 67100672 0 0 67092480 0 1 0 67092480 1 8192 67100672 8192 67100672 8192 P 8192 0 67100672 0 0 0 67100672 0 0 0 0 8191 0 0 8191 8192 67100672 8192 67100672 8192 P 8192 0 8192 0 0 0 8192 0 0 0 0 1 0 0 1 8192 8192 8192 8192 8192 P sat_c 12 x 22 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 0 0 sat_g 3 x 20 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0
=== test01 ===
Loading the ascii dump into NNC pointset powerset pps:
Re-dumping pps (for double checking): size 1 space_dim 18 space_dim 18 -ZE -EM +CM +GM +CS +GS -CP -GP +SC -SG con_sys (up-to-date) topology NOT_NECESSARILY_CLOSED 22 x 20 (not_sorted) index_first_pending 22 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 = 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 0 0 0 -8192 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 -8192 0 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 1 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 > 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 >= 0 0 1 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 -1 > 67100672 0 -1 0 -8192 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 >= 8191 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >=
gen_sys (up-to-date) topology NOT_NECESSARILY_CLOSED 12 x 20 (not_sorted) index_first_pending 12 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 C 1 0 8191 0 0 0 8191 0 0 8191 0 0 0 8191 0 1 8191 1 8191 0 C 8192 0 67100672 0 67100671 0 67100672 67100671 0 67092480 0 67100672 0 67092480 67100672 8192 549755797504 8192 549755797504 8192 P 8192 0 67100672 0 67092481 0 67100672 67092481 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 8192 P 8192 0 8192 0 67100671 0 8192 67100671 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 8192 P 8192 0 67100672 0 67092481 0 67100672 67092481 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 0 C 1 0 8191 0 8191 0 8191 8191 0 8191 0 8191 0 8191 8191 1 67108863 1 67108863 0 C 8192 0 67100672 0 0 0 67100672 0 0 0 0 8191 0 0 8191 8192 67100672 8192 67100672 0 C 1 0 0 0 8191 0 0 8191 0 0 0 8191 0 0 8191 1 67100672 1 67100672 0 C 8192 0 67100672 0 0 0 67100672 0 0 67092480 0 1 0 67092480 1 8192 67100672 8192 67100672 8192 P 8192 0 67100672 0 0 0 67100672 0 0 0 0 8191 0 0 8191 8192 67100672 8192 67100672 8192 P 8192 0 8192 0 0 0 8192 0 0 0 0 1 0 0 1 8192 8192 8192 8192 8192 P
sat_c 12 x 22 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 1 0 0
sat_g 0 x 0
Extracting NNC polyhedron ph from powerset: Pretty printing its constraints: *** ph *** B + 8192*D - R = 0, Q = 1, B + 8192*D - P = 0, O = 1, B + 8192*D - I - 8192*N = 0, I - M = 0, L = 0, B + 8192*D - I - 8192*K = 0, J = 0, H = 0, D - G = 0, B - F = 0, E = 0, C = 0, A = 0, B - I > 0, -B - 8192*D + I >= -67100672, -B >= -8191, I >= 0, D >= 0. Pretty printing its generators: *** ph *** c(O + Q), c(8191*D + 8191*G + 8191*K + 8191*N + O + 67100672*P + Q + 67100672*R), c(8191*B + 8191*F + 8191*I + 8191*M + O + 8191*P + Q + 8191*R), c(8191*B + 8191*D + 8191*F + 8191*G + 8191*I + 8191*K + 8191*M + 8191*N + O + 67108863*P + Q + 67108863*R), p((8192*B + 8192*F + K + N + 8192*O + 8192*P + 8192*Q + 8192*R)/8192), p((8192*B + 67100671*D + 8192*F + 67100671*G + 67100672*K + 67100672*N + 8192*O + 549688705024*P + 8192*Q + 549688705024*R)/8192), p((67100672*B + 67100672*F + 8191*K + 8191*N + 8192*O + 67100672*P + 8192*Q + 67100672*R)/8192), p((67100672*B + 67100672*F + 67092480*I + K + 67092480*M + N + 8192*O + 67100672*P + 8192*Q + 67100672*R)/8192), p((67100672*B + 67092481*D + 67100672*F + 67092481*G + 67100672*K + 67100672*N + 8192*O + 549688705024*P + 8192*Q + 549688705024*R)/8192), p((67100672*B + 67100671*D + 67100672*F + 67100671*G + 67092480*I + 67100672*K + 67092480*M + 67100672*N + 8192*O + 549755797504*P + 8192*Q + 549755797504*R)/8192).
Creating a C_Polyhedron c_ph from ph:
Dumping the C_Polyhedron: space_dim 18 -ZE -EM -CM -GM +CS -GS -CP -GP -SC -SG con_sys (up-to-date) topology NECESSARILY_CLOSED 21 x 19 (not_sorted) index_first_pending 21 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >= 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 = 0 0 1 0 8192 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 = -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 0 0 0 -8192 0 0 0 0 = 0 0 0 0 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 = 0 0 1 0 8192 0 0 0 0 -1 0 -8192 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 = 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 = 0 0 1 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 = 0 0 1 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 >= 67100672 0 -1 0 -8192 0 0 0 0 1 0 0 0 0 0 0 0 0 0 >= 8191 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 >= 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 >=
gen_sys (not_up-to-date) topology NECESSARILY_CLOSED 0 x 0 (sorted) index_first_pending 0
sat_c 0 x 0
sat_g 0 x 0
Pretty printing its constraints: *** c_ph *** B + 8192*D - R = 0, Q = 1, B + 8192*D - P = 0, O = 1, B + 8192*D - I - 8192*N = 0, I - M = 0, L = 0, B + 8192*D - I - 8192*K = 0, J = 0, H = 0, D - G = 0, B - F = 0, E = 0, C = 0, A = 0, B - I >= 0, -B - 8192*D + I >= -67100672, -B >= -8191, I >= 0, D >= 0. Checking for an integer point ... true
Dumping the C_Polyhedron copy: space_dim 18 -ZE -EM -CM -GM -CS +GS -CP -GP -SC -SG con_sys (not_up-to-date) topology NECESSARILY_CLOSED 0 x 0 (sorted) index_first_pending 0
gen_sys (up-to-date) topology NECESSARILY_CLOSED 6 x 19 (not_sorted) index_first_pending 6 8192 0 67100672 0 0 0 67100672 0 0 0 0 8191 0 0 8191 8192 67100672 8192 67100672 P 8192 0 67100672 0 67092481 0 67100672 67092481 0 0 0 67100672 0 0 67100672 8192 549688705024 8192 549688705024 P 1 0 8191 0 8191 0 8191 8191 0 8191 0 8191 0 8191 8191 1 67108863 1 67108863 P 1 0 0 0 8191 0 0 8191 0 0 0 8191 0 0 8191 1 67100672 1 67100672 P 1 0 8191 0 0 0 8191 0 0 8191 0 0 0 8191 0 1 8191 1 8191 P 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 P
sat_c 0 x 0
sat_g 0 x 0
Pretty printing its generators: *** c_ph2 *** p((67100672*B + 67100672*F + 8191*K + 8191*N + 8192*O + 67100672*P + 8192*Q + 67100672*R)/8192), p((67100672*B + 67092481*D + 67100672*F + 67092481*G + 67100672*K + 67100672*N + 8192*O + 549688705024*P + 8192*Q + 549688705024*R)/8192), p(8191*B + 8191*D + 8191*F + 8191*G + 8191*I + 8191*K + 8191*M + 8191*N + O + 67108863*P + Q + 67108863*R), p(8191*D + 8191*G + 8191*K + 8191*N + O + 67100672*P + Q + 67100672*R), p(8191*B + 8191*F + 8191*I + 8191*M + O + 8191*P + Q + 8191*R), p(O + Q). Checking for an integer point ... true