Checking Differential Invariance of Conjunctions of Polynomial Equalities

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^.

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)

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	0.003 True	True	True
	2	1	1	3	True	True	True	True
	3	1	1	3	0.030 True	0.003 True	0.002 True	0.002 True
	4	2	1	2	0.002 True	0.002 True	0.002 True	0.002 True
	5	2	1	4	0.031 True	0.019 True	0.002 True	0.002 True
	6	3	1	3	0.025 True	0.019 True	0.002 True	0.002 True
	7	2	1	5	0.035 True	0.018 True	0.002 True	0.002 True
	8	3	1	2	0.130 True	0.060 True	0.003 True	0.003 True
	9	3	1	2	0.017 True	0.013 True	0.003 True	0.003 True
	10	3	1	2	0.021 True	0.014 True	0.002 True	0.002 True
	11	4	1	4	Timeout	Timeout	0.005 True	0.004 True
	12	4	1	2	0.025 True	0.020 True	0.004 True	0.004 True
	13	4	1	2	Timeout	1.577 True	0.003 True	0.003 True
	14	5	1	6	Timeout	Timeout	0.005 True	0.005 True
	15	5	1	3	0.493 True	0.603 True	0.005 True	0.005 True
	16	5	1	2	0.251 True	0.058 True	0.004 True	0.004 True

2. Singularities

	Prob.	Dim	d.Inv	d.VF	SoSDRI	SoSDRI-OPT	DRI ∧	DRI ∧-OPT
	1	3	2	3	0.135 True	0.046 True	0.003 True	0.003 True
	2	3	2	3	0.035 True	0.018 True	0.003 True	0.002 True
	3	3	2	1	0.133 True	0.085 True	0.002 True	0.002 True
	4	3	2	3	0.036 True	0.035 True	0.003 True	0.003 True
	5	3	3	2	0.010 True	0.009 True	0.002 True	0.002 True
	6	9	9	8	0.305 True	0.265 True	0.009 True	0.009 True
	7	5	2	4	Timeout	Timeout	0.007 True	0.007 True
	8	9	5	4	10.560 True	10.560 True	0.005 True	0.005 True

3. Higher Integrals

	Prob.	Dim	d.Inv	d.VF	SoSDRI	SoSDRI-OPT	DRI ∧	DRI ∧-OPT
	1	3	2	3	0.460 True	0.125 True	0.004 True	0.003 True
	2	6	2	2	0.002 True	0.002 True	0.002 True	0.002 True
	3	6	3	2	Timeout	Timeout	0.014 True	0.013 True
	4	6	6	2	Timeout	Timeout	Timeout	1.299 False

4. Other conjunctions

	Prob.	Dim	d.Inv	d.VF	SoSDRI	SoSDRI-OPT	DRI ∧	DRI ∧-OPT
	1	3	2	1	0.172 True	0.134 True	0.003 True	0.003 True
	2	6	2	3	Timeout	Timeout	0.008 True	0.006 True
	3	3	6	2	16.520 True	Timeout	0.075 True	0.051 True

All runs

	Prob.	Dim	d.Inv	d.VF	SoSDRI	SoSDRI-OPT	DRI ∧	DRI ∧-OPT
	1	1	1	1	True	True	True	True
	2	1	1	3	True	True	True	True
	3	1	1	3	0.008 True	0.004 True	0.002 True	0.002 True
	4	2	1	2	0.002 True	0.002 True	0.002 True	0.002 True
	5	2	1	4	0.035 True	0.019 True	0.002 True	0.002 True
	6	3	1	3	0.025 True	0.019 True	0.002 True	0.002 True
	7	2	1	5	0.035 True	0.018 True	0.002 True	0.002 True
	8	3	1	2	0.135 True	0.064 True	0.003 True	0.003 True
	9	3	1	2	0.017 True	0.013 True	0.003 True	0.003 True
	10	3	1	2	0.022 True	0.014 True	0.002 True	0.002 True
	11	4	1	4	Timeout	Timeout	0.005 True	0.004 True
	12	4	1	2	0.027 True	0.020 True	0.004 True	0.004 True
	13	4	1	2	Timeout	1.607 True	0.003 True	0.003 True
	14	5	1	6	Timeout	Timeout	0.006 True	0.006 True
	15	5	1	3	0.522 True	0.635 True	0.005 True	0.005 True
	16	5	1	2	0.266 True	0.063 True	0.005 True	0.004 True
	17	3	2	3	0.140 True	0.052 True	0.003 True	0.003 True
	18	3	2	3	0.035 True	0.020 True	0.003 True	0.003 True
	19	3	2	1	0.148 True	0.091 True	0.003 True	0.003 True
	20	3	2	3	0.038 True	0.039 True	0.003 True	0.003 True
	21	3	3	2	0.011 True	0.009 True	0.002 True	0.002 True
	22	9	9	8	0.323 True	0.277 True	0.010 True	0.009 True
	23	5	2	4	Timeout	Timeout	0.007 True	0.007 True
	24	9	5	4	10.580 True	10.580 True	0.005 True	0.005 True
	25	3	2	3	0.475 True	0.133 True	0.004 True	0.004 True
	26	6	2	2	0.002 True	0.002 True	0.003 True	0.002 True
	27	6	3	2	Timeout	Timeout	0.014 True	0.013 True
	28	6	6	2	Timeout	Timeout	Timeout	1.279 False
	29	3	2	1	0.124 True	0.114 True	0.003 True	0.003 True
	30	6	2	3	Timeout	Timeout	0.006 True	0.005 True
	31	3	6	2	16.420 True	Timeout	0.066 True	0.047 True
	32	12	146	291	Timeout	Timeout	Timeout	Timeout

Created with Wolfram Mathematica 9.0