सैद्धांतिक कंप्यूटर विज्ञान की शांत, अमूर्त दुनिया में, शोधकर्ता अक्सर तुल्यता (equivalence) की समस्या से जूझते हैं: यह निर्धारित करना कि क्या दो अलग-अलग दिखने वाली संरचनाएं वास्तव में एक ही अंतर्निहित वास्तविकता का प्रतिनिधित्व करती हैं। कल्पना कीजिए कि एक मशीन बनाने के निर्देशों का एक सेट है। आप निर्देशों को एक लंबे, घुमावदार पैराग्राफ में लिख सकते हैं, या आप उन्हें आरेखों (diagrams) के साथ एक बुलेटेड सूची में तोड़ सकते हैं। यदि दोनों निर्देशों के सेट से बिल्कुल एक ही मशीन तैयार होती है और वह ठीक एक ही तरह से कार्य करती है, तो वे तुल्य हैं, भले ही वे दिखने में बिल्कुल एक जैसे न हों। यह अवधारणा 'डायग्रामैटिक रीजनिंग' (आरेखीय तर्क) नामक एक क्षेत्र के केंद्र में है, जहाँ प्रक्रियाओं को समीकरणों के बजाय चित्रों के रूप में दर्शाया जाता है—जैसे कि रेखाओं से जुड़े बॉक्स। इन चित्रों का उपयोग जटिल प्रणालियों के मॉडल बनाने के लिए किया जाता है, जैसे बिजली का प्रवाह या क्वांटम कंप्यूटरों का व्यवहार। क्वांटम कंप्यूटिंग के क्षेत्र में, जहाँ मशीनें सूचनाओं को उन तरीकों से संचालित करती हैं जो रोजमर्रा की सहज बुद्धि को चुनौती देते हैं, दो अलग-अलग सर्किट आरेखों के एक ही कार्य करने की पुष्टि करना एक महत्वपूर्ण सुरक्षा जांच है। यदि कोई कंप्यूटर यह सिद्ध नहीं कर सकता कि दो डिज़ाइन समान हैं, तो उस पर भविष्य की तकनीक को चलाने वाले हार्डवेयर को अनुकूलित या सत्यापित करने के लिए भरोसा नहीं किया जा सकता।

फ्रांस और जर्मनी के शोधकर्ताओं की एक टीम ने अब एक नया सेट पेश किया है जो यह परीक्षण करने के लिए डिज़ाइन किया गया है कि आधुनिक स्वचालित तर्क उपकरण (automated reasoning tools) इस विशिष्ट प्रकार की तुल्यता को कितनी अच्छी तरह संभाल सकते हैं। उनका कार्य उन समस्याओं के एक परिवार पर केंद्रित है जिन्हें वे 'डायग्राममैटिक इक्विलवेंस' कहते हैं, जो एक सरल प्रश्न पूछता है: दिए गए दो अलग-अलग सर्किट आरेखों को क्या नियमों के एक निश्चित सेट का उपयोग करके एक-दूसरे में बदला जा सकता है? शोधकर्ताओं ने केवल प्रश्न ही नहीं पूछा; उन्होंने इस समस्या के हजारों अद्वितीय, कठिन उदाहरण उत्पन्न करने के लिए एक फैक्ट्री बनाई। उन्होंने कठिनाई के तीन अलग-अलग स्तर बनाए, जो तारों के आदान-प्रदान (swapping of wires) वाले एक सरलीकृत संस्करण से लेकर विभिन्न प्रकार के इलेक्ट्रॉनिक घटकों वाले एक जटिल संस्करण तक विस्तृत हैं। प्रत्येक स्तर के लिए, उन्होंने दृश्य आरेखों को एक ऐसी भाषा में अनुवादित किया जिसे कंप्यूटर पढ़ सकें, जिससे दुनिया के सबसे उन्नत ऑटोमेटेड थ्योरम प्रूवर्स और लॉजिक सॉल्वर्स के लिए एक कठोर परीक्षण स्थल तैयार हुआ।

शोधकर्ताओं ने खेल के नियमों को परिभाषित करने से शुरुआत की। उनके सिस्टम में, सर्किट बुनियादी निर्माण खंडों (generators) से बने होते हैं, जो तारों से जुड़े होते हैं। ये कनेक्शन दो तरीकों से हो सकते हैं: एक के बाद एक, जैसे एक श्रृंखला, या समानांतर पटरियों की तरह अगल-बगल। समस्या का मुख्य केंद्र यह तथ्य है कि एक ही सर्किट को कई अलग-अलग तरीकों से बनाया जा सकता है। जिस तरह एक वाक्य का अर्थ बदले बिना उसे पुनर्व्यवस्थित किया जा सकता है, उसी तरह एक सर्किट आरेख को विशिष्ट गणितीय नियमों के अनुसार घुमाया, खींचा या पुनर्गठित किया जा सकता है जिन्हें 'कोहेरेंस इक्वेशन्स' (coherence equations) कहा जाता है। एक कंप्यूटर के लिए चुनौती यह है कि वह दो ऐसे आरेखों को देखे जो पूरी तरह से अलग दिखते हैं और यह निर्धारित करे कि क्या वे वास्तव में उन्हीं नियमों के तहत एक ही वस्तु हैं। इसे परीक्षण योग्य बनाने के लिए, टीम ने समस्या के तीन रूपांतरण बनाए। पहला, और सबसे सामान्य, जिसमें किसी भी प्रकार का घटक शामिल हो सकता है। दूसरा, सभी घटकों को हटा देता है, केवल तार छोड़ देता है जिन्हें इधर-उधर बदला जा सकता है, जो प्रभावी रूप से समस्या को 'परम्यूटेशन' (क्रमपरिवर्तन) में बदल देता है। तीसरा, दूसरे का एक सरलीकृत संस्करण है, जो अधिक प्रबंधनीय, हालांकि अभी भी कठिन पहेली बनाने के लिए केवल सबसे बुनियादी निर्माण खंडों का उपयोग करता है।

डेटा उत्पन्न करने के लिए, टीम ने कंप्यूटर प्रोग्राम लिखे जो 'सर्किट आर्किटेक्ट्स' के रूप में कार्य करते हैं। ये प्रोग्राम एक खाली ग्रिड से शुरू होते हैं और यादृच्छिक रूप से घटकों और तारों को रखते हैं। फिर वे एक श्रृंखला रूपांतरण लागू करते हैं—जैसे तार को मोड़ना या दो आसन्न ब्लॉकों को बदलना—ताकि पहले सर्किट के गणितीय रूप से समान दिखने वाला दूसरा संस्करण बनाया जा सके, जो दिखता तो अलग है लेकिन समान है। प्रोग्राम यह सुनिश्चित करते हैं कि दोनों परिणामी आरेख निर्माण द्वारा तुल्य हैं, जिसका अर्थ है कि उत्तर हमेशा "हाँ" है, लेकिन इसे सिद्ध करने का मार्ग आरेख की जटिलता के भीतर छिपा हुआ है। शोधकर्ताओं ने हजारों ऐसे जोड़े उत्पन्न किए, जिनमें इनपुट तारों की संख्या और आरेखों के आकार को बदलकर कठिनाई का एक स्पेक्ट्रम बनाया। इसके बाद उन्होंने इन दृश्य पहेलियों को वैज्ञानिक समुदाय द्वारा उपयोग किए जाने वाले दो मानक प्रारूपों में एनकोड किया, जिससे कोई भी स्वचालित तर्क उपकरण समाधान का प्रयास कर सके।

जब शोधकर्ताओं ने इन बेंचमार्क को परीक्षण के लिए रखा, तो उन्होंने इन्हें आज उपलब्ध अग्रणी स्वचालित तर्क उपकरणों के विरुद्ध खड़ा किया। उन्होंने दो विशिष्ट प्रणालियों को चुना: एक जो अंकगणितीय और तार्किक बाधाओं (arithmetic and logical constraints) को संभालने में उत्कृष्ट है, और दूसरी जो सामान्य तार्किक निष्कर्ष (general logical deduction) के लिए एक शक्ति केंद्र है। परिणामों ने प्रदर्शन में एक स्पष्ट विभाजन प्रकट किया। अंकगणितीय बाधाओं को संभालने के लिए डिज़ाइन किया गया सिस्टम काफी अधिक सक्षम साबित हुआ, जिसने सरल और मध्यम कठिनाई वाले अधिकांश पजल्स को हल किया। इसने कई मामलों में बीस तारों और सैकड़ों घटकों वाले सर्किटों की तुल्यता को सत्यापित करने में सफलता प्राप्त की। हालाँकि, सामान्य निष्कर्ष (general deduction) प्रणाली संघर्ष करती रही। यह लगभग किसी भी जटिल समस्या को हल करने में विफल रही, और अपेक्षाकृत छोटे सर्किटों पर भी अटक गई। शोधकर्ताओं ने पाया कि समस्या की कठिनाई दो मुख्य कारकों द्वारा संचालित थी: शामिल तारों की संख्या और आरेख में कुल कनेक्शनों की संख्या। जैसे-जैसे ये संख्याएँ बढ़ीं, उपकरणों की समाधान खोजने की क्षमता तेजी से गिर गई।

यह अध्ययन स्वचालित तर्क के क्षेत्र में एक महत्वपूर्ण बाधा (bottleneck) को उजागर करता है। जबकि कंप्यूटर तेजी से शक्तिशाली होते जा रहे हैं, अंकगणितीय तर्क और जटिल संरचनात्मक नियमों के हेरफेर का विशिष्ट संयोजन एक कठिन चुनौती बना हुआ है। शोधकर्ताओं ने देखा कि वे उपकरण जो सबसे अच्छा प्रदर्शन करते थे, वे थे जो तारों को नियंत्रित करने वाले गणितीय बाधाओं को स्वाभाविक रूप से समझ सकते थे, बजाय इसके कि वे केवल तार्किक चरणों के माध्यम से उन्हें निकालने का प्रयास करें। यह सुझाव देता है कि डायग्राममैटिक इक्विलवेंस को कुशलतापूर्वक हल करने के लिए, भविष्य के उपकरणों को अपने मूल तर्क में अंकगणितीय तर्क को अधिक गहराई से एकीकृत करने की आवश्यकता हो सकती है। यह कार्य क्वांटम सर्किटों को सत्यापित करने की समस्या को हल करने का दावा नहीं करता है, लेकिन इसने एक महत्वपूर्ण 'स्ट्रेस टेस्ट' प्रदान किया है। इन बेंचमार्क को एक मानकीकृत, चुनौतीपूर्ण सेट प्रदान करके, टीम ने वैज्ञानिक समुदाय को प्रगति को मापने का एक स्पष्ट तरीका दिया है। ये बेंचमार्क एक दर्पण के रूप में कार्य करते हैं, जो हमारे स्वचालित उपकरणों की वर्तमान सीमाओं को दर्शाते हैं और जटिल, आधारित-आरेख प्रणालियों के सत्यापन को एक विश्वसनीय वास्तविकता बनाने के लिए आवश्यक विशिष्ट सुधारों की ओर संकेत करते हैं।