Checking Differential Invariance of Conjunctions of Polynomial Equalities

The source files and examples (Mathematica™ Package) can be found here.

We experimentally compare DRI-based proof rules on a heterogeneous collection of 32 candidates encoded as a conjunction of polynomials.

The four proof rules are:

  1. SoSDRI: Using DRI with sum-of-squares.
  2. SoSDRI-OPT: Optimized SoSDRI.
  3. DRI^: New proof rule for conjunction of polynomial equalities.
  4. DRI^-OPT: Optimized DRI^.

The full set of benchmarks is sub-divided into 4 classes of invariant sets that were used in the experiments:
  1. isolated equilibria (zeros of the vector field)
  2. other singularities
  3. high integrals, which are conceptually harder for all the proof rules considered
  4. abstract examples (either random conjunctions or hand crafted)
Generally, we observe DRI^ out-performing SoSDRI. The optimized versions perform slightly better on average.

The dimension of the vector field is given under Dim in the tables below. Also shown are the polynomial degree of the invariant candidate d.Inv and the degree of the vector field d.VF defined as the maximum degree of all the polynomials of the vector field. True means that the proof rule was able to prove the invariance of the candidate, otherwise it prints False as all proof rules here are necessary and sufficient. The time out is set to 60s per rule per problem. The benchmarks of different classes are available below. Time is given in second.

Figures compare the number of invariant varieties which each rule could prove within 60 seconds. The vertical axis shows cumulative time spent on the problems (log scale).

1. Equilibria

Prob. Dim d.Inv d.VF SoSDRI SoSDRI-OPT DRI ∧ DRI ∧-OPT
1 1 1 1
0.013
True SoSDRI_vs_DRIConj_11.gif
0.003
True SoSDRI_vs_DRIConj_12.gif
SoSDRI_vs_DRIConj_13.gif
True SoSDRI_vs_DRIConj_14.gif
SoSDRI_vs_DRIConj_15.gif
True SoSDRI_vs_DRIConj_16.gif
2 1 1 3
SoSDRI_vs_DRIConj_17.gif
True SoSDRI_vs_DRIConj_18.gif
SoSDRI_vs_DRIConj_19.gif
True SoSDRI_vs_DRIConj_20.gif
SoSDRI_vs_DRIConj_21.gif
True SoSDRI_vs_DRIConj_22.gif
SoSDRI_vs_DRIConj_23.gif
True SoSDRI_vs_DRIConj_24.gif
3 1 1 3
0.030
True SoSDRI_vs_DRIConj_25.gif
0.003
True SoSDRI_vs_DRIConj_26.gif
0.002
True SoSDRI_vs_DRIConj_27.gif
0.002
True SoSDRI_vs_DRIConj_28.gif
4 2 1 2
0.002
True SoSDRI_vs_DRIConj_29.gif
0.002
True SoSDRI_vs_DRIConj_30.gif
0.002
True SoSDRI_vs_DRIConj_31.gif
0.002
True SoSDRI_vs_DRIConj_32.gif
5 2 1 4
0.031
True SoSDRI_vs_DRIConj_33.gif
0.019
True SoSDRI_vs_DRIConj_34.gif
0.002
True SoSDRI_vs_DRIConj_35.gif
0.002
True SoSDRI_vs_DRIConj_36.gif
6 3 1 3
0.025
True SoSDRI_vs_DRIConj_37.gif
0.019
True SoSDRI_vs_DRIConj_38.gif
0.002
True SoSDRI_vs_DRIConj_39.gif
0.002
True SoSDRI_vs_DRIConj_40.gif
7 2 1 5
0.035
True SoSDRI_vs_DRIConj_41.gif
0.018
True SoSDRI_vs_DRIConj_42.gif
0.002
True SoSDRI_vs_DRIConj_43.gif
0.002
True SoSDRI_vs_DRIConj_44.gif
8 3 1 2
0.130
True SoSDRI_vs_DRIConj_45.gif
0.060
True SoSDRI_vs_DRIConj_46.gif
0.003
True SoSDRI_vs_DRIConj_47.gif
0.003
True SoSDRI_vs_DRIConj_48.gif
9 3 1 2
0.017
True SoSDRI_vs_DRIConj_49.gif
0.013
True SoSDRI_vs_DRIConj_50.gif
0.003
True SoSDRI_vs_DRIConj_51.gif
0.003
True SoSDRI_vs_DRIConj_52.gif
10 3 1 2
0.021
True SoSDRI_vs_DRIConj_53.gif
0.014
True SoSDRI_vs_DRIConj_54.gif
0.002
True SoSDRI_vs_DRIConj_55.gif
0.002
True SoSDRI_vs_DRIConj_56.gif
11 4 1 4
SoSDRI_vs_DRIConj_57.gif
Timeout
SoSDRI_vs_DRIConj_58.gif
Timeout
0.005
True SoSDRI_vs_DRIConj_59.gif
0.004
True SoSDRI_vs_DRIConj_60.gif
12 4 1 2
0.025
True SoSDRI_vs_DRIConj_61.gif
0.020
True SoSDRI_vs_DRIConj_62.gif
0.004
True SoSDRI_vs_DRIConj_63.gif
0.004
True SoSDRI_vs_DRIConj_64.gif
13 4 1 2
SoSDRI_vs_DRIConj_65.gif
Timeout
1.577
True SoSDRI_vs_DRIConj_66.gif
0.003
True SoSDRI_vs_DRIConj_67.gif
0.003
True SoSDRI_vs_DRIConj_68.gif
14 5 1 6
SoSDRI_vs_DRIConj_69.gif
Timeout
SoSDRI_vs_DRIConj_70.gif
Timeout
0.005
True SoSDRI_vs_DRIConj_71.gif
0.005
True SoSDRI_vs_DRIConj_72.gif
15 5 1 3
0.493
True SoSDRI_vs_DRIConj_73.gif
0.603
True SoSDRI_vs_DRIConj_74.gif
0.005
True SoSDRI_vs_DRIConj_75.gif
0.005
True SoSDRI_vs_DRIConj_76.gif
16 5 1 2
0.251
True SoSDRI_vs_DRIConj_77.gif
0.058
True SoSDRI_vs_DRIConj_78.gif
0.004
True SoSDRI_vs_DRIConj_79.gif
0.004
True SoSDRI_vs_DRIConj_80.gif

SoSDRI_vs_DRIConj_82.gif

2. Singularities

Prob. Dim d.Inv d.VF SoSDRI SoSDRI-OPT DRI ∧ DRI ∧-OPT
1 3 2 3
0.135
True SoSDRI_vs_DRIConj_84.gif
0.046
True SoSDRI_vs_DRIConj_85.gif
0.003
True SoSDRI_vs_DRIConj_86.gif
0.003
True SoSDRI_vs_DRIConj_87.gif
2 3 2 3
0.035
True SoSDRI_vs_DRIConj_88.gif
0.018
True SoSDRI_vs_DRIConj_89.gif
0.003
True SoSDRI_vs_DRIConj_90.gif
0.002
True SoSDRI_vs_DRIConj_91.gif
3 3 2 1
0.133
True SoSDRI_vs_DRIConj_92.gif
0.085
True SoSDRI_vs_DRIConj_93.gif
0.002
True SoSDRI_vs_DRIConj_94.gif
0.002
True SoSDRI_vs_DRIConj_95.gif
4 3 2 3
0.036
True SoSDRI_vs_DRIConj_96.gif
0.035
True SoSDRI_vs_DRIConj_97.gif
0.003
True SoSDRI_vs_DRIConj_98.gif
0.003
True SoSDRI_vs_DRIConj_99.gif
5 3 3 2
0.010
True SoSDRI_vs_DRIConj_100.gif
0.009
True SoSDRI_vs_DRIConj_101.gif
0.002
True SoSDRI_vs_DRIConj_102.gif
0.002
True SoSDRI_vs_DRIConj_103.gif
6 9 9 8
0.305
True SoSDRI_vs_DRIConj_104.gif
0.265
True SoSDRI_vs_DRIConj_105.gif
0.009
True SoSDRI_vs_DRIConj_106.gif
0.009
True SoSDRI_vs_DRIConj_107.gif
7 5 2 4
SoSDRI_vs_DRIConj_108.gif
Timeout
SoSDRI_vs_DRIConj_109.gif
Timeout
0.007
True SoSDRI_vs_DRIConj_110.gif
0.007
True SoSDRI_vs_DRIConj_111.gif
8 9 5 4
10.560
True SoSDRI_vs_DRIConj_112.gif
10.560
True SoSDRI_vs_DRIConj_113.gif
0.005
True SoSDRI_vs_DRIConj_114.gif
0.005
True SoSDRI_vs_DRIConj_115.gif

SoSDRI_vs_DRIConj_117.gif

3. Higher Integrals

Prob. Dim d.Inv d.VF SoSDRI SoSDRI-OPT DRI ∧ DRI ∧-OPT
1 3 2 3
0.460
True SoSDRI_vs_DRIConj_119.gif
0.125
True SoSDRI_vs_DRIConj_120.gif
0.004
True SoSDRI_vs_DRIConj_121.gif
0.003
True SoSDRI_vs_DRIConj_122.gif
2 6 2 2
0.002
True SoSDRI_vs_DRIConj_123.gif
0.002
True SoSDRI_vs_DRIConj_124.gif
0.002
True SoSDRI_vs_DRIConj_125.gif
0.002
True SoSDRI_vs_DRIConj_126.gif
3 6 3 2
SoSDRI_vs_DRIConj_127.gif
Timeout
SoSDRI_vs_DRIConj_128.gif
Timeout
0.014
True SoSDRI_vs_DRIConj_129.gif
0.013
True SoSDRI_vs_DRIConj_130.gif
4 6 6 2
SoSDRI_vs_DRIConj_131.gif
Timeout
SoSDRI_vs_DRIConj_132.gif
Timeout
SoSDRI_vs_DRIConj_133.gif
Timeout
1.299
False SoSDRI_vs_DRIConj_134.gif

SoSDRI_vs_DRIConj_136.gif

4. Other conjunctions

Prob. Dim d.Inv d.VF SoSDRI SoSDRI-OPT DRI ∧ DRI ∧-OPT
1 3 2 1
0.172
True SoSDRI_vs_DRIConj_138.gif
0.134
True SoSDRI_vs_DRIConj_139.gif
0.003
True SoSDRI_vs_DRIConj_140.gif
0.003
True SoSDRI_vs_DRIConj_141.gif
2 6 2 3
SoSDRI_vs_DRIConj_142.gif
Timeout
SoSDRI_vs_DRIConj_143.gif
Timeout
0.008
True SoSDRI_vs_DRIConj_144.gif
0.006
True SoSDRI_vs_DRIConj_145.gif
3 3 6 2
16.520
True SoSDRI_vs_DRIConj_146.gif
SoSDRI_vs_DRIConj_147.gif
Timeout
0.075
True SoSDRI_vs_DRIConj_148.gif
0.051
True SoSDRI_vs_DRIConj_149.gif

SoSDRI_vs_DRIConj_151.gif

All runs

4/tr> tr style='vertical-align: baseline;'>
Prob. Dim d.Inv d.VF SoSDRI SoSDRI-OPT DRI ∧ DRI ∧-OPT
1 1 1 1
SoSDRI_vs_DRIConj_154.gif
True SoSDRI_vs_DRIConj_155.gif
SoSDRI_vs_DRIConj_156.gif
True SoSDRI_vs_DRIConj_157.gif
SoSDRI_vs_DRIConj_158.gif
True SoSDRI_vs_DRIConj_159.gif
SoSDRI_vs_DRIConj_160.gif
True SoSDRI_vs_DRIConj_161.gif
2 1 1 3
SoSDRI_vs_DRIConj_162.gif
True SoSDRI_vs_DRIConj_163.gif
SoSDRI_vs_DRIConj_164.gif
True SoSDRI_vs_DRIConj_165.gif
SoSDRI_vs_DRIConj_166.gif
True SoSDRI_vs_DRIConj_167.gif
SoSDRI_vs_DRIConj_168.gif
True SoSDRI_vs_DRIConj_169.gif
3 1 1 3
0.008
True SoSDRI_vs_DRIConj_170.gif
0.004
True SoSDRI_vs_DRIConj_171.gif
0.002
True SoSDRI_vs_DRIConj_172.gif
0.002
True SoSDRI_vs_DRIConj_173.gif
4 2 1 2
0.002
True SoSDRI_vs_DRIConj_174.gif
0.002
True SoSDRI_vs_DRIConj_175.gif
0.002
True SoSDRI_vs_DRIConj_176.gif
0.002
True SoSDRI_vs_DRIConj_177.gif
5 2 1 4
0.035
True SoSDRI_vs_DRIConj_178.gif
0.019
True SoSDRI_vs_DRIConj_179.gif
0.002
True SoSDRI_vs_DRIConj_180.gif
0.002
True SoSDRI_vs_DRIConj_181.gif
6 3 1 3
0.025
True SoSDRI_vs_DRIConj_182.gif
0.019
True SoSDRI_vs_DRIConj_183.gif
0.002
True SoSDRI_vs_DRIConj_184.gif
0.002
True SoSDRI_vs_DRIConj_185.gif
7 2 1 5
0.035
True SoSDRI_vs_DRIConj_186.gif
0.018
True SoSDRI_vs_DRIConj_187.gif
0.002
True SoSDRI_vs_DRIConj_188.gif
0.002
True SoSDRI_vs_DRIConj_189.gif
8 3 1 2
0.135
True SoSDRI_vs_DRIConj_190.gif
0.064
True SoSDRI_vs_DRIConj_191.gif
0.003
True SoSDRI_vs_DRIConj_192.gif
0.003
True SoSDRI_vs_DRIConj_193.gif
9 3 1 2
0.017
True SoSDRI_vs_DRIConj_194.gif
0.013
True SoSDRI_vs_DRIConj_195.gif
0.003
True SoSDRI_vs_DRIConj_196.gif
0.003
True SoSDRI_vs_DRIConj_197.gif
10 3 1 2
0.022
True SoSDRI_vs_DRIConj_198.gif
0.014
True SoSDRI_vs_DRIConj_199.gif
0.002
True SoSDRI_vs_DRIConj_200.gif
0.002
True SoSDRI_vs_DRIConj_201.gif
11 4 1 4
SoSDRI_vs_DRIConj_202.gif
Timeout
SoSDRI_vs_DRIConj_203.gif
Timeout
0.005
True SoSDRI_vs_DRIConj_204.gif
0.004
True SoSDRI_vs_DRIConj_205.gif
12 4 1 2
0.027
True SoSDRI_vs_DRIConj_206.gif
0.020
True SoSDRI_vs_DRIConj_207.gif
0.004
True SoSDRI_vs_DRIConj_208.gif
0.004
True SoSDRI_vs_DRIConj_209.gif
13 4 1 2
SoSDRI_vs_DRIConj_210.gif
Timeout
1.607
True SoSDRI_vs_DRIConj_211.gif
0.003
True SoSDRI_vs_DRIConj_212.gif
0.003
True SoSDRI_vs_DRIConj_213.gif
14 5 1 6
SoSDRI_vs_DRIConj_214.gif
Timeout
SoSDRI_vs_DRIConj_215.gif
Timeout
0.006
True SoSDRI_vs_DRIConj_216.gif
0.006
True SoSDRI_vs_DRIConj_217.gif
15 5 1 3
0.522
True SoSDRI_vs_DRIConj_218.gif
0.635
True SoSDRI_vs_DRIConj_219.gif
0.005
True SoSDRI_vs_DRIConj_220.gif
0.005
True SoSDRI_vs_DRIConj_221.gif
16 5 1 2
0.266
True SoSDRI_vs_DRIConj_222.gif
0.063
True SoSDRI_vs_DRIConj_223.gif
0.005
True SoSDRI_vs_DRIConj_224.gif
0.004
True SoSDRI_vs_DRIConj_225.gif
17 3 2 3
0.140
True SoSDRI_vs_DRIConj_226.gif
0.052
True SoSDRI_vs_DRIConj_227.gif
0.003
True SoSDRI_vs_DRIConj_228.gif
0.003
True SoSDRI_vs_DRIConj_229.gif
18 3 2 3
0.035
True SoSDRI_vs_DRIConj_230.gif
0.020
True SoSDRI_vs_DRIConj_231.gif
0.003
True SoSDRI_vs_DRIConj_232.gif
0.003
True SoSDRI_vs_DRIConj_233.gif
19 3 2 1
0.148
True SoSDRI_vs_DRIConj_234.gif
0.091
True SoSDRI_vs_DRIConj_235.gif
0.003
True SoSDRI_vs_DRIConj_236.gif
0.003
True SoSDRI_vs_DRIConj_237.gif
20 3 2 3
0.038
True SoSDRI_vs_DRIConj_238.gif
0.039
True SoSDRI_vs_DRIConj_239.gif
0.003
True SoSDRI_vs_DRIConj_240.gif
0.003
True SoSDRI_vs_DRIConj_241.gif
21 3 3 2
0.011
True SoSDRI_vs_DRIConj_242.gif
0.009
True SoSDRI_vs_DRIConj_243.gif
0.002
True SoSDRI_vs_DRIConj_244.gif
0.002
True SoSDRI_vs_DRIConj_245.gif
22 9 9 8
0.323
True SoSDRI_vs_DRIConj_246.gif
0.277
True SoSDRI_vs_DRIConj_247.gif
0.010
True SoSDRI_vs_DRIConj_248.gif
0.009
True SoSDRI_vs_DRIConj_249.gif
23 5 2 4
SoSDRI_vs_DRIConj_250.gif
Timeout
SoSDRI_vs_DRIConj_251.gif
Timeout
0.007
True SoSDRI_vs_DRIConj_252.gif
0.007
True SoSDRI_vs_DRIConj_253.gif
24 9 5 4
10.580
True SoSDRI_vs_DRIConj_254.gif
10.580
True SoSDRI_vs_DRIConj_255.gif
0.005
True SoSDRI_vs_DRIConj_256.gif
0.005
True SoSDRI_vs_DRIConj_257.gif
25 3 2 3
0.475
True SoSDRI_vs_DRIConj_258.gif
0.133
True SoSDRI_vs_DRIConj_259.gif
0.004
True SoSDRI_vs_DRIConj_260.gif
0.004
True SoSDRI_vs_DRIConj_261.gif
26 6 2 2
0.002
True SoSDRI_vs_DRIConj_262.gif
0.002
True SoSDRI_vs_DRIConj_263.gif
0.003
True SoSDRI_vs_DRIConj_264.gif
0.002
True SoSDRI_vs_DRIConj_265.gif
27 6 3 2
SoSDRI_vs_DRIConj_266.gif
Timeout
SoSDRI_vs_DRIConj_267.gif
Timeout
0.014
True SoSDRI_vs_DRIConj_268.gif
0.013
True SoSDRI_vs_DRIConj_269.gif
28 6 6 2
SoSDRI_vs_DRIConj_270.gif
Timeout
SoSDRI_vs_DRIConj_271.gif
Timeout
SoSDRI_vs_DRIConj_272.gif
Timeout
1.279
False SoSDRI_vs_DRIConj_273.gif
29 3 2 1
0.124
True SoSDRI_vs_DRIConj_274.gif
0.114
True SoSDRI_vs_DRIConj_275.gif
0.003
True SoSDRI_vs_DRIConj_276.gif
0.003
True SoSDRI_vs_DRIConj_277.gif
30 6 2 3
SoSDRI_vs_DRIConj_278.gif
Timeout
SoSDRI_vs_DRIConj_279.gif
Timeout
0.006
True SoSDRI_vs_DRIConj_280.gif
0.005
True SoSDRI_vs_DRIConj_281.gif
31 3 6 2
16.420
True SoSDRI_vs_DRIConj_282.gif
SoSDRI_vs_DRIConj_283.gif
Timeout
0.066
True SoSDRI_vs_DRIConj_284.gif
0.047
True SoSDRI_vs_DRIConj_285.gif
32 12 146 291
SoSDRI_vs_DRIConj_286.gif
Timeout
SoSDRI_vs_DRIConj_287.gif
Timeout
SoSDRI_vs_DRIConj_288.gif
Timeout
SoSDRI_vs_DRIConj_289.gif
Timeout

SoSDRI_vs_DRIConj_291.gif

Spikey Created with Wolfram Mathematica 9.0