لمعالجة الحالات المعقدة، نعود إلى نهج التقسيم والسلب لتفكيك التعقيد: بدلًا من عدد قليل من الاستدعاءات المعقدة لـ BaB، نعتمد على عدد كبير من استدعاءات البرمجة الخطية الصحيحة الجزئية (MILP) الصغيرة. ويتمثل الخطوة الحاسمة في اختيار عدد قليل جدًا ولكن مهم جدًا من وحدات التنشيط ReLU لمعالجتها باستخدام متغيرات ثنائية (مكلفة). وقد كانت المحاولات السابقة غير مثالية من حيث هذا الجانب. ولتحديد هذه المتغيرات المهمة لوحدات ReLU، نقترح طريقة جديدة لتصنيف وحدات ReLU تُسمى "تصنيف وعي الحل" (SAS)، كما نُعدّل دوال التفرع BaB-SR وBaB-FSB لتصبح دوال تصنيف عالمية لوحدات ReLU (GS). ونقارن بينها نظريًا وتجريبيًا، حيث تُظهر SAS كفاءة أعلى في اختيار مجموعة من المتغيرات التي يجب فتحها باستخدام المتغيرات الثنائية. مقارنةً بالحلول السابقة، تقلل SAS من عدد المتغيرات الثنائية بنسبة تصل إلى 6 أضعاف، مع الحفاظ على نفس مستوى الدقة. عند تنفيذها في إطار Hybrid MILP، والذي يبدأ بتشغيل α,β-CROWN مع فترة انتهاء زمنية قصيرة لحل الحالات الأسهل، ثم ينتقل إلى استدعاءات MILP الجزئية، ينتج مُتحقق دقيق جدًا وفعال، حيث يقلل من عدد الحالات غير المحددة بنسبة تصل إلى 40%، ويُبقيها على مستوى منخفض (من 8% إلى 15%)، مع الحفاظ على زمن تشغيل معقول (متوسطه 46 ثانية إلى 417 ثانية لكل حالة)، حتى بالنسبة لشبكات التعلم العميق الكبيرة نسبيًا التي تحتوي على 2 مليون معامل.