प्रमाण यह है कि एसएटी एनपी-पूर्ण है एक रचनात्मक प्रमाण है, इसलिए इसे एक कार्यक्रम के रूप में लागू करना संभव होना चाहिए। क्या किसी ने ऐसा किया है?कंपाइलर्स जो एसएटी समस्याओं में सत्यापन एल्गोरिदम का अनुवाद करते हैं
मैं एक प्रोग्राम (एक कंपाइलर) की तलाश में हूं, जो एक प्रोग्राम इनपुट (जो सच या गलत देता है) लेता है और एक एसएटी फॉर्मूला आउटपुट करता है।
तो, उदाहरण के लिए, कंपाइलर निम्नलिखित प्रोग्राम (पाइथोनिक सिंटैक्स में दिखा सकता है, लेकिन कोई भी भाषा मेरे साथ ठीक है), इनपुट के रूप में, और एक एसएटी फॉर्मूला आउटपुट कर सकता है। एसएटी सॉल्वर को एसएटी फॉर्मूला को खिलााना पैरामीटर "सर्टिफिकेट" का समाधान देगा। इस मामले में, समाधान [गलत, सही, सही, सही, गलत] होगा, यह दर्शाता है कि {-3, -2, 5} एक समाधान है।
def verify(certificate):
problem = [-7, -3, -2, 5, 8]
sum = 0
for (x, b) in zip(problem, certificate):
if b:
sum += x
return sum == 0
जाहिर उत्पादन सैट सूत्र अन्य सहायक चर होता है, तो संकलक से संकेत मिलता है जो चर प्रमाण पत्र के अनुरूप होगा।
ऐसे कंपाइलर्स पहले से मौजूद हैं? क्या उनमें से कोई भी खुला स्रोत है?