सेट थ्योरी के निर्धारित खंडों के लिए जटिलता मूल्यांकन। IV: नेस्टेड सेट्स पर बाधाओं से बूलियन सूत्रों के लिए एक द्विघाती कमी

स्वचालित सेट-थ्योरिटिक इनफेरेंसिंग में एक योगदान के रूप में, x=y∖z, x≠y∖z, और z=x के रूपों के लिटेरल्स के संयोजनों का एक अनुवाद प्रस्तावित किया गया है, जहां x, y, z उन वेरिएबल्स के लिए खड़े हैं जो वोन न्यूमान सेट्स के ब्रह्मांड में बिखरे हुए हैं, को एक अपेक्षाकृत सरल संयोजक सामान्य रूप के क्वांटिफायर-मुक्त बूलियन सूत्रों में। लक्षित भाषा में सूत्र ऐसे वेरिएबल्स शामिल होते हैं जो सेट्स के बूलियन रिंग पर फैले होते हैं, साथ ही एक अंतर परिचालक और समता, असंगति, और समावेश को दर्शाने वाले रिलेटर्स होते हैं। इसके अलावा, प्रत्येक अनुवाद का परिणाम x=y∖z और x≠y∖z के रूपों के लिटेरल्स का संयोजन और उनके पूर्ववर्ती अकेले लिटेरल्स होते हैं और उनके परिणाम या तो वेरिएबल्स के बीच समावेश (सख्त या नॉन-सख्त) होते हैं, या वेरिएबल्स के बीच समानताएँ होती हैं। सरल और प्राकृतिक अर्थशास्त्र को दर्शाते हुए, जो संतोषजनकता संरक्षण सुनिश्चित करता है, प्रस्तावित अनुवाद का द्विघाती एल्गोरिदमिक समय जटिलता है और दो भाषाओं के बीच एक पुल बनाता है, जिनमें से दोनों को NP-संपूर्ण संतोषजनकता समस्या के लिए जाना जाता है।