adaptive_cruise_control_non_linear_2026: 18/50 instances have an infeasible (empty) input region

[ttj]

Hi — while running NNV against adaptive_cruise_control_non_linear_2026 we found that 18 of the 50 instances appear to specify an EMPTY input region, i.e. the conjunction of the input constraints is infeasible, so no input point exists. We wanted to flag this with the benchmark proposer in case it is unintended — typically a benchmark instance is expected to have a non-empty input set.

Every instance includes the nonlinear input constraint

(assert (and (> X[0,0] 0.0) (>= (* X[0,0] 200.0) (* X[0,1] X[0,1]))))   ; 200·x0 ≥ x1²

For the 18 instances below, the per-instance box places x1 far enough from 0 that min(x1²) over the box exceeds max(200·x0) = 200·x0_hi, so 200·x0 ≥ x1² can never hold and the input region is empty:

instance	x0 ∈	x1 ∈	max 200·x0	min x1²	empty because
instance_4	[0, 20]	[160, 200]	4000	25600	200·x0 ≤ 4000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_9	[0, 20]	[-200, -160]	4000	25600	200·x0 ≤ 4000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_10	[0, 20]	[80, 120]	4000	6400	200·x0 ≤ 4000 < 6400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_12	[20, 40]	[-160, -120]	8000	14400	200·x0 ≤ 8000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_14	[0, 20]	[-160, -120]	4000	14400	200·x0 ≤ 4000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_16	[80, 100]	[160, 200]	20000	25600	200·x0 ≤ 20000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_17	[40, 60]	[-200, -160]	12000	25600	200·x0 ≤ 12000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_19	[40, 60]	[160, 200]	12000	25600	200·x0 ≤ 12000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_23	[20, 40]	[120, 160]	8000	14400	200·x0 ≤ 8000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_25	[40, 60]	[-160, -120]	12000	14400	200·x0 ≤ 12000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_27	[20, 40]	[-200, -160]	8000	25600	200·x0 ≤ 8000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_31	[0, 20]	[-120, -80]	4000	6400	200·x0 ≤ 4000 < 6400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_35	[80, 100]	[-200, -160]	20000	25600	200·x0 ≤ 20000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_36	[40, 60]	[120, 160]	12000	14400	200·x0 ≤ 12000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_38	[60, 80]	[160, 200]	16000	25600	200·x0 ≤ 16000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_39	[20, 40]	[160, 200]	8000	25600	200·x0 ≤ 8000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_42	[60, 80]	[-200, -160]	16000	25600	200·x0 ≤ 16000 < 25600 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible
instance_45	[0, 20]	[120, 160]	4000	14400	200·x0 ≤ 4000 < 14400 ≤ x1² ⇒ 200·x0 ≥ x1² infeasible

How it was detected: interval arithmetic over the input constraints (using the official vnnlib parser's AST), cross-checked against a dense grid of the box — no grid point satisfies the nonlinear constraint for any of the 18.

Questions for the proposer:

1. Are these 18 instances intended to have an empty input region? (An empty input set makes the property hold vacuously, which we'd report as unsat.)
2. If not, should the x1 ranges be tightened toward 0, or the 200·x0 ≥ x1² constant adjusted, so the input set is non-empty?

Happy to share the exact per-instance parse/IA check if useful. Thanks!

[ttj]

Tagging who it seems is proposer: @lukasmrohwer from source https://github.com/lukasmrohwer/acc-non-linear-properties-benchmark

[lukasmrohwer]

Hi @ttj, thanks for bringing this up. I was actually aware that some instances might have empty input regions through the method in which I partitioned the input variables into sub-regions.

To answer your questions, I did intend this behaviour since the solver would simply return unsat for those instances, as you mentioned. If necessary, I can attempt to filter the input sub-regions for non-empty inputs, however I am aware that the final deadline is coming up very shortly.

[ttj]

So, I guess okay for now given intended and deadline. However, if I understand, in these cases, the neural parts essentially are irrelevant, beyond understanding what inputs mean? Eg, one doesn't really need a neural network verifier to check these specs?

I suppose it's an interesting edge case given the increasing complexity of spec language, as one could imagine a user writing/generating unsat input constraints (or output constraints), and if sufficiently complicated, tools could need to detect and handle such cases.

[lukasmrohwer]

Yes, in these cases, the neural parts are essentially irrelevant. It would make sense to remove these types of instances in the future, but you are right, it does bring up an interesting edge case.