एसएटी समस्या का सभी समाधान खोजने के लिए वर्णित एसएटी सॉल्वर का उपयोग करने का निश्चित रूप से एक तरीका है, हालांकि यह सबसे प्रभावी तरीका नहीं हो सकता है।
बस अपनी मूल समस्या का हल ढूंढने के लिए सॉल्वर का उपयोग करें, एक ऐसा खंड जोड़ें जो आपके द्वारा अभी मिले समाधान को रद्द करने के अलावा कुछ भी नहीं करता है, नई समस्या का हल ढूंढने के लिए सॉल्वर का उपयोग करें, और आगे। तब तक जारी रहें जब तक आपको कोई समस्या न हो जो असंतुष्ट है।
उदाहरण के लिए, आप (X or Y) and (X or Z) को संतुष्ट रखना चाहते हैं।
X सच है, Y और Z मनमाना साथ चार: वहाँ पाँच समाधान कर रहे हैं।
X झूठी, Y और Z सत्य के साथ एक।
तो आप अपने solver चलाते हैं, और मान लें कि यह आप समाधान (X, Y, Z) = (T, F, F) देता हैं। आप बाधा
not (X and (not Y) and (not Z))
साथ --- इस समाधान --- और केवल इस समाधान से इनकार कर सकते हैं इस बाधा खंड
(not X) or Y or Z
तो अब आप पर अपने solver चला सकते हैं के रूप में लिखा जा सकता है नई समस्या
(X or Y) and (X or Z) and ((not X) or Y or Z)
और बहुत आगे।
जैसा मैंने कहा, यह वही करने का एक तरीका है जो आप चाहते हैं, लेकिन यह शायद सबसे प्रभावी तरीका नहीं है। जब आपका एसएटी सॉल्वर समाधान की तलाश में है, तो यह समस्या के बारे में बहुत कुछ सीखता है, लेकिन यह आपको वह सारी जानकारी वापस नहीं देता है --- यह आपको वह समाधान देता है जो इसे मिला। जब आप फिर से सॉल्वर चलाते हैं, तो उसे दूर की गई सारी जानकारी को फिर से सीखना होता है।
व्यक्ति जो कृपया downvoted व्याख्या कर सकते हैं क्यों? इस ब्लॉग एंट्री को पढ़ने के बाद (http://blog.stackoverflow.com/2011/07/its-ok-to-ask-and-answer-your-own-questions/), मैंने सोचा कि मैंने यहां क्या किया था "न केवल ठीक है, "लेकिन" स्पष्ट रूप से प्रोत्साहित किया। " – Vectornaut
यह बिल्कुल ठीक है। अच्छा जवाब, बीटीडब्ल्यू। –