बाधा तर्क प्रोग्रामिंग: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 2: Line 2:
{{Programming paradigms}}
{{Programming paradigms}}


'''बाधा [[तर्क प्रोग्रामिंग]]''' [[बाधा प्रोग्रामिंग]] का एक रूप है जिसमें बाधा संतुष्टि की अवधारणाओं को सम्मिलित करने के लिए तर्क प्रोग्रामिंग को विस्तृत जाता है। एक बाधा तर्क प्रोग्राम एक तर्क प्रोग्राम है जिसके डेटा में भौतिकी बाधाएं होती हैं। बाधा सहित तर्क का एक उदाहरण {{code|2=prolog|A(X,Y) :- X+Y>0, B(X), C(Y)}} है इस भाग में {{code|2=prolog|X+Y>0}} एक बाधा है जो <code>A(X,Y)</code>, <code>B(X)</code> और <code>C(Y)</code> के नियमित तर्क प्रोग्रामिंग के रूप में [[शाब्दिक (गणितीय तर्क)]] हैं। यह तर्क एक नियम का अनुसरण करता है। जिसके अंतर्गत कथन <code>A(X,Y)</code> <code>X+Y</code> शून्य से अधिक होता है। जिससे <code>B(X)</code> और <code>C(Y)</code> दोनों सत्य होते हैं।
'''[[तर्क प्रोग्रामिंग|बाधा तर्क प्रोग्रामिंग]]''' [[बाधा प्रोग्रामिंग]] का एक रूप है जिसमें बाधा संतुष्टि की अवधारणाओं को सम्मिलित करने के लिए तर्क प्रोग्रामिंग को विस्तृत जाता है। एक बाधा तर्क प्रोग्राम एक तर्क प्रोग्राम है जिसके डेटा में भौतिकी बाधाएं होती हैं। बाधा सहित तर्क का एक उदाहरण {{code|2=prolog|A(X,Y) :- X+Y>0, B(X), C(Y)}} है इस भाग में {{code|2=prolog|X+Y>0}} एक बाधा है जो <code>A(X,Y)</code>, <code>B(X)</code> और <code>C(Y)</code> के नियमित तर्क प्रोग्रामिंग के रूप में [[शाब्दिक (गणितीय तर्क)]] हैं। यह तर्क एक नियम का अनुसरण करता है। जिसके अंतर्गत कथन <code>A(X,Y)</code> <code>X+Y</code> शून्य से अधिक होता है। जिससे <code>B(X)</code> और <code>C(Y)</code> दोनों सत्य होते हैं।


जैसा कि नियमित तार्किक प्रोग्रामिंग भाषा में होता है। प्रोग्रामों से किसी लक्ष्य की उपयोगिता के विषय में जानकारी प्राप्त की जाती है। जिसमें शाब्दिक तर्क के अतिरिक्त बाधाएँ भी हो सकती हैं। यह लक्ष्य के लिए एक प्रमाण उन खंडों से बना होता है जिनकी भौतिक संतोषजनक बाधाएँ और शाब्दिक होती हैं जो परिवर्तन में अन्य खंडों का उपयोग करके सिद्ध की जा सकती हैं। इनका निष्पादन एक अनुवादक द्वारा किया जाता है, जो लक्ष्य से प्रारम्भ होता है और लक्ष्य को सिद्ध करने के प्रयास कर रहे खंडों का पुनः अवलोकन करता है। इस अवलोकन के समय आने वाली बाधाओं को एक भंडारण में रखा जाता है जिसे बाधा भंडार कहा जाता है। यदि यह भंडारण असंतोषजनक पाया जाता है तो अनुवादक पीछे हट जाता है और लक्ष्य को सिद्ध करने के लिए अन्य खंडों का उपयोग करने का प्रयास करता है। सामान्यतः एक अपूर्ण एल्गोरिदम का उपयोग करके बाधा भंडार की संतुष्टि की जांच की जा सकती है, जो सदैव असंगतता का पता नहीं लगाती है।
जैसा कि नियमित तार्किक प्रोग्रामिंग भाषा में होता है। प्रोग्रामों से किसी लक्ष्य की उपयोगिता के विषय में जानकारी प्राप्त की जाती है। जिसमें शाब्दिक तर्क के अतिरिक्त बाधाएँ भी हो सकती हैं। यह लक्ष्य के लिए एक प्रमाण उन खंडों से बना होता है जिनकी भौतिक संतोषजनक बाधाएँ और शाब्दिक होती हैं जो परिवर्तन में अन्य खंडों का उपयोग करके सिद्ध की जा सकती हैं। इनका निष्पादन एक अनुवादक द्वारा किया जाता है, जो लक्ष्य से प्रारम्भ होता है और लक्ष्य को सिद्ध करने के प्रयास कर रहे खंडों का पुनः अवलोकन करता है। इस अवलोकन के समय आने वाली बाधाओं को एक भंडारण में रखा जाता है जिसे बाधा भंडार कहा जाता है। यदि यह भंडारण असंतोषजनक पाया जाता है तो अनुवादक पीछे हट जाता है और लक्ष्य को सिद्ध करने के लिए अन्य खंडों का उपयोग करने का प्रयास करता है। सामान्यतः एक अपूर्ण एल्गोरिदम का उपयोग करके बाधा भंडार की संतुष्टि की जांच की जा सकती है, जो सदैव असंगतता का पता नहीं लगाती है।
Line 30: Line 30:
अनुवादक ने लक्ष्य को सिद्ध कर दिया था जब वर्तमान लक्ष्य रिक्त था और बाधा भंडार को असंतोषजनक नहीं पाया गया है। निष्पादन का परिणाम (सरलीकृत) बाधाओं का वर्तमान समूह है। इस समूह में <math>X=2</math> जैसे बाधा सम्मिलित हो सकती हैं जो वेरिएबल (चर) को एक विशिष्ट मान के लिए बाध्य करती हैं लेकिन इसमें <math>X>2</math> जैसे बाधा भी सम्मिलित हो सकती हैं जो केवल वेरिएबल को एक विशिष्ट मान दिए बिना बाध्य करती हैं।
अनुवादक ने लक्ष्य को सिद्ध कर दिया था जब वर्तमान लक्ष्य रिक्त था और बाधा भंडार को असंतोषजनक नहीं पाया गया है। निष्पादन का परिणाम (सरलीकृत) बाधाओं का वर्तमान समूह है। इस समूह में <math>X=2</math> जैसे बाधा सम्मिलित हो सकती हैं जो वेरिएबल (चर) को एक विशिष्ट मान के लिए बाध्य करती हैं लेकिन इसमें <math>X>2</math> जैसे बाधा भी सम्मिलित हो सकती हैं जो केवल वेरिएबल को एक विशिष्ट मान दिए बिना बाध्य करती हैं।


'''औपचारिक रूप से, बाधा तर्क प्रोग्रामिंग के शब्दों को व्यु'''त्पत्तियों के संदर्भ में परिभाषित किया गया है। एक संक्रमण जोड़े लक्ष्य/भंडार की एक युग्म है, नोट किया गया <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math>. ऐसा जोड़ा राज्य से जाने की संभावना बताता है <math>\langle G,S \rangle</math> कहना <math>\langle G',S' \rangle</math>. ऐसा संक्रमण तीन संभावित मामलों में संभव है:
औपचारिक रूप से, बाधा तर्क प्रोग्रामिंग के शब्दों को व्युत्पत्तियों के संदर्भ में परिभाषित किया गया है। प्रसंस्करण युग्म लक्ष्य या भंडार युग्म द्वारा निर्धारित किए गए युग्म <math>\langle G,S \rangle \rightarrow \langle G',S' \rangle</math> एक युग्म है। इस प्रकार की युग्मों की स्थिति <math>\langle G,S \rangle</math> से <math>\langle G',S' \rangle</math> तक जाने की संभावना है।


* {{mvar|G}} का एक तत्व एक बाधा है {{mvar|C}}, <math>G'=G \backslash \{C\}</math> और <math>S'=S \cup \{C\}</math> दूसरे शब्दों में, एक बाधा को लक्ष्य से बाधा भंडार में ले जाया जा सकता है।
* {{mvar|G}} का एक तत्व {{mvar|C}} की बाधा <math>G'=G \backslash \{C\}</math> और <math>S'=S \cup \{C\}</math> है। दूसरे शब्दों में, एक बाधा को लक्ष्य से बाधा भंडार में ले जाया जा सकता है।
* का एक तत्व {{mvar|G}} शाब्दिक है <math>L(t_1,\ldots,t_n)</math>, वहाँ एक खंड सम्मिलित है, जो नए चर का उपयोग करके फिर से लिखा गया है <math>L(t_1',\ldots,t_n') :- B</math>, <math>G'</math> है {{mvar|G}} साथ <math>L(t_1,\ldots,t_n)</math> द्वारा प्रतिस्थापित <math>t_1=t_1',\ldots,t_n=t_n',B</math>, और <math>S'=S</math>; दूसरे शब्दों में, एक शाब्दिक को एक खंड के नए संस्करण के एल्गोरिदम द्वारा प्रतिस्थापित किया जा सकता है, जिसमें सिर में समान विधेय होता है, नए संस्करण के एल्गोरिदम और लक्ष्य के शब्दों की उपरोक्त समानताएं जोड़ते हुए
* {{mvar|G}} का तत्व एक शाब्दिक तर्क <math>L(t_1,\ldots,t_n)</math> है जिसमे एक भाग सम्मिलित है जो नए वेरिएबल का उपयोग करके फिर से <math>L(t_1',\ldots,t_n') :- B</math>, <math>G'</math> लिखा गया है। {{mvar|G}} के साथ <math>L(t_1,\ldots,t_n)</math> द्वारा प्रतिस्थापित <math>t_1=t_1',\ldots,t_n=t_n',B</math>, और <math>S'=S</math> है। दूसरे शब्दों में, एक शाब्दिक तर्क को एक खंड के नए संस्करण के एल्गोरिदम द्वारा प्रतिस्थापित किया जा सकता है। जिसमें नए संस्करण के एल्गोरिदम और लक्ष्य के शब्दों की उपरोक्त समानताएं जोड़ते हुए एक भाग में समान विधेय होता है।
* {{mvar|S}} और <math>S'</math> विशिष्ट बाधा शब्दार्थ के अनुसार समान हैं।  
* {{mvar|S}} और <math>S'</math> विशिष्ट बाधा शब्दार्थ के अनुसार समान हैं।  


संक्रमण का एक क्रम एक व्युत्पत्ति है। एक लक्ष्य {{mvar|G}} सिद्ध किया जा सकता है अगर वहाँ से कोई व्युत्पत्ति सम्मिलित है <math>\langle G, \emptyset \rangle</math> को <math>\langle \emptyset, S \rangle</math> कुछ संतोषजनक बाधा भंडार के लिए {{mvar|S}}. यह शब्दार्थ एक अनुवादक के संभावित विकास को औपचारिक रूप देता है जो अपेक्षाकृत रूप से प्रक्रिया के लक्ष्य का शाब्दिक चयन करता है और शाब्दिक को बदलने के लिए खंड। दूसरे शब्दों में, इस शब्दार्थ के तहत एक लक्ष्य सिद्ध होता है यदि शाब्दिक और खंडों के विकल्पों का एक क्रम सम्मिलित होता है, संभवतः कई लोगों के बीच, जो एक खाली लक्ष्य और संतोषजनक भंडार की ओर ले जाता है।
प्रसंस्करण का अनुक्रम एक व्युत्पत्ति है। एक लक्ष्य {{mvar|G}} सिद्ध किया जा सकता है यदि वहाँ से कोई व्युत्पत्ति सम्मिलित है। <math>\langle G, \emptyset \rangle</math> को <math>\langle \emptyset, S \rangle</math> के संतोषजनक बाधा भंडार के लिए {{mvar|S}} शब्दार्थ के अनुवादक के संभावित विकास को औपचारिक रूप देता है जो अपेक्षाकृत रूप से प्रक्रिया के लक्ष्य का शाब्दिक चयन करता है और शाब्दिक तर्क को परिवर्तित करने के लिए खंड को दूसरे शब्दों में इस शब्दार्थ के अंतर्गत एक लक्ष्य सिद्ध होता है यदि शाब्दिक तर्क और खंडों के विकल्पों का एक क्रम सम्मिलित होता है। संभवतः कई लोगों के बीच जो एक रिक्त लक्ष्य और संतोषजनक भंडार की ओर ले जाता है।


वास्तविक दुभाषिए लक्ष्य तत्वों को एलआईएफओ क्रम में संसाधित करते हैं: तत्वों को सामने से जोड़ा जाता है और सामने से संसाधित किया जाता है। वे उस क्रम के अनुसार दूसरे नियम का खंड भी चुनते हैं जिसमें वे लिखे गए हैं, और संशोधित होने पर बाधा संग्रह को फिर से लिखते हैं।
वास्तविक अनुवादक लक्ष्य तत्वों को एलआईएफओ क्रम में संसाधित करते हैं तत्वों को सामने से जोड़ा जाता है और सामने से संसाधित किया जाता है। वे उस क्रम के अनुसार दूसरे नियम का खंड भी चुनते हैं जिसमें वे लिखे गए हैं और संशोधित होने पर बाधा संग्रह को फिर से लिखते हैं।


तीसरे संभावित प्रकार का संक्रमण समतुल्य भंडार के साथ बाधा भंडार का प्रतिस्थापन है। यह प्रतिस्थापन उन विशिष्ट विधियों द्वारा किया जाता है, जैसे बाधा प्रचार। बाधा तर्क प्रोग्रामिंग का शब्दार्थ न केवल उपयोग की जाने वाली बाधाओं के लिए पैरामीट्रिक है बल्कि बाधा भंडार को फिर से लिखने की विधि के लिए भी है। अभ्यास में उपयोग की जाने वाली विशिष्ट विधियां बाधा भंडार को हल करने में आसान होती हैं। यदि बाधा भंडार असंतोषजनक है, तो यह सरलीकरण कभी-कभी इस असंतोष का पता लगा सकता है, लेकिन हमेशा नहीं।
तीसरा संभावित प्रकार का प्रसंस्करण समतुल्य भंडार के साथ बाधा भंडार का प्रतिस्थापन है। यह प्रतिस्थापन उन विशिष्ट विधियों जैसे बाधा प्रचार द्वारा किया जाता है। बाधा तर्क प्रोग्रामिंग का शब्दार्थ न केवल उपयोग की जाने वाली बाधाओं के लिए पैरामीट्रिक है बल्कि बाधा भंडार को फिर से लिखने की विधि के लिए भी है। अभ्यास में उपयोग की जाने वाली विशिष्ट विधियां बाधा भंडार को हल करने में आसान होती हैं। यदि बाधा भंडार असंतोषजनक है तो यह सरलीकरण कभी-कभी इस असंतोष का पता लगा सकता है लेकिन हमेशा नहीं पता लगा सकता है।


लक्ष्य सिद्ध होने पर बाधा तर्क प्रोग्राम के खिलाफ लक्ष्य का मूल्यांकन करने का नतीजा परिभाषित किया गया है। इस मामले में, प्रारंभिक युग्म से एक युग्म के लिए व्युत्पत्ति सम्मिलित है जहां लक्ष्य खाली है। इस दूसरी युग्म के बाधा भंडार को मूल्यांकन का परिणाम माना जाता है। ऐसा इसलिए है क्योंकि बाधा भंडार में लक्ष्य को सिद्ध करने के लिए संतोषजनक माने जाने वाले सभी प्रतिबंध सम्मिलित हैं। दूसरे शब्दों में, लक्ष्य उन सभी परिवर्तनीय मूल्यांकनों के लिए सिद्ध होता है जो इन बाधाओं को पूरा करते हैं।
लक्ष्य सिद्ध होने पर बाधा तर्क प्रोग्राम के विरुद्ध लक्ष्य का मूल्यांकन करने का परिणाम परिभाषित किया गया है। इस स्थिति में प्रारंभिक युग्म से एक युग्म के लिए व्युत्पत्ति सम्मिलित है जहां लक्ष्य रिक्त है। इस दूसरी युग्म के बाधा भंडार को मूल्यांकन का परिणाम माना जाता है। ऐसा इसलिए है क्योंकि बाधा भंडार में लक्ष्य को सिद्ध करने के लिए संतोषजनक माने जाने वाले सभी प्रतिबंध सम्मिलित हैं। दूसरे शब्दों में लक्ष्य उन सभी परिवर्तनीय मूल्यांकनों के लिए सिद्ध होता है जो इन बाधाओं को पूरा करते हैं।


दो शाब्दिक शब्दों की युग्मदार समानता को प्रायः <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> द्वारा संक्षेप में निरूपित किया जाता है यह एक आशुलिपि है बाधाओं के लिए बाधा तर्क प्रोग्रामिंग के लिए शब्दार्थ का एक सामान्य संस्करण <math>t_1=t_1',\ldots,t_n=t_n'</math> सीधे बाधा भंडार में जोड़ता है बल्कि लक्ष्य की तुलना में।
दो शाब्दिक शब्दों की युग्म समानता को प्रायः <math>L(t_1,\ldots,t_n)=L(t_1',\ldots,t_n')</math> द्वारा संक्षेप में निरूपित किया जाता है यह एक आशुलिपि है। लेकिन लक्ष्य की तुलना में बाधाओं के लिए बाधा तर्क प्रोग्रामिंग शब्दार्थ का एक सामान्य संस्करण <math>t_1=t_1',\ldots,t_n=t_n'</math> सीधे बाधा भंडार में जोड़ता है।


== नियम और शर्तें ==
== नियम और शर्तें ==


शब्दों की विभिन्न परिभाषाओं का उपयोग किया जाता है, जिससे पेड़ों, वास्तविक या परिमित डोमेन पर विभिन्न प्रकार की बाधा तर्क प्रोग्रामिंग उत्पन्न होती है। एक प्रकार की बाधा जो हमेशा सम्मिलित रहती है वह शर्तों की समानता है। इस प्रकार की बाधाएं आवश्यक हैं क्योंकि अनुवादक <code>t1=t2</code> को लक्ष्य में जोड़ता है जब भी एक शाब्दिक <code>P(...t1...)</code> को क्लॉज फ्रेश वेरिएंट के एल्गोरिदम के साथ बदल दिया जाता है जिसका सिर <code>P(...t2...)</code>.
शब्दों की विभिन्न परिभाषाओं का उपयोग किया जाता है। जिससे वास्तविक या परिमित डोमेन पर विभिन्न प्रकार की बाधा तर्क प्रोग्रामिंग उत्पन्न होती है। एक प्रकार की बाधा जो सदैव सम्मिलित रहती है वह शर्तों की समानता है। इस प्रकार की बाधाएं आवश्यक हैं क्योंकि अनुवादक <code>t1=t2</code> को लक्ष्य में जोड़ता है जब भी एक शाब्दिक <code>P(...t1...)</code> को नए संस्करण के एल्गोरिदम के साथ परिवर्तित कर दिया जाता है जिसका क्रम <code>P(...t2...)</code> है।


=== पेड़ की शर्तें ===
=== रेखीय नियम ===


पेड़ की शर्तों के साथ बाधा तर्क प्रोग्रामिंग बाधा भंडार में बाधाओं के रूप में प्रतिस्थापन को संग्रहित करके नियमित तर्क प्रोग्रामिंग का अनुकरण करती है। शर्तें चर, स्थिरांक और फ़ंक्शन प्रतीक हैं जो अन्य शर्तों पर प्रयुक्त होते हैं। शर्तों के बीच समानता और असमानताओं पर विचार की जाने वाली एकमात्र बाधाएं हैं। समानता विशेष रूप से महत्वपूर्ण है, क्योंकि<code>t1=t2</code> जैसे प्रतिबंध प्रायः अनुवादक द्वारा उत्पन्न किए जाते हैं। शर्तों पर समानता की बाधाओं को सरल बनाया जा सकता है, जिसे एकीकरण के माध्यम से हल किया जाता है:
रेखीय नियमों के साथ बाधा तर्क प्रोग्रामिंग बाधा भंडार में बाधाओं के रूप में प्रतिस्थापन को संग्रहित करके नियमित तर्क प्रोग्रामिंग का अनुकरण करती है। शर्तें वेरिएबल स्थिरांक और फ़ंक्शन प्रतीक हैं जो अन्य शर्तों पर प्रयुक्त होते हैं। शर्तों के बीच समानता और असमानताओं पर विचार की जाने वाली एकमात्र बाधाएं हैं। समानता विशेष रूप से महत्वपूर्ण है, क्योंकि<code>t1=t2</code> जैसे प्रतिबंध प्रायः अनुवादक द्वारा उत्पन्न किए जाते हैं। शर्तों पर समानता की बाधाओं को सरल बनाया जा सकता है। जिसे एकीकरण के माध्यम से हल किया जाता है।


एक बाधा <code>t1=t2</code> को सरल बनाया जा सकता है यदि दोनों पद अन्य पदों पर प्रयुक्त कार्य प्रतीक हैं। यदि दो फ़ंक्शन प्रतीक समान हैं और सबटर्म की संख्या भी समान है, तो इस बाधा को सबटर्म की युग्मदार समानता से परिवर्तित जा सकता है। यदि शर्तें अलग-अलग फ़ंक्शन प्रतीकों या एक ही फ़ैक्टर से बनी हैं, लेकिन अलग-अलग शर्तों पर, बाधा असंतुष्ट है।
एक बाधा <code>t1=t2</code> को सरल बनाया जा सकता है यदि दोनों पद अन्य पदों पर प्रयुक्त फ़ंक्शन प्रतीक हैं। यदि दो फ़ंक्शन प्रतीक समान हैं और उपनियम की संख्या भी समान है तो इस बाधा को उपनियम की युग्म समानता से परिवर्तित जा सकता है। यदि शर्तें अलग-अलग फ़ंक्शन प्रतीकों या एक ही गुणक से बनी हैं लेकिन अलग-अलग शर्तों पर बाधा को असंतुष्ट करती है।


यदि दो पदों में से एक एक चर है, तो चर का एकमात्र अनुमत मान दूसरा पद हो सकता है। जिसके परिणाम स्वरूप, अन्य शब्द चर को वर्तमान लक्ष्य और बाधा भंडार में बदल सकते हैं, इस प्रकार व्यावहारिक रूप से चर को विचार से हटा सकते हैं। स्वयं के साथ एक चर की समानता के विशेष मामले में, बाधा को हमेशा संतुष्ट के रूप में हटाया जा सकता है।
यदि दो पदों में से एक वेरिएबल है तो वेरिएबल का एकमात्र अनुमत मान दूसरा पद हो सकता है। जिसके परिणाम स्वरूप अन्य शब्द वेरिएबल को वर्तमान लक्ष्य और बाधा भंडार में परिवर्तित कर सकते हैं। इस प्रकार सामान्य रूप से वेरिएबल को विचार से हटा सकते हैं। स्वयं के साथ एक वेरिएबल की समानता की विशेष स्थिति में बाधा को सदैव संतुष्ट के रूप में हटाया जा सकता है। बाधा संतुष्टि के इस रूप में वेरिएबल मान पद हैं।


बाधा संतुष्टि के इस रूप में, चर मान पद हैं।
=== वास्तविक संख्याए ===


=== असली ===
वास्तविक संख्या के साथ बाधा तर्क प्रोग्रामिंग शब्दों के रूप में वास्तविक भावों का उपयोग करती है। जब कोई फ़ंक्शन प्रतीकों का उपयोग नहीं किया जाता है तो शब्द संभवतः वेरिएबल सहित वास्तविक रूप से अभिव्यक्ति होते हैं। इस स्थिति में प्रत्येक वेरिएबल केवल एक वास्तविक संख्या को मान के रूप में ले सकता है। शुद्ध होने के लिए पद वेरिएबल और वास्तविक स्थिरांक पर व्यंजक हैं। शर्तों के बीच समानता एक प्रकार की बाधा है जो सदैव सम्मिलित रहती है क्योंकि अनुवादक निष्पादन के समय शर्तों की समानता उत्पन्न करता है। एक उदाहरण के रूप में यदि वर्तमान लक्ष्य का पहला अक्षर <code>A(X+1)</code> है और अनुवादक ने एक खंड चुना है जो <code>A(Y-1):-Y=1</code> फिर से लिखने के बाद वेरिएबल हैं वर्तमान में बाधाओं को जोड़ा गया है जिसका लक्ष्य <code>X+1=Y-1</code> और <math>Y=1</math> हैं। फ़ंक्शन प्रतीकों के लिए उपयोग किए जाने वाले सरलीकरण के नियम स्पष्ट रूप से उपयोग नहीं किए जाते हैं। <code>X+1=Y-1</code> केवल इसलिए असंतोषजनक नहीं है क्योंकि पहली अभिव्यक्ति <code>+</code> का उपयोग करके बनाई गई है और दूसरी <code>-</code> का उपयोग करके बनाई गई है।


वास्तविक संख्या के साथ बाधा तर्क प्रोग्रामिंग शब्दों के रूप में वास्तविक भावों का उपयोग करती है। जब कोई फ़ंक्शन प्रतीकों का उपयोग नहीं किया जाता है, तो शब्द वास्तविक रूप से अभिव्यक्ति होते हैं, संभवतः चर सहित। इस मामले में, प्रत्येक चर केवल एक वास्तविक संख्या को मान के रूप में ले सकता है।
वास्तविक संख्याए और फ़ंक्शन प्रतीकों को जोड़ा जा सकता है। जो उन शर्तों के लिए अग्रणी होते हैं। जो वास्तविक और फ़ंक्शन प्रतीकों पर अन्य शर्तों पर प्रयुक्त होते हैं। औपचारिक रूप से, वेरिएबल और वास्तविक स्थिरांक भाव हैं अन्य अभिव्यक्तियों पर किसी भी अंकगणितीय संचालक के रूप में वेरिएबल स्थिरांक (शून्य एरिटी फ़ंक्शन प्रतीक) और भाव शब्द हैं। जैसा कि कोई भी फ़ंक्शन प्रतीक शर्तों पर प्रयुक्त होता है। दूसरे शब्दों में पद व्यंजकों पर निर्मित होते हैं जबकि व्यंजक संख्याओं और वेरिएबलों पर निर्मित होते हैं। इस स्थिति में वेरिएबल वास्तविक संख्या और शब्दों से अधिक होते हैं। दूसरे शब्दों में वेरिएबल एक वास्तविक संख्या को मान के रूप में ले सकता है जबकि दूसरा एक पद लेता है।


सटीक होने के लिए, पद चर और वास्तविक स्थिरांक पर व्यंजक हैं। शर्तों के बीच समानता एक प्रकार की बाधा है जो हमेशा सम्मिलित रहती है, क्योंकि अनुवादक निष्पादन के समय शर्तों की समानता उत्पन्न करता है। एक उदाहरण के रूप में, यदि वर्तमान लक्ष्य का पहला अक्षर <code>A(X+1)</code> है और अनुवादक ने एक खंड चुना है जो <code>A(Y-1):-Y=1</code> फिर से लिखने के बाद वेरिएबल्स हैं, वर्तमान में बाधाओं को जोड़ा गया है लक्ष्य <code>X+1=Y-1</code> और <math>Y=1</math> हैं। फ़ंक्शन प्रतीकों के लिए उपयोग किए जाने वाले सरलीकरण के नियम स्पष्ट रूप से उपयोग नहीं किए जाते हैं <code>X+1=Y-1</code> केवल इसलिए असंतोषजनक नहीं है क्योंकि पहली अभिव्यक्ति <code>+</code> का उपयोग करके बनाई गई है और दूसरी <code>-</code> का उपयोग करके बनाई गई है।
यदि दो शब्दों में से कोई भी वास्तविक अभिव्यक्ति नहीं है, तो दो शब्दों की समानता को वास्तविक शर्तों के नियमों का उपयोग करके सरल बनाया जा सकता है। उदाहरण के लिए यदि दो शब्दों में एक ही फ़ंक्शन प्रतीक और उपनियम की संख्या है तो उनकी समानता की बाधा को उपनियम की समानता से परिवर्तित किया जा सकता है।
 
रियल और फ़ंक्शन प्रतीकों को जोड़ा जा सकता है, जो उन शर्तों के लिए अग्रणी होते हैं जो वास्तविक और फ़ंक्शन प्रतीकों पर अन्य शर्तों पर प्रयुक्त होते हैं। औपचारिक रूप से, चर और वास्तविक स्थिरांक भाव हैं, अन्य अभिव्यक्तियों पर किसी भी अंकगणितीय ऑपरेटर के रूप में। चर, स्थिरांक (शून्य-एरिटी-फ़ंक्शन प्रतीक), और भाव शब्द हैं, जैसा कि कोई भी फ़ंक्शन प्रतीक शर्तों पर प्रयुक्त होता है। दूसरे शब्दों में, पद व्यंजकों पर निर्मित होते हैं, जबकि व्यंजक संख्याओं और चरों पर निर्मित होते हैं। इस मामले में, चर वास्तविक संख्या और शब्दों से अधिक होते हैं। दूसरे शब्दों में, एक चर एक वास्तविक संख्या को मान के रूप में ले सकता है, जबकि दूसरा एक पद लेता है।
 
यदि दो शब्दों में से कोई भी वास्तविक अभिव्यक्ति नहीं है, तो दो शब्दों की समानता को वृक्ष शर्तों के नियमों का उपयोग करके सरल बनाया जा सकता है। उदाहरण के लिए, यदि दो शब्दों में एक ही फ़ंक्शन प्रतीक और सबटर्म की संख्या है, तो उनकी समानता की बाधा को सबटर्म की समानता से परिवर्तित किया जा सकता है।


=== परिमित डोमेन ===
=== परिमित डोमेन ===
{{see also|बाधा संतुष्टि समस्या}}
{{see also|बाधा संतुष्टि समस्या}}


बाधा तर्क प्रोग्रामिंग में प्रयुक्त बाधाओं की तीसरी श्रेणी परिमित डोमेन की है। चर के मान इस मामले में एक परिमित डोमेन से लिए गए हैं, जो प्रायः पूर्णांक संख्याओं के होते हैं। प्रत्येक चर के लिए, एक अलग डोमेन निर्दिष्ट किया जा सकता है: <code>X::[1..5]</code> उदाहरण के लिए इसका मतलब है कि <code>X</code> के बीच है <code>1</code> और <code>5</code> के बीच है। एक चर का डोमेन उन सभी मानों की गणना करके भी दिया जा सकता है जो एक चर कर सकते हैं लेना; इसलिए, उपरोक्त डोमेन घोषणा को <code>X::[1,2,3,4,5]</code> भी लिखा जा सकता है। डोमेन निर्दिष्ट करने का यह दूसरा तरीका उन डोमेन के लिए स्वीकृति देता है जो पूर्णांकों से नहीं बने हैं, जैसे कि <code>X::[george,mary,john]</code>यदि एक चर का डोमेन निर्दिष्ट नहीं है, तो इसे भाषा में प्रतिनिधित्व करने योग्य पूर्णांकों का समूह माना जाता है।<code>[X,Y,Z]::[1..5]</code> जैसे डिक्लेरेशन का उपयोग करके वेरिएबल्स के एक समूह को एक ही डोमेन दिया जा सकता है।
बाधा तर्क प्रोग्रामिंग में प्रयुक्त बाधाओं की तीसरी श्रेणी परिमित डोमेन की है। वेरिएबल के मान इस स्थिति में एक परिमित डोमेन से लिए गए हैं, जो प्रायः पूर्णांक संख्याओं के होते हैं। प्रत्येक वेरिएबल के लिए एक अलग डोमेन <code>X::[1..5]</code>निर्दिष्ट किया जा सकता है उदाहरण के लिए इसका अर्थ यह है कि <code>X</code> के बीच है <code>1</code> और <code>5</code> है। एक वेरिएबल का डोमेन उन सभी मानों की गणना करके भी दिया जा सकता है जो एक वेरिएबल कर सकते हैं। इसलिए उपरोक्त डोमेन घोषणा को <code>X::[1,2,3,4,5]</code> भी लिखा जा सकता है। डोमेन निर्दिष्ट करने का यह दूसरा तरीका उन डोमेन के लिए स्वीकृति देता है जो पूर्णांकों से नहीं बने हैं। जैसे कि <code>X::[george,mary,john]</code> यदि एक वेरिएबल का डोमेन निर्दिष्ट नहीं है तो इसे भाषा में प्रतिनिधित्व करने योग्य पूर्णांकों का समूह<code>[X,Y,Z]::[1..5]</code> माना जाता है। जैसे घोषण पत्र का उपयोग करके वेरिएबल के समूह को एक ही डोमेन दिया जा सकता है।


निष्पादन के समय चर के डोमेन को कम किया जा सकता है। वास्तव में, जैसा कि अनुवादक बाधा संग्रह में बाधा डालता है, यह स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार करता है, और ये ऑपरेशन चर के डोमेन को कम कर सकते हैं। यदि किसी चर का डोमेन खाली हो जाता है, तो बाधा भंडार असंगत होता है, और एल्गोरिथम पीछे हट जाता है। यदि किसी चर का डोमेन एक सिंगलटन बन जाता है, तो चर को उसके डोमेन में अद्वितीय मान निर्दिष्ट किया जा सकता है। आमतौर पर प्रयुक्त की जाने वाली संगति के रूप आर्क संगति, हाइपर-आर्क संगति और बाध्य संगति हैं। एक चर के वर्तमान डोमेन का विशिष्ट शाब्दिक उपयोग करके निरीक्षण किया जा सकता है; उदाहरण के लिए, <code>dom(X,D)</code>) एक चर <code>D</code> के वर्तमान डोमेन <code>X</code> को ढूंढता है।
निष्पादन के समय वेरिएबल के डोमेन को कम किया जा सकता है। वास्तव में जैसा कि अनुवादक बाधा संग्रह में बाधा डालता है यह स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार करता है और ये संचालित वेरिएबल के डोमेन को कम कर सकते हैं। यदि किसी वेरिएबल का डोमेन रिक्त हो जाता है तो बाधा भंडार असंगत होता है और एल्गोरिथम पीछे हट जाता है। यदि किसी वेरिएबल का डोमेन एकल डोमेन बन जाता है तो वेरिएबल को उसके डोमेन में अद्वितीय मान निर्दिष्ट किया जा सकता है। सामान्यतः प्रयुक्त की जाने वाली संगति के रूप आर्क संगति, हाइपर-आर्क संगति और बाध्य संगति हैं। एक वेरिएबल के वर्तमान डोमेन का विशिष्ट शाब्दिक उपयोग करके निरीक्षण किया जा सकता है। उदाहरण के लिए <code>dom(X,D)</code>) एक वेरिएबल <code>D</code> के वर्तमान डोमेन <code>X</code> की खोज करता है।


रियल के डोमेन के लिए, फ़ंक्टर का उपयोग पूर्णांक के डोमेन के साथ किया जा सकता है। इस मामले में, एक पद पूर्णांकों पर एक व्यंजक हो सकता है, एक स्थिरांक हो सकता है, या अन्य पदों पर एक फ़ंक्टर का अनुप्रयोग हो सकता है। एक चर एक मनमाना शब्द मान के रूप में ले सकता है, यदि इसके डोमेन को पूर्णांक या स्थिरांक के सेट के रूप में निर्दिष्ट नहीं किया गया है।
वास्तविक डोमेन के लिए प्रकार्यक का उपयोग पूर्णांक के डोमेन के साथ किया जा सकता है। इस स्थिति में एक पद पूर्णांकों पर व्यंजक हो सकता है या एक स्थिरांक हो सकता है या अन्य पदों पर एक प्रकार्यक का अनुप्रयोग हो सकता है। एक वेरिएबल अपेखाकृत शब्द मान के रूप में ले सकता है। यदि इसके डोमेन को पूर्णांक या स्थिरांक के रूप में निर्दिष्ट नहीं किया गया है।


== बाधा भंडार ==
== बाधा भंडार ==


बाधा भंडार में वे कंस्ट्रेंट होते हैं जिन्हें वर्तमान में संतोषजनक माना जाता है। यह माना जा सकता है कि नियमित तर्क प्रोग्रामिंग के लिए वर्तमान प्रतिस्थापन क्या है। जब केवल ट्री शर्तों की स्वीकृति होती है, तो बाधा भंडार में<code>t1=t2</code> के रूप में कंस्ट्रेंट होते हैं; इन बाधाओं को एकीकरण द्वारा सरल किया जाता है, जिसके परिणामस्वरूप <code>variable=term</code> के रूप में बाधा उत्पन्न होती है; ऐसी बाधाएं एक प्रतिस्थापन के बराबर हैं।
बाधा भंडार में वे बाधा भंडार होते हैं जिन्हें वर्तमान में संतोषजनक माना जाता है। यह माना जा सकता है कि नियमित तर्क प्रोग्रामिंग के लिए वर्तमान प्रतिस्थापन क्या है। जब केवल ट्री शर्तों की स्वीकृति होती है तो बाधा भंडार में<code>t1=t2</code> के रूप में बाधा भंडार होते हैं इन बाधाओं को एकीकरण द्वारा सरल किया जाता है। जिसके परिणामस्वरूप <code>variable=term</code> के रूप में बाधा उत्पन्न होती है ऐसी बाधाएं एक प्रतिस्थापन के बराबर होती हैं।


हालाँकि, बाधा भंडार में <code>t1!=t2</code> के रूप में भी बाधाएँ हो सकती हैं, यदि अंतर ! = शर्तों के बीच की स्वीकृति है। जब वास्तविक या परिमित डोमेन पर बाधाओं की स्वीकृति दी जाती है, तो बाधा भंडार में डोमेन-विशिष्ट बाधाएँ भी हो सकती हैं जैसे <code>X+2=Y/2</code> आदि।
हालाँकि, बाधा भंडार में <code>t1!=t2</code> के रूप में भी बाधाएँ हो सकती हैं, यदि <code>!=</code> के बीच की स्वीकृति है। जब वास्तविक या परिमित डोमेन पर बाधाओं की स्वीकृति दी जाती है तो बाधा भंडार में डोमेन विशिष्ट बाधाएँ जैसे <code>X+2=Y/2</code>भी हो सकती हैं।


बाधा भंडार वर्तमान प्रतिस्थापन की अवधारणा को दो तरह से विस्तारित करता है। सबसे पहले, इसमें न केवल एक खंड के एक नए संस्करण के सिर के साथ एक शाब्दिक समानता से उत्पन्न बाधाएं सम्मिलित हैं, बल्कि खंडों के एल्गोरिदम की बाधाएं भी सम्मिलित हैं। दूसरा, इसमें न केवल फॉर्म <code>variable=value</code> की बाधाएं होती हैं बल्कि माना बाधा भाषा पर भी बाधाएं होती हैं। जबकि एक नियमित लॉजिक प्रोग्राम के सफल मूल्यांकन का परिणाम अंतिम प्रतिस्थापन है, एक कंस्ट्रेंट लॉजिक प्रोग्राम का परिणाम अंतिम बाधा भंडार है, जिसमें फॉर्म <code>variable=value</code> का कंस्ट्रेंट हो सकता है लेकिन सामान्य रूप से मनमाना प्रतिबंध हो सकता है।
बाधा भंडार वर्तमान प्रतिस्थापन की अवधारणा को दो प्रकार से विस्तारित करता है। सबसे पहले इसमें न केवल एक खंड के एक नए संस्करण के भाग के साथ एक शाब्दिक समानता से उत्पन्न बाधाएं सम्मिलित हैं बल्कि खंडों के एल्गोरिदम की बाधाएं भी सम्मिलित हैं। दूसरा इसमें न केवल <code>variable=value</code> के रूप मे बाधाएं होती हैं। मानक बाधा भाषा पर भी बाधाएं होती हैं। जबकि एक नियमित तर्क प्रोग्राम के सफल मूल्यांकन का परिणाम अंतिम प्रतिस्थापन है एक बाधा तर्क प्रोग्राम का परिणाम अंतिम बाधा भंडार है। जिसमें <code>variable=value</code> का रूप बाधा हो सकता है लेकिन सामान्य रूप से अपेक्षाकृत प्रतिबंध हो सकता है।


डोमेन-विशिष्ट बाधाएँ क्लॉज़ के एल्गोरिदम से और क्लॉज़ हेड के साथ एक शाब्दिक समानता से बाधा भंडार में आ सकती हैं: उदाहरण के लिए, यदि अनुवादक शाब्दिक <code>A(X+2)</code> को एक क्लॉज़ के साथ फिर से लिखता है जिसका ताज़ा वेरिएंट हेड है <code>A(Y/2)</code>, बाधा <code>X+2=Y/2</code> बाधा भंडार में जोड़ा गया है। यदि एक चर वास्तविक या परिमित डोमेन अभिव्यक्ति में प्रकट होता है, तो यह केवल वास्तविक या परिमित डोमेन में मान ले सकता है। इस प्रकार का एक चर मूल्य के रूप में अन्य शर्तों पर प्रयुक्त एक फ़ंक्टर से बने शब्द को नहीं ले सकता है। बाधा भंडार असंतोषजनक है यदि एक चर विशिष्ट डोमेन के मान और शर्तों पर प्रयुक्त फ़ंक्टर दोनों को लेने के लिए बाध्य है।
डोमेन-विशिष्ट बाधाएँ एल्गोरिदम से और मुख्य भाग के साथ एक शाब्दिक समानता से बाधा भंडार में आ सकती हैं। उदाहरण के लिए यदि अनुवादक शाब्दिक <code>A(X+2)</code> को एक बाधा के साथ फिर से लिखता है जिसका नया संस्कारण <code>A(Y/2)</code> है तब <code>X+2=Y/2</code> को बाधा भंडार में जोड़ा जा सकता है। यदि एक वेरिएबल वास्तविक या परिमित डोमेन अभिव्यक्ति में प्रकट होता है, तो यह केवल वास्तविक या परिमित डोमेन में मान ले सकता है। इस प्रकार का एक वेरिएबल मान के रूप में अन्य शर्तों पर प्रयुक्त एक प्रकार्यक से बने शब्द को नहीं ले सकता है। बाधा भंडार असंतोषजनक है यदि एक वेरिएबल विशिष्ट डोमेन के मान और शर्तों पर प्रयुक्त प्रकार्यक दोनों को लेने के लिए बाध्य है।


बाधा भंडार में कंस्ट्रेंट जोड़े जाने के बाद, बाधा भंडार पर कुछ ऑपरेशन किए जाते हैं। कौन से ऑपरेशन किए जाते हैं यह माना जाने वाले डोमेन और बाधाओं पर निर्भर करता है। उदाहरण के लिए, एकीकरण का उपयोग परिमित वृक्ष समानता के लिए किया जाता है, वास्तविक से अधिक बहुपद समीकरणों के लिए चर उन्मूलन, परिमित डोमेन के लिए स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार। इन परिचालनों का लक्ष्य संतोषप्रदता की जांच और समाधान के लिए बाधा भंडार को आसान बनाना है।
बाधा भंडार में बाधा जोड़े जाने के बाद बाधा भंडार पर कुछ संचालन किए जाते हैं। कौन से संचालन किए जाते हैं यह माना जाने वाले डोमेन और बाधाओं पर निर्भर करता है। उदाहरण के लिए, एकीकरण का उपयोग परिमित ट्री समानता के लिए किया जाता है। वास्तविक से अधिक बहुपद समीकरणों के लिए वेरिएबल उन्मूलन, परिमित डोमेन के लिए स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार इन परिचालनों का लक्ष्य संतोषप्रदता की जांच और समाधान के लिए बाधा भंडार को आसान बनाना है।


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


== लेबलिंग ==
== लेबलिंग ==


लेबलिंग लिटरल का उपयोग बाधा भंडार की संतुष्टि या आंशिक संतुष्टि की जांच करने और एक संतोषजनक असाइनमेंट खोजने के लिए परिमित डोमेन पर चर पर किया जाता है। एक लेबलिंग शाब्दिक प्रपत्र <code>labeling([variables])</code> का होता है, जहां तर्क परिमित डोमेन पर चर की एक सूची है। जब भी अनुवादक इस प्रकार के शाब्दिक का मूल्यांकन करता है, तो यह सूची के चर के डोमेन पर खोज करता है ताकि सभी प्रासंगिक बाधाओं को पूरा करने वाले असाइनमेंट को ढूंढा जा सके। आमतौर पर, यह बैकट्रैकिंग के एक रूप द्वारा किया जाता है: चर का मूल्यांकन क्रम में किया जाता है, उनमें से प्रत्येक के लिए सभी संभावित मानों का प्रयास किया जाता है, और असंगतता का पता चलने पर बैकट्रैकिंग की जाती है।
लेबलिंग लिटरल का उपयोग बाधा भंडार की संतुष्टि या आंशिक संतुष्टि की जांच करने और एक संतोषजनक असाइनमेंट खोजने के लिए परिमित डोमेन पर वेरिएबल पर किया जाता है। एक लेबलिंग शाब्दिक प्रपत्र <code>labeling([variables])</code> का होता है, जहां तर्क परिमित डोमेन पर वेरिएबल की एक सूची है। जब भी अनुवादक इस प्रकार के शाब्दिक का मूल्यांकन करता है, तो यह सूची के वेरिएबल के डोमेन पर खोज करता है ताकि सभी प्रासंगिक बाधाओं को पूरा करने वाले असाइनमेंट को ढूंढा जा सके। आमतौर पर, यह बैकट्रैकिंग के एक रूप द्वारा किया जाता है: वेरिएबल का मूल्यांकन क्रम में किया जाता है, उनमें से प्रत्येक के लिए सभी संभावित मानों का प्रयास किया जाता है, और असंगतता का पता चलने पर बैकट्रैकिंग की जाती है।


लेबलिंग शाब्दिक का पहला उपयोग वास्तविक जांच संतुष्टि या बाधा भंडार की आंशिक संतुष्टि के लिए है। जब अनुवादक बाधा संग्रह में बाधा जोड़ता है, तो यह केवल उस पर स्थानीय स्थिरता का एक रूप प्रयुक्त करता है। यह ऑपरेशन असंगतता का पता नहीं लगा सकता है, भले ही बाधा भंडार असंतोषजनक हो। चर के एक सेट पर शाब्दिक लेबलिंग इन चरों पर बाधाओं की संतुष्टि जांच को प्रयुक्त करता है। जिसके परिणाम स्वरूप, बाधा भंडार में उल्लिखित सभी चर का उपयोग करने से भंडार की संतुष्टि की जांच होती है।
लेबलिंग शाब्दिक का पहला उपयोग वास्तविक जांच संतुष्टि या बाधा भंडार की आंशिक संतुष्टि के लिए है। जब अनुवादक बाधा संग्रह में बाधा जोड़ता है, तो यह केवल उस पर स्थानीय स्थिरता का एक रूप प्रयुक्त करता है। यह ऑपरेशन असंगतता का पता नहीं लगा सकता है, भले ही बाधा भंडार असंतोषजनक हो। वेरिएबल के एक सेट पर शाब्दिक लेबलिंग इन चरों पर बाधाओं की संतुष्टि जांच को प्रयुक्त करता है। जिसके परिणाम स्वरूप, बाधा भंडार में उल्लिखित सभी वेरिएबल का उपयोग करने से भंडार की संतुष्टि की जांच होती है।


लेबलिंग शाब्दिक का दूसरा उपयोग वास्तव में उन चरों का मूल्यांकन निर्धारित करना है जो बाधा भंडार को संतुष्ट करते हैं। शाब्दिक लेबलिंग के बिना, वेरिएबल्स को केवल तभी मान दिया जाता है जब बाधा भंडार में <code>X=value</code> के रूप में एक बाधा होती है और जब स्थानीय संगति एक चर के डोमेन को एक मान तक कम कर देती है। कुछ चरों पर शाब्दिक लेबलिंग इन चरों का मूल्यांकन करने के लिए बाध्य करता है। दूसरे शब्दों में, शाब्दिक लेबलिंग पर विचार करने के बाद, सभी चरों को एक मान निर्दिष्ट किया जाता है।
लेबलिंग शाब्दिक का दूसरा उपयोग वास्तव में उन चरों का मूल्यांकन निर्धारित करना है जो बाधा भंडार को संतुष्ट करते हैं। शाब्दिक लेबलिंग के बिना, वेरिएबल्स को केवल तभी मान दिया जाता है जब बाधा भंडार में <code>X=value</code> के रूप में एक बाधा होती है और जब स्थानीय संगति एक वेरिएबल के डोमेन को एक मान तक कम कर देती है। कुछ चरों पर शाब्दिक लेबलिंग इन चरों का मूल्यांकन करने के लिए बाध्य करता है। दूसरे शब्दों में, शाब्दिक लेबलिंग पर विचार करने के बाद, सभी चरों को एक मान निर्दिष्ट किया जाता है।


आम तौर पर, बाधा तर्क प्रोग्राम इस प्रकार से लिखे जाते हैं कि लेबलिंग अक्षर का मूल्यांकन बाधा भंडार में जितनी संभव हो उतनी बाधाओं के बाद ही किया जाता है। ऐसा इसलिए है क्योंकि शाब्दिक लेबलिंग खोज को प्रयुक्त करती है, और संतुष्ट होने के लिए अधिक बाधाएं होने पर खोज अधिक कुशल होती है। निम्नलिखित संरचना वाले बाधा तर्क प्रोग्राम द्वारा एक बाधा संतुष्टि समस्या को सामान्य रूप से हल किया जाता है:
आम तौर पर, बाधा तर्क प्रोग्राम इस प्रकार से लिखे जाते हैं कि लेबलिंग अक्षर का मूल्यांकन बाधा भंडार में जितनी संभव हो उतनी बाधाओं के बाद ही किया जाता है। ऐसा इसलिए है क्योंकि शाब्दिक लेबलिंग खोज को प्रयुक्त करती है, और संतुष्ट होने के लिए अधिक बाधाएं होने पर खोज अधिक कुशल होती है। निम्नलिखित संरचना वाले बाधा तर्क प्रोग्राम द्वारा एक बाधा संतुष्टि समस्या को सामान्य रूप से हल किया जाता है:
Line 127: Line 123:
समानता कुछ बाधाओं को सरल लोगों के साथ बदलकर बाधा संग्रह को सरल बनाने की स्वीकृति देती है; विशेष रूप से, यदि एक तुल्यता नियम में तीसरी बाधा <code>true</code> है, और दूसरी बाधा सम्मिलित है, तो पहली बाधा बाधा संग्रह से हटा दी जाती है। अनुमान नई बाधाओं को जोड़ने की स्वीकृति देता है, जिससे बाधा भंडार की असंगतता सिद्ध हो सकती है, और आमतौर पर इसकी संतुष्टि को स्थापित करने के लिए आवश्यक खोज की मात्रा कम हो सकती है।
समानता कुछ बाधाओं को सरल लोगों के साथ बदलकर बाधा संग्रह को सरल बनाने की स्वीकृति देती है; विशेष रूप से, यदि एक तुल्यता नियम में तीसरी बाधा <code>true</code> है, और दूसरी बाधा सम्मिलित है, तो पहली बाधा बाधा संग्रह से हटा दी जाती है। अनुमान नई बाधाओं को जोड़ने की स्वीकृति देता है, जिससे बाधा भंडार की असंगतता सिद्ध हो सकती है, और आमतौर पर इसकी संतुष्टि को स्थापित करने के लिए आवश्यक खोज की मात्रा कम हो सकती है।


कंस्ट्रेंट हैंडलिंग नियमों के संयोजन में तार्किक प्रोग्रामिंग क्लॉज का उपयोग बाधा भंडार की संतुष्टि की स्थापना के लिए एक विधि निर्दिष्ट करने के लिए किया जा सकता है। विधि के विभिन्न विकल्पों को प्रयुक्त करने के लिए विभिन्न खंडों का उपयोग किया जाता है; निष्पादन के समय बाधा भंडार को फिर से लिखने के लिए बाधा प्रबंधन नियमों का उपयोग किया जाता है। एक उदाहरण के रूप में, इकाई प्रसार के साथ बैकट्रैकिंग को इस प्रकार प्रयुक्त किया जा सकता है। चलो <code>holds(L)</code> एक प्रस्तावक खंड का प्रतिनिधित्व करता है, जिसमें सूची <code>L</code> में अक्षर उसी क्रम में होते हैं जैसे उनका मूल्यांकन किया जाता है। एल्गोरिथम को सही या गलत के लिए शाब्दिक निर्दिष्ट करने के विकल्प के लिए क्लॉज का उपयोग करके प्रयुक्त किया जा सकता है, और प्रसार को निर्दिष्ट करने के लिए बाधाओं से निपटने के नियमों को प्रयुक्त किया जा सकता है। ये नियम निर्दिष्ट करते हैं कि <code>holds([l|L])</code> को हटाया जा सकता है यदि भंडार से <code>l=true</code> होता है, और इसे <code>holds(L)</code> के रूप में फिर से लिखा जा सकता है यदि <code>l=false</code> भंडार से अनुसरण करता है। इसी तरह, <code>holds([l])</code> को <code>l=true</code> से परिवर्तित जा सकता है। इस उदाहरण में, तर्क प्रोग्रामिंग के खंडों का उपयोग करके एक चर के लिए मान का चुनाव कार्यान्वित किया जाता है; हालांकि, इसे डिसजंक्टिव कंस्ट्रेंट हैंडलिंग रूल्स या CHR∨ नामक एक्सटेंशन का उपयोग करके बाधा प्रबंधन नियमों में एन्कोड किया जा सकता है।
कंस्ट्रेंट हैंडलिंग नियमों के संयोजन में तार्किक प्रोग्रामिंग क्लॉज का उपयोग बाधा भंडार की संतुष्टि की स्थापना के लिए एक विधि निर्दिष्ट करने के लिए किया जा सकता है। विधि के विभिन्न विकल्पों को प्रयुक्त करने के लिए विभिन्न खंडों का उपयोग किया जाता है; निष्पादन के समय बाधा भंडार को फिर से लिखने के लिए बाधा प्रबंधन नियमों का उपयोग किया जाता है। एक उदाहरण के रूप में, इकाई प्रसार के साथ बैकट्रैकिंग को इस प्रकार प्रयुक्त किया जा सकता है। चलो <code>holds(L)</code> एक प्रस्तावक खंड का प्रतिनिधित्व करता है, जिसमें सूची <code>L</code> में अक्षर उसी क्रम में होते हैं जैसे उनका मूल्यांकन किया जाता है। एल्गोरिथम को सही या गलत के लिए शाब्दिक निर्दिष्ट करने के विकल्प के लिए क्लॉज का उपयोग करके प्रयुक्त किया जा सकता है, और प्रसार को निर्दिष्ट करने के लिए बाधाओं से निपटने के नियमों को प्रयुक्त किया जा सकता है। ये नियम निर्दिष्ट करते हैं कि <code>holds([l|L])</code> को हटाया जा सकता है यदि भंडार से <code>l=true</code> होता है, और इसे <code>holds(L)</code> के रूप में फिर से लिखा जा सकता है यदि <code>l=false</code> भंडार से अनुसरण करता है। इसी तरह, <code>holds([l])</code> को <code>l=true</code> से परिवर्तित जा सकता है। इस उदाहरण में, तर्क प्रोग्रामिंग के खंडों का उपयोग करके एक वेरिएबल के लिए मान का चुनाव कार्यान्वित किया जाता है; हालांकि, इसे डिसजंक्टिव कंस्ट्रेंट हैंडलिंग रूल्स या CHR∨ नामक एक्सटेंशन का उपयोग करके बाधा प्रबंधन नियमों में एन्कोड किया जा सकता है।


== बॉटम-अप मूल्यांकन ==
== बॉटम-अप मूल्यांकन ==
Line 152: Line 148:
बॉटम-अप रणनीति में वही खामी नहीं है, क्योंकि जो परिणाम पहले ही प्राप्त हो चुके हैं, उनका कोई प्रभाव नहीं पड़ता है। उपरोक्त प्रोग्राम पर, बॉटम-अप रणनीति परिणामों के सेट में <code>A(q)</code> को जोड़ना शुरू करती है; दूसरे चरण में,<code>B(X):-A(X)</code> का उपयोग <code>B(q)</code> को प्राप्त करने के लिए किया जाता है; तीसरे चरण में, वर्तमान परिणामों से प्राप्त होने वाले एकमात्र तथ्य <code>A(q)</code> और <code>B(q)</code> हैं, जो पहले से ही परिणामों के सेट में हैं। जिसके परिणाम स्वरूप, एल्गोरिथ्म बंद हो जाता है।
बॉटम-अप रणनीति में वही खामी नहीं है, क्योंकि जो परिणाम पहले ही प्राप्त हो चुके हैं, उनका कोई प्रभाव नहीं पड़ता है। उपरोक्त प्रोग्राम पर, बॉटम-अप रणनीति परिणामों के सेट में <code>A(q)</code> को जोड़ना शुरू करती है; दूसरे चरण में,<code>B(X):-A(X)</code> का उपयोग <code>B(q)</code> को प्राप्त करने के लिए किया जाता है; तीसरे चरण में, वर्तमान परिणामों से प्राप्त होने वाले एकमात्र तथ्य <code>A(q)</code> और <code>B(q)</code> हैं, जो पहले से ही परिणामों के सेट में हैं। जिसके परिणाम स्वरूप, एल्गोरिथ्म बंद हो जाता है।


उपरोक्त उदाहरण में, केवल प्रयुक्त तथ्य ग्राउंड लिटरल थे। सामान्य तौर पर, प्रत्येक खंड जिसमें केवल एल्गोरिदम में बाधाएँ होती हैं, एक तथ्य माना जाता है। उदाहरण के लिए, एक खंड <code>A(X):-X>0,X<10</code> तथ्य भी माना जाता है। तथ्यों की इस विस्तारित परिभाषा के लिए, कुछ तथ्य समतुल्य हो सकते हैं, जबकि वाक्यात्मक रूप से समान नहीं। उदाहरण के लिए, <code>A(q)</code> के बराबर है <code>A(X):-X=q</code> और दोनों के बराबर हैं <code>A(X):-X=Y, Y=q</code>. इस समस्या को हल करने के लिए, तथ्यों को सामान्य रूप में अनुवादित किया जाता है जिसमें सिर में सभी अलग-अलग चरों का एक टपल होता है; दो तथ्य तब समतुल्य होते हैं यदि उनके एल्गोरिदम सिर के चर पर समतुल्य होते हैं, अर्थात, इन चरों तक सीमित होने पर उनके समाधान के सेट समान होते हैं।
उपरोक्त उदाहरण में, केवल प्रयुक्त तथ्य ग्राउंड लिटरल थे। सामान्य तौर पर, प्रत्येक खंड जिसमें केवल एल्गोरिदम में बाधाएँ होती हैं, एक तथ्य माना जाता है। उदाहरण के लिए, एक खंड <code>A(X):-X>0,X<10</code> तथ्य भी माना जाता है। तथ्यों की इस विस्तारित परिभाषा के लिए, कुछ तथ्य समतुल्य हो सकते हैं, जबकि वाक्यात्मक रूप से समान नहीं। उदाहरण के लिए, <code>A(q)</code> के बराबर है <code>A(X):-X=q</code> और दोनों के बराबर हैं <code>A(X):-X=Y, Y=q</code>. इस समस्या को हल करने के लिए, तथ्यों को सामान्य रूप में अनुवादित किया जाता है जिसमें सिर में सभी अलग-अलग चरों का एक टपल होता है; दो तथ्य तब समतुल्य होते हैं यदि उनके एल्गोरिदम सिर के वेरिएबल पर समतुल्य होते हैं, अर्थात, इन चरों तक सीमित होने पर उनके समाधान के सेट समान होते हैं।


जैसा कि वर्णन किया गया है, बॉटम-अप दृष्टिकोण में उन परिणामों पर विचार न करने का लाभ है जो पहले ही प्राप्त हो चुके हैं। हालाँकि, यह अभी भी उन परिणामों को प्राप्त कर सकता है जो उनमें से किसी के बराबर नहीं होने के बावजूद पहले से प्राप्त किए गए हैं। एक उदाहरण के रूप में, निम्न प्रोग्राम का नीचे से ऊपर का मूल्यांकन अनंत है:
जैसा कि वर्णन किया गया है, बॉटम-अप दृष्टिकोण में उन परिणामों पर विचार न करने का लाभ है जो पहले ही प्राप्त हो चुके हैं। हालाँकि, यह अभी भी उन परिणामों को प्राप्त कर सकता है जो उनमें से किसी के बराबर नहीं होने के बावजूद पहले से प्राप्त किए गए हैं। एक उदाहरण के रूप में, निम्न प्रोग्राम का नीचे से ऊपर का मूल्यांकन अनंत है:
Line 160: Line 156:
A(X):-X=Y+1, A(Y).
A(X):-X=Y+1, A(Y).
</syntaxhighlight>
</syntaxhighlight>
बॉटम-अप इवैल्यूएशन एल्गोरिद्म सबसे पहले यह निकालता है कि <code>A(X)</code> <code>X=0</code> और <code>X>0</code> के लिए सही है। दूसरे चरण में, तीसरे खंड के साथ पहला तथ्य <code>A(1)</code> की व्युत्पत्ति के लिए स्वीकृति देता है। तीसरे चरण में, <code>A(2)</code> व्युत्पन्न होता है, आदि। हालाँकि, ये तथ्य पहले से ही इस तथ्य से जुड़े हुए हैं कि <code>A(X)</code> किसी भी गैर-नकारात्मक X के लिए सत्य है। परिणामों के वर्तमान सेट में जोड़ा गया। यदि नया परिणाम सेट द्वारा पहले से ही उलझा हुआ है, तो उसे इसमें नहीं जोड़ा जाता है। चूंकि तथ्यों को खंड के रूप में संग्रहीत किया जाता है, संभवतः "स्थानीय चर" के साथ, उनके सिर के चर पर प्रवेश प्रतिबंधित है।
बॉटम-अप इवैल्यूएशन एल्गोरिद्म सबसे पहले यह निकालता है कि <code>A(X)</code> <code>X=0</code> और <code>X>0</code> के लिए सही है। दूसरे चरण में, तीसरे खंड के साथ पहला तथ्य <code>A(1)</code> की व्युत्पत्ति के लिए स्वीकृति देता है। तीसरे चरण में, <code>A(2)</code> व्युत्पन्न होता है, आदि। हालाँकि, ये तथ्य पहले से ही इस तथ्य से जुड़े हुए हैं कि <code>A(X)</code> किसी भी गैर-नकारात्मक X के लिए सत्य है। परिणामों के वर्तमान सेट में जोड़ा गया। यदि नया परिणाम सेट द्वारा पहले से ही उलझा हुआ है, तो उसे इसमें नहीं जोड़ा जाता है। चूंकि तथ्यों को खंड के रूप में संग्रहीत किया जाता है, संभवतः "स्थानीय चर" के साथ, उनके सिर के वेरिएबल पर प्रवेश प्रतिबंधित है।


== समवर्ती बाधा तर्क प्रोग्रामिंग ==
== समवर्ती बाधा तर्क प्रोग्रामिंग ==

Revision as of 11:24, 19 May 2023

बाधा तर्क प्रोग्रामिंग बाधा प्रोग्रामिंग का एक रूप है जिसमें बाधा संतुष्टि की अवधारणाओं को सम्मिलित करने के लिए तर्क प्रोग्रामिंग को विस्तृत जाता है। एक बाधा तर्क प्रोग्राम एक तर्क प्रोग्राम है जिसके डेटा में भौतिकी बाधाएं होती हैं। बाधा सहित तर्क का एक उदाहरण A(X,Y) :- X+Y>0, B(X), C(Y) है इस भाग में X+Y>0 एक बाधा है जो A(X,Y), B(X) और C(Y) के नियमित तर्क प्रोग्रामिंग के रूप में शाब्दिक (गणितीय तर्क) हैं। यह तर्क एक नियम का अनुसरण करता है। जिसके अंतर्गत कथन A(X,Y) X+Y शून्य से अधिक होता है। जिससे B(X) और C(Y) दोनों सत्य होते हैं।

जैसा कि नियमित तार्किक प्रोग्रामिंग भाषा में होता है। प्रोग्रामों से किसी लक्ष्य की उपयोगिता के विषय में जानकारी प्राप्त की जाती है। जिसमें शाब्दिक तर्क के अतिरिक्त बाधाएँ भी हो सकती हैं। यह लक्ष्य के लिए एक प्रमाण उन खंडों से बना होता है जिनकी भौतिक संतोषजनक बाधाएँ और शाब्दिक होती हैं जो परिवर्तन में अन्य खंडों का उपयोग करके सिद्ध की जा सकती हैं। इनका निष्पादन एक अनुवादक द्वारा किया जाता है, जो लक्ष्य से प्रारम्भ होता है और लक्ष्य को सिद्ध करने के प्रयास कर रहे खंडों का पुनः अवलोकन करता है। इस अवलोकन के समय आने वाली बाधाओं को एक भंडारण में रखा जाता है जिसे बाधा भंडार कहा जाता है। यदि यह भंडारण असंतोषजनक पाया जाता है तो अनुवादक पीछे हट जाता है और लक्ष्य को सिद्ध करने के लिए अन्य खंडों का उपयोग करने का प्रयास करता है। सामान्यतः एक अपूर्ण एल्गोरिदम का उपयोग करके बाधा भंडार की संतुष्टि की जांच की जा सकती है, जो सदैव असंगतता का पता नहीं लगाती है।

समीक्षा

औपचारिक रूप से बाधा तर्क प्रोग्राम नियमित तर्क प्रोग्रामों की तरह होते हैं, लेकिन भौतिकी भाग में नियमित तर्क प्रोग्रामिंग शाब्दिक तर्क के अतिरिक्त बाधाएं हो सकती हैं। एक उदाहरण के रूप में X>0 एक बाधा है और निम्नलिखित बाधा तर्क प्रोग्राम के अंतिम भाग में सम्मिलित है।

B(X,1):- X<0.
B(X,Y):- X=1, Y>0.
A(X,Y):- X>0, B(X,Y).

नियमित तर्क प्रोग्रामिंग की तरह A(X,1) जैसे लक्ष्य का मूल्यांकन करने के लिए Y=1 के साथ अंतिम भाग के एल्गोरिदम का मूल्यांकन करने की आवश्यकता होती है। नियमित तार्किक प्रोग्रामिंग की तरह, इसके परिवर्तित लक्ष्य B(X,1) को सिद्ध करने की आवश्यकता होती है। नियमित तार्किक प्रोग्रामिंग के विपरीत, इसके लिए X>0 को संतुष्ट करने के लिए एक बाधा की भी आवश्यकता होती है। अंतिम भाग के एल्गोरिदम में बाधा नियमित तार्किक प्रोग्रामिंग में X>0 को तब तक सिद्ध नहीं किया जा सकता है जब तक कि X पूरी तरह से मूल रूप मे और निष्पादन के लिए बाध्य न हो। यदि ऐसा नहीं होता है तो प्रोग्राम विफल हो सकता है।

जब बाधा का सामना करना पड़ता है तो एक बाधा संतुष्ट होती है या नहीं संतुष्ट होती है यह सदैव निर्धारित नहीं किया जा सकता है। इस स्थिति में उदाहरण के लिए X का मान निर्धारित नहीं होता है जब अंतिम भाग का मूल्यांकन किया जाता है। जिसके परिणाम स्वरूप, इस बिंदु पर बाधा X>0 संतुष्ट नहीं है और न ही इसका उल्लंघन किया गया है। B(X,1) के मूल्यांकन में आगे बढ़ने और फिर जाँचने के अतिरिक्त कि क्या X का परिणामी मान बाद में धनात्मक है अनुवादक बाधा X>0 को संग्रहीत करता है और फिर B(X,1)के मूल्यांकन में आगे बढ़ता है इस प्रकार अनुवादक B(X,1) के मूल्यांकन के समय बाधा X>0 के उल्लंघन का पता लगा सकता है और B(X,1)के मूल्यांकन के निष्कर्ष की प्रतीक्षा करने के अतिरिक्त, यदि यह स्थिति है तो शीघ्र पीछे हट जाता है।

सामान्यतः बाधा तर्क प्रोग्राम का मूल्यांकन एक नियमित तर्क प्रोग्राम के रूप में होता है। हालाँकि, मूल्यांकन के समय आने वाली बाधाओं को एक बाधा भंडारण में रखा जाता है। जिसे एक बाधा भंडार कहा जाता है। एक उदाहरण के रूप में लक्ष्य A(X,1) का मूल्यांकन Y=1 के साथ पहले खंड के एल्गोरिदम का मूल्यांकन करके आगे बढ़ता है यह मूल्यांकन X>0 को बाधा भंडार में जोड़ता है और लक्ष्य B(X,1) को सिद्ध करने की आवश्यकता होती है। इस लक्ष्य को सिद्ध करने का प्रयास करते समय पहला भाग प्रयुक्त किया जाता है लेकिन इसका मूल्यांकन X<0 को बाधा भंडार में जोड़ता है। यह जोड़ बाधा भंडार को असंतोषजनक बनाता है। जिससे अनुवादक फिर पीछे हट जाता है और बाधा भंडार से अंतिम योग को हटा देता है। दूसरे एल्गोरिदम का मूल्यांकन X=1 और Y>0 को बाधा भंडार में जोड़ता है। चूंकि बाधा भंडार संतोषजनक है और सिद्ध करने के लिए कोई अन्य शाब्दिक तर्क नहीं है इसीलिए अनुवादक समाधान X=1, Y=1 के साथ स्थगित हो जाता है।

शब्दार्थ

बाधा तर्क प्रोग्रामों के शब्दार्थ को एक आभासी अनुवादक के संदर्भ में परिभाषित किया जा सकता है जो निष्पादन के समय एक युग्म को बनाए रखता है। इस युग्म के पहले तत्व को वर्तमान लक्ष्य कहा जाता है दूसरे तत्व को बाधा भंडार कहा जाता है। वर्तमान लक्ष्य में वे अक्षर सम्मिलित हैं जिन्हें अनुवादक सिद्ध करने का प्रयास कर रहा है और इसमें कुछ बाधाएँ भी हो सकती हैं जिन्हें वह संतुष्ट करने का प्रयास कर रहा है। बाधा भंडार में वे सभी बाधाए सम्मिलित हैं जिन्हें अनुवादक ने अब तक संतोषजनक माना है।

प्रारंभ में वर्तमान अवधारणा एक लक्ष्य है जिसमे बाधा भंडार रिक्त होता है। अनुवादक पहले तत्व को वर्तमान लक्ष्य से हटाकर और उसका विश्लेषण करके आगे बढ़ता है। इस विश्लेषण का विवरण नीचे समझाया गया है, लेकिन अंत में यह विश्लेषण सफल समाप्ति या विफलता उत्पन्न कर सकता है। इस विश्लेषण में पुनरावर्ती कॉल सम्मिलित हो सकती हैं और सम्मिलित लक्ष्य के लिए नए अक्षर और बाधा भंडार में नई बाधा सम्मिलित हो सकती है। यदि कोई विफलता उत्पन्न होती है तो अनुवादक पीछे हट जाता है। एक सफल समाप्ति तब उत्पन्न होती है जब वर्तमान लक्ष्य रिक्त होता है और बाधा संग्रह संतोषजनक होती है।

लक्ष्य से हटाए गए शाब्दिक तर्क के विश्लेषण का विवरण इस प्रकार है। लक्ष्य के सामने से इस शाब्दिक तर्क को हटाने के बाद यह जाँच की जाती है कि यह एक बाधा है या एक शाब्दिक तर्क है। यदि यह एक बाधा है, तो इसे बाधा भंडार में जोड़ा जाता है। यदि यह एक शाब्दिक तर्क है तब इसको शाब्दिक तर्क के समान विधेय मे चुना जाता है एल्गोरिदम को उसके वेरिएबल्स को नए वेरिएबल्स (लक्ष्य में नहीं होने वाले वेरिएबल्स) के साथ परिवर्तित करके पुनः लिखा जाता है। परिणाम को एल्गोरिदम का एक नया संस्करण कहा जाता है। इसके बाद भाग के नए संस्करण का मुख्य भाग लक्ष्य के सामने रखा जाता है। जिससे शाब्दिक तर्क के प्रत्येक तर्क की समानता नए संस्करण के मुख्य भाग से संबंधित एक साथ लक्ष्य के सामने भी रखी गई है। इन प्रोग्रामों के समय कुछ जाँचें की जाती हैं। विशेष रूप से प्रत्येक समय एक नई बाधा जोड़े जाने पर बाधा भंडार की स्थिरता के लिए जाँच की जाती है। सिद्धांतिक रूप में जब भी बाधा भंडार असंतुष्ट होता है। एल्गोरिथ्म पीछे हट सकता है। हालाँकि प्रत्येक चरण पर असंतोष की जाँच अक्षम होती है इस कारण से इसके स्थान पर अपूर्ण संतुष्टि जाँचकर्ता का उपयोग किया जा सकता है। सामान्यतः संतोषजनक तर्क की जाँच उन तरीकों का उपयोग करके की जाती है जो बाधा संग्रह को सरल बनाते हैं और जो कि इसे समतुल्य लेकिन हल करने के लिए सरल रूप में फिर से लिखते हैं। ये विधियां कभी-कभी असंतोषजनक बाधा भंडार की असंतोषजनकता सिद्ध कर सकती हैं लेकिन सदैव ऐसा नहीं होता है।

अनुवादक ने लक्ष्य को सिद्ध कर दिया था जब वर्तमान लक्ष्य रिक्त था और बाधा भंडार को असंतोषजनक नहीं पाया गया है। निष्पादन का परिणाम (सरलीकृत) बाधाओं का वर्तमान समूह है। इस समूह में जैसे बाधा सम्मिलित हो सकती हैं जो वेरिएबल (चर) को एक विशिष्ट मान के लिए बाध्य करती हैं लेकिन इसमें जैसे बाधा भी सम्मिलित हो सकती हैं जो केवल वेरिएबल को एक विशिष्ट मान दिए बिना बाध्य करती हैं।

औपचारिक रूप से, बाधा तर्क प्रोग्रामिंग के शब्दों को व्युत्पत्तियों के संदर्भ में परिभाषित किया गया है। प्रसंस्करण युग्म लक्ष्य या भंडार युग्म द्वारा निर्धारित किए गए युग्म एक युग्म है। इस प्रकार की युग्मों की स्थिति से तक जाने की संभावना है।

  • G का एक तत्व C की बाधा और है। दूसरे शब्दों में, एक बाधा को लक्ष्य से बाधा भंडार में ले जाया जा सकता है।
  • G का तत्व एक शाब्दिक तर्क है जिसमे एक भाग सम्मिलित है जो नए वेरिएबल का उपयोग करके फिर से , लिखा गया है। G के साथ द्वारा प्रतिस्थापित , और है। दूसरे शब्दों में, एक शाब्दिक तर्क को एक खंड के नए संस्करण के एल्गोरिदम द्वारा प्रतिस्थापित किया जा सकता है। जिसमें नए संस्करण के एल्गोरिदम और लक्ष्य के शब्दों की उपरोक्त समानताएं जोड़ते हुए एक भाग में समान विधेय होता है।
  • S और विशिष्ट बाधा शब्दार्थ के अनुसार समान हैं।

प्रसंस्करण का अनुक्रम एक व्युत्पत्ति है। एक लक्ष्य G सिद्ध किया जा सकता है यदि वहाँ से कोई व्युत्पत्ति सम्मिलित है। को के संतोषजनक बाधा भंडार के लिए S शब्दार्थ के अनुवादक के संभावित विकास को औपचारिक रूप देता है जो अपेक्षाकृत रूप से प्रक्रिया के लक्ष्य का शाब्दिक चयन करता है और शाब्दिक तर्क को परिवर्तित करने के लिए खंड को दूसरे शब्दों में इस शब्दार्थ के अंतर्गत एक लक्ष्य सिद्ध होता है यदि शाब्दिक तर्क और खंडों के विकल्पों का एक क्रम सम्मिलित होता है। संभवतः कई लोगों के बीच जो एक रिक्त लक्ष्य और संतोषजनक भंडार की ओर ले जाता है।

वास्तविक अनुवादक लक्ष्य तत्वों को एलआईएफओ क्रम में संसाधित करते हैं तत्वों को सामने से जोड़ा जाता है और सामने से संसाधित किया जाता है। वे उस क्रम के अनुसार दूसरे नियम का खंड भी चुनते हैं जिसमें वे लिखे गए हैं और संशोधित होने पर बाधा संग्रह को फिर से लिखते हैं।

तीसरा संभावित प्रकार का प्रसंस्करण समतुल्य भंडार के साथ बाधा भंडार का प्रतिस्थापन है। यह प्रतिस्थापन उन विशिष्ट विधियों जैसे बाधा प्रचार द्वारा किया जाता है। बाधा तर्क प्रोग्रामिंग का शब्दार्थ न केवल उपयोग की जाने वाली बाधाओं के लिए पैरामीट्रिक है बल्कि बाधा भंडार को फिर से लिखने की विधि के लिए भी है। अभ्यास में उपयोग की जाने वाली विशिष्ट विधियां बाधा भंडार को हल करने में आसान होती हैं। यदि बाधा भंडार असंतोषजनक है तो यह सरलीकरण कभी-कभी इस असंतोष का पता लगा सकता है लेकिन हमेशा नहीं पता लगा सकता है।

लक्ष्य सिद्ध होने पर बाधा तर्क प्रोग्राम के विरुद्ध लक्ष्य का मूल्यांकन करने का परिणाम परिभाषित किया गया है। इस स्थिति में प्रारंभिक युग्म से एक युग्म के लिए व्युत्पत्ति सम्मिलित है जहां लक्ष्य रिक्त है। इस दूसरी युग्म के बाधा भंडार को मूल्यांकन का परिणाम माना जाता है। ऐसा इसलिए है क्योंकि बाधा भंडार में लक्ष्य को सिद्ध करने के लिए संतोषजनक माने जाने वाले सभी प्रतिबंध सम्मिलित हैं। दूसरे शब्दों में लक्ष्य उन सभी परिवर्तनीय मूल्यांकनों के लिए सिद्ध होता है जो इन बाधाओं को पूरा करते हैं।

दो शाब्दिक शब्दों की युग्म समानता को प्रायः द्वारा संक्षेप में निरूपित किया जाता है यह एक आशुलिपि है। लेकिन लक्ष्य की तुलना में बाधाओं के लिए बाधा तर्क प्रोग्रामिंग शब्दार्थ का एक सामान्य संस्करण सीधे बाधा भंडार में जोड़ता है।

नियम और शर्तें

शब्दों की विभिन्न परिभाषाओं का उपयोग किया जाता है। जिससे वास्तविक या परिमित डोमेन पर विभिन्न प्रकार की बाधा तर्क प्रोग्रामिंग उत्पन्न होती है। एक प्रकार की बाधा जो सदैव सम्मिलित रहती है वह शर्तों की समानता है। इस प्रकार की बाधाएं आवश्यक हैं क्योंकि अनुवादक t1=t2 को लक्ष्य में जोड़ता है जब भी एक शाब्दिक P(...t1...) को नए संस्करण के एल्गोरिदम के साथ परिवर्तित कर दिया जाता है जिसका क्रम P(...t2...) है।

रेखीय नियम

रेखीय नियमों के साथ बाधा तर्क प्रोग्रामिंग बाधा भंडार में बाधाओं के रूप में प्रतिस्थापन को संग्रहित करके नियमित तर्क प्रोग्रामिंग का अनुकरण करती है। शर्तें वेरिएबल स्थिरांक और फ़ंक्शन प्रतीक हैं जो अन्य शर्तों पर प्रयुक्त होते हैं। शर्तों के बीच समानता और असमानताओं पर विचार की जाने वाली एकमात्र बाधाएं हैं। समानता विशेष रूप से महत्वपूर्ण है, क्योंकिt1=t2 जैसे प्रतिबंध प्रायः अनुवादक द्वारा उत्पन्न किए जाते हैं। शर्तों पर समानता की बाधाओं को सरल बनाया जा सकता है। जिसे एकीकरण के माध्यम से हल किया जाता है।

एक बाधा t1=t2 को सरल बनाया जा सकता है यदि दोनों पद अन्य पदों पर प्रयुक्त फ़ंक्शन प्रतीक हैं। यदि दो फ़ंक्शन प्रतीक समान हैं और उपनियम की संख्या भी समान है तो इस बाधा को उपनियम की युग्म समानता से परिवर्तित जा सकता है। यदि शर्तें अलग-अलग फ़ंक्शन प्रतीकों या एक ही गुणक से बनी हैं लेकिन अलग-अलग शर्तों पर बाधा को असंतुष्ट करती है।

यदि दो पदों में से एक वेरिएबल है तो वेरिएबल का एकमात्र अनुमत मान दूसरा पद हो सकता है। जिसके परिणाम स्वरूप अन्य शब्द वेरिएबल को वर्तमान लक्ष्य और बाधा भंडार में परिवर्तित कर सकते हैं। इस प्रकार सामान्य रूप से वेरिएबल को विचार से हटा सकते हैं। स्वयं के साथ एक वेरिएबल की समानता की विशेष स्थिति में बाधा को सदैव संतुष्ट के रूप में हटाया जा सकता है। बाधा संतुष्टि के इस रूप में वेरिएबल मान पद हैं।

वास्तविक संख्याए

वास्तविक संख्या के साथ बाधा तर्क प्रोग्रामिंग शब्दों के रूप में वास्तविक भावों का उपयोग करती है। जब कोई फ़ंक्शन प्रतीकों का उपयोग नहीं किया जाता है तो शब्द संभवतः वेरिएबल सहित वास्तविक रूप से अभिव्यक्ति होते हैं। इस स्थिति में प्रत्येक वेरिएबल केवल एक वास्तविक संख्या को मान के रूप में ले सकता है। शुद्ध होने के लिए पद वेरिएबल और वास्तविक स्थिरांक पर व्यंजक हैं। शर्तों के बीच समानता एक प्रकार की बाधा है जो सदैव सम्मिलित रहती है क्योंकि अनुवादक निष्पादन के समय शर्तों की समानता उत्पन्न करता है। एक उदाहरण के रूप में यदि वर्तमान लक्ष्य का पहला अक्षर A(X+1) है और अनुवादक ने एक खंड चुना है जो A(Y-1):-Y=1 फिर से लिखने के बाद वेरिएबल हैं वर्तमान में बाधाओं को जोड़ा गया है जिसका लक्ष्य X+1=Y-1 और हैं। फ़ंक्शन प्रतीकों के लिए उपयोग किए जाने वाले सरलीकरण के नियम स्पष्ट रूप से उपयोग नहीं किए जाते हैं। X+1=Y-1 केवल इसलिए असंतोषजनक नहीं है क्योंकि पहली अभिव्यक्ति + का उपयोग करके बनाई गई है और दूसरी - का उपयोग करके बनाई गई है।

वास्तविक संख्याए और फ़ंक्शन प्रतीकों को जोड़ा जा सकता है। जो उन शर्तों के लिए अग्रणी होते हैं। जो वास्तविक और फ़ंक्शन प्रतीकों पर अन्य शर्तों पर प्रयुक्त होते हैं। औपचारिक रूप से, वेरिएबल और वास्तविक स्थिरांक भाव हैं अन्य अभिव्यक्तियों पर किसी भी अंकगणितीय संचालक के रूप में वेरिएबल स्थिरांक (शून्य एरिटी फ़ंक्शन प्रतीक) और भाव शब्द हैं। जैसा कि कोई भी फ़ंक्शन प्रतीक शर्तों पर प्रयुक्त होता है। दूसरे शब्दों में पद व्यंजकों पर निर्मित होते हैं जबकि व्यंजक संख्याओं और वेरिएबलों पर निर्मित होते हैं। इस स्थिति में वेरिएबल वास्तविक संख्या और शब्दों से अधिक होते हैं। दूसरे शब्दों में वेरिएबल एक वास्तविक संख्या को मान के रूप में ले सकता है जबकि दूसरा एक पद लेता है।

यदि दो शब्दों में से कोई भी वास्तविक अभिव्यक्ति नहीं है, तो दो शब्दों की समानता को वास्तविक शर्तों के नियमों का उपयोग करके सरल बनाया जा सकता है। उदाहरण के लिए यदि दो शब्दों में एक ही फ़ंक्शन प्रतीक और उपनियम की संख्या है तो उनकी समानता की बाधा को उपनियम की समानता से परिवर्तित किया जा सकता है।

परिमित डोमेन

बाधा तर्क प्रोग्रामिंग में प्रयुक्त बाधाओं की तीसरी श्रेणी परिमित डोमेन की है। वेरिएबल के मान इस स्थिति में एक परिमित डोमेन से लिए गए हैं, जो प्रायः पूर्णांक संख्याओं के होते हैं। प्रत्येक वेरिएबल के लिए एक अलग डोमेन X::[1..5]निर्दिष्ट किया जा सकता है उदाहरण के लिए इसका अर्थ यह है कि X के बीच है 1 और 5 है। एक वेरिएबल का डोमेन उन सभी मानों की गणना करके भी दिया जा सकता है जो एक वेरिएबल कर सकते हैं। इसलिए उपरोक्त डोमेन घोषणा को X::[1,2,3,4,5] भी लिखा जा सकता है। डोमेन निर्दिष्ट करने का यह दूसरा तरीका उन डोमेन के लिए स्वीकृति देता है जो पूर्णांकों से नहीं बने हैं। जैसे कि X::[george,mary,john] यदि एक वेरिएबल का डोमेन निर्दिष्ट नहीं है तो इसे भाषा में प्रतिनिधित्व करने योग्य पूर्णांकों का समूह[X,Y,Z]::[1..5] माना जाता है। जैसे घोषण पत्र का उपयोग करके वेरिएबल के समूह को एक ही डोमेन दिया जा सकता है।

निष्पादन के समय वेरिएबल के डोमेन को कम किया जा सकता है। वास्तव में जैसा कि अनुवादक बाधा संग्रह में बाधा डालता है यह स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार करता है और ये संचालित वेरिएबल के डोमेन को कम कर सकते हैं। यदि किसी वेरिएबल का डोमेन रिक्त हो जाता है तो बाधा भंडार असंगत होता है और एल्गोरिथम पीछे हट जाता है। यदि किसी वेरिएबल का डोमेन एकल डोमेन बन जाता है तो वेरिएबल को उसके डोमेन में अद्वितीय मान निर्दिष्ट किया जा सकता है। सामान्यतः प्रयुक्त की जाने वाली संगति के रूप आर्क संगति, हाइपर-आर्क संगति और बाध्य संगति हैं। एक वेरिएबल के वर्तमान डोमेन का विशिष्ट शाब्दिक उपयोग करके निरीक्षण किया जा सकता है। उदाहरण के लिए dom(X,D)) एक वेरिएबल D के वर्तमान डोमेन X की खोज करता है।

वास्तविक डोमेन के लिए प्रकार्यक का उपयोग पूर्णांक के डोमेन के साथ किया जा सकता है। इस स्थिति में एक पद पूर्णांकों पर व्यंजक हो सकता है या एक स्थिरांक हो सकता है या अन्य पदों पर एक प्रकार्यक का अनुप्रयोग हो सकता है। एक वेरिएबल अपेखाकृत शब्द मान के रूप में ले सकता है। यदि इसके डोमेन को पूर्णांक या स्थिरांक के रूप में निर्दिष्ट नहीं किया गया है।

बाधा भंडार

बाधा भंडार में वे बाधा भंडार होते हैं जिन्हें वर्तमान में संतोषजनक माना जाता है। यह माना जा सकता है कि नियमित तर्क प्रोग्रामिंग के लिए वर्तमान प्रतिस्थापन क्या है। जब केवल ट्री शर्तों की स्वीकृति होती है तो बाधा भंडार मेंt1=t2 के रूप में बाधा भंडार होते हैं इन बाधाओं को एकीकरण द्वारा सरल किया जाता है। जिसके परिणामस्वरूप variable=term के रूप में बाधा उत्पन्न होती है ऐसी बाधाएं एक प्रतिस्थापन के बराबर होती हैं।

हालाँकि, बाधा भंडार में t1!=t2 के रूप में भी बाधाएँ हो सकती हैं, यदि != के बीच की स्वीकृति है। जब वास्तविक या परिमित डोमेन पर बाधाओं की स्वीकृति दी जाती है तो बाधा भंडार में डोमेन विशिष्ट बाधाएँ जैसे X+2=Y/2भी हो सकती हैं।

बाधा भंडार वर्तमान प्रतिस्थापन की अवधारणा को दो प्रकार से विस्तारित करता है। सबसे पहले इसमें न केवल एक खंड के एक नए संस्करण के भाग के साथ एक शाब्दिक समानता से उत्पन्न बाधाएं सम्मिलित हैं बल्कि खंडों के एल्गोरिदम की बाधाएं भी सम्मिलित हैं। दूसरा इसमें न केवल variable=value के रूप मे बाधाएं होती हैं। मानक बाधा भाषा पर भी बाधाएं होती हैं। जबकि एक नियमित तर्क प्रोग्राम के सफल मूल्यांकन का परिणाम अंतिम प्रतिस्थापन है एक बाधा तर्क प्रोग्राम का परिणाम अंतिम बाधा भंडार है। जिसमें variable=value का रूप बाधा हो सकता है लेकिन सामान्य रूप से अपेक्षाकृत प्रतिबंध हो सकता है।

डोमेन-विशिष्ट बाधाएँ एल्गोरिदम से और मुख्य भाग के साथ एक शाब्दिक समानता से बाधा भंडार में आ सकती हैं। उदाहरण के लिए यदि अनुवादक शाब्दिक A(X+2) को एक बाधा के साथ फिर से लिखता है जिसका नया संस्कारण A(Y/2) है तब X+2=Y/2 को बाधा भंडार में जोड़ा जा सकता है। यदि एक वेरिएबल वास्तविक या परिमित डोमेन अभिव्यक्ति में प्रकट होता है, तो यह केवल वास्तविक या परिमित डोमेन में मान ले सकता है। इस प्रकार का एक वेरिएबल मान के रूप में अन्य शर्तों पर प्रयुक्त एक प्रकार्यक से बने शब्द को नहीं ले सकता है। बाधा भंडार असंतोषजनक है यदि एक वेरिएबल विशिष्ट डोमेन के मान और शर्तों पर प्रयुक्त प्रकार्यक दोनों को लेने के लिए बाध्य है।

बाधा भंडार में बाधा जोड़े जाने के बाद बाधा भंडार पर कुछ संचालन किए जाते हैं। कौन से संचालन किए जाते हैं यह माना जाने वाले डोमेन और बाधाओं पर निर्भर करता है। उदाहरण के लिए, एकीकरण का उपयोग परिमित ट्री समानता के लिए किया जाता है। वास्तविक से अधिक बहुपद समीकरणों के लिए वेरिएबल उन्मूलन, परिमित डोमेन के लिए स्थानीय स्थिरता के एक रूप को प्रयुक्त करने के लिए बाधा प्रसार इन परिचालनों का लक्ष्य संतोषप्रदता की जांच और समाधान के लिए बाधा भंडार को आसान बनाना है।

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

लेबलिंग

लेबलिंग लिटरल का उपयोग बाधा भंडार की संतुष्टि या आंशिक संतुष्टि की जांच करने और एक संतोषजनक असाइनमेंट खोजने के लिए परिमित डोमेन पर वेरिएबल पर किया जाता है। एक लेबलिंग शाब्दिक प्रपत्र labeling([variables]) का होता है, जहां तर्क परिमित डोमेन पर वेरिएबल की एक सूची है। जब भी अनुवादक इस प्रकार के शाब्दिक का मूल्यांकन करता है, तो यह सूची के वेरिएबल के डोमेन पर खोज करता है ताकि सभी प्रासंगिक बाधाओं को पूरा करने वाले असाइनमेंट को ढूंढा जा सके। आमतौर पर, यह बैकट्रैकिंग के एक रूप द्वारा किया जाता है: वेरिएबल का मूल्यांकन क्रम में किया जाता है, उनमें से प्रत्येक के लिए सभी संभावित मानों का प्रयास किया जाता है, और असंगतता का पता चलने पर बैकट्रैकिंग की जाती है।

लेबलिंग शाब्दिक का पहला उपयोग वास्तविक जांच संतुष्टि या बाधा भंडार की आंशिक संतुष्टि के लिए है। जब अनुवादक बाधा संग्रह में बाधा जोड़ता है, तो यह केवल उस पर स्थानीय स्थिरता का एक रूप प्रयुक्त करता है। यह ऑपरेशन असंगतता का पता नहीं लगा सकता है, भले ही बाधा भंडार असंतोषजनक हो। वेरिएबल के एक सेट पर शाब्दिक लेबलिंग इन चरों पर बाधाओं की संतुष्टि जांच को प्रयुक्त करता है। जिसके परिणाम स्वरूप, बाधा भंडार में उल्लिखित सभी वेरिएबल का उपयोग करने से भंडार की संतुष्टि की जांच होती है।

लेबलिंग शाब्दिक का दूसरा उपयोग वास्तव में उन चरों का मूल्यांकन निर्धारित करना है जो बाधा भंडार को संतुष्ट करते हैं। शाब्दिक लेबलिंग के बिना, वेरिएबल्स को केवल तभी मान दिया जाता है जब बाधा भंडार में X=value के रूप में एक बाधा होती है और जब स्थानीय संगति एक वेरिएबल के डोमेन को एक मान तक कम कर देती है। कुछ चरों पर शाब्दिक लेबलिंग इन चरों का मूल्यांकन करने के लिए बाध्य करता है। दूसरे शब्दों में, शाब्दिक लेबलिंग पर विचार करने के बाद, सभी चरों को एक मान निर्दिष्ट किया जाता है।

आम तौर पर, बाधा तर्क प्रोग्राम इस प्रकार से लिखे जाते हैं कि लेबलिंग अक्षर का मूल्यांकन बाधा भंडार में जितनी संभव हो उतनी बाधाओं के बाद ही किया जाता है। ऐसा इसलिए है क्योंकि शाब्दिक लेबलिंग खोज को प्रयुक्त करती है, और संतुष्ट होने के लिए अधिक बाधाएं होने पर खोज अधिक कुशल होती है। निम्नलिखित संरचना वाले बाधा तर्क प्रोग्राम द्वारा एक बाधा संतुष्टि समस्या को सामान्य रूप से हल किया जाता है:

solve(X):-constraints(X), labeling(X)
constraints(X):- (all constraints of the CSP)

जब अनुवादक लक्ष्य solve(args) का मूल्यांकन करता है, तो यह वर्तमान लक्ष्य में पहले खंड के नए संस्करण के एल्गोरिदम को रखता है। चूँकि पहला लक्ष्य constraints(X') है, दूसरे खंड का मूल्यांकन किया जाता है, और यह ऑपरेशन सभी बाधाओं को वर्तमान लक्ष्य में और अंततः बाधा भंडार में ले जाता है। इसके बाद लिटरल labeling(X') का मूल्यांकन किया जाता है, जिससे बाधा भंडार के समाधान की तलाश की जाती है। चूंकि बाधा भंडार में मूल कंस्ट्रेंट संतुष्टि समस्या के बिल्कुल कंस्ट्रेंट होते हैं, इसलिए यह ऑपरेशन मूल समस्या के समाधान की तलाश करता है।

प्रोग्राम सुधार

इसकी दक्षता में सुधार के लिए दिए गए बाधा तर्क प्रोग्राम को सुधारा जा सकता है। पहला नियम यह है कि लेबलिंग लिटरल को तब रखा जाना चाहिए जब लेबल लिटरल पर अधिक से अधिक प्रतिबंध बाधा भंडार में जमा हो जाएं। जबकि सिद्धांत में A(X):-labeling(X),X>0 के समतुल्य A(X):-X>0,labeling(X) है, वह खोज जो तब की जाती है जब अनुवादक लेबलिंग शाब्दिक का सामना करता है बाधा भंडार जिसमें बाधा X>0 नहीं है। परिणामस्वरूप, यह समाधान उत्पन्न कर सकता है, जैसे कि X=-1, जो बाद में इस बाधा को पूरा नहीं करने के लिए पाया गया। दूसरी ओर, दूसरे सूत्रीकरण में खोज तभी की जाती है जब बाधा पहले से ही बाधा भंडार में हो। जिसके परिणाम स्वरूप, खोज केवल उन समाधानों को लौटाती है जो इसके अनुरूप हैं, इस तथ्य का लाभ उठाते हुए कि अतिरिक्त बाधाएं खोज स्थान को कम करती हैं।

एक दूसरा सुधार जो दक्षता में वृद्धि कर सकता है, खंड के एल्गोरिदम में शाब्दिक से पहले बाधाओं को रखना है। दोबारा, A(X):-B(X),X>0 और A(X):-X>0,B(X) सिद्धांत रूप में समतुल्य हैं। हालाँकि, पहले को अधिक संगणना की आवश्यकता हो सकती है। उदाहरण के लिए, यदि बाधा भंडार में कंस्ट्रेंट X<-2 है, तो अनुवादक पहले मामले में B(X) का पुनरावर्ती मूल्यांकन करता है; यदि यह सफल होता है, तो यह पता चलता है कि X>0 जोड़ते समय बाधा भंडार असंगत है। दूसरे मामले में, उस क्लॉज का मूल्यांकन करते समय, अनुवादक पहले X>0 को बाधा भंडार में जोड़ता है और फिर संभवतः B(X) का मूल्यांकन करता है। चूंकि X>0 के अतिरिक्त होने के बाद बाधा भंडार असंगत हो जाता है, B(X) का पुनरावर्ती मूल्यांकन बिल्कुल नहीं किया जाता है।

एक तीसरा सुधार जो दक्षता बढ़ा सकता है, वह अनावश्यक बाधाओं को जोड़ना है। यदि प्रोग्रामर जानता है (किसी भी तरह से) कि किसी समस्या का समाधान एक विशिष्ट बाधा को संतुष्ट करता है, तो वे उस बाधा को जल्द से जल्द बाधा भंडार की असंगति पैदा करने के लिए सम्मिलित कर सकते हैं। उदाहरण के लिए, यदि यह पहले से ज्ञात है कि B(X) के मूल्यांकन के परिणामस्वरूप X के लिए धनात्मक मूल्य होगा, तो प्रोग्रामर B(X) की किसी भी घटना से पहले एक्स> 0 जोड़ सकता है। एक उदाहरण के रूप में,A(X,Y):-B(X),C(X) लक्ष्य A(-2,Z) पर विफल हो जाएगा, लेकिन यह केवल उपलक्ष्य B(X) के मूल्यांकन के समय पाया गया है। . दूसरी ओर, यदि उपरोक्त खंड को A(X,Y):-X>0,A(X),B(X) से बदल दिया जाता है, तो जैसे ही बाधा X>0 को बाधा में जोड़ा जाता है, अनुवादक पीछे हट जाता है। भंडार, जो B(X) के मूल्यांकन से पहले भी शुरू होता है।

बाधा से निपटने के नियम

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

A(X) <=> B(X) | C(X)
A(X) ==> B(X) | C(X)

पहला नियम बताता है कि, यदि B(X) भंडार द्वारा प्रवेश किया जाता है, तो बाधा A(X) को C(X) के रूप में फिर से लिखा जा सकता है। एक उदाहरण के रूप में,N*X>0 को X>0 के रूप में फिर से लिखा जा सकता है यदि भंडार का तात्पर्य N>0 से है। प्रतीक <=> तर्क में समानता जैसा दिखता है, और बताता है कि पहली बाधा बाद के बराबर है। व्यवहार में, इसका तात्पर्य है कि पहली बाधा को बाद वाले से परिवर्तित जा सकता है।

इसके अतिरिक्त दूसरा नियम निर्दिष्ट करता है कि बाद की बाधा पहले का परिणाम है, यदि बीच में बाधा बाधा भंडार से जुड़ी हुई है। जिसके परिणाम स्वरूप, यदि A(X) बाधा भंडार में है और B(X) बाधा भंडार से जुड़ा हुआ है, तो भंडार में C(X) जोड़ा जा सकता है। तुल्यता के मामले से अलग, यह एक जोड़ है और प्रतिस्थापन नहीं है: नया अवरोध जोड़ा जाता है लेकिन पुराना बना रहता है।

समानता कुछ बाधाओं को सरल लोगों के साथ बदलकर बाधा संग्रह को सरल बनाने की स्वीकृति देती है; विशेष रूप से, यदि एक तुल्यता नियम में तीसरी बाधा true है, और दूसरी बाधा सम्मिलित है, तो पहली बाधा बाधा संग्रह से हटा दी जाती है। अनुमान नई बाधाओं को जोड़ने की स्वीकृति देता है, जिससे बाधा भंडार की असंगतता सिद्ध हो सकती है, और आमतौर पर इसकी संतुष्टि को स्थापित करने के लिए आवश्यक खोज की मात्रा कम हो सकती है।

कंस्ट्रेंट हैंडलिंग नियमों के संयोजन में तार्किक प्रोग्रामिंग क्लॉज का उपयोग बाधा भंडार की संतुष्टि की स्थापना के लिए एक विधि निर्दिष्ट करने के लिए किया जा सकता है। विधि के विभिन्न विकल्पों को प्रयुक्त करने के लिए विभिन्न खंडों का उपयोग किया जाता है; निष्पादन के समय बाधा भंडार को फिर से लिखने के लिए बाधा प्रबंधन नियमों का उपयोग किया जाता है। एक उदाहरण के रूप में, इकाई प्रसार के साथ बैकट्रैकिंग को इस प्रकार प्रयुक्त किया जा सकता है। चलो holds(L) एक प्रस्तावक खंड का प्रतिनिधित्व करता है, जिसमें सूची L में अक्षर उसी क्रम में होते हैं जैसे उनका मूल्यांकन किया जाता है। एल्गोरिथम को सही या गलत के लिए शाब्दिक निर्दिष्ट करने के विकल्प के लिए क्लॉज का उपयोग करके प्रयुक्त किया जा सकता है, और प्रसार को निर्दिष्ट करने के लिए बाधाओं से निपटने के नियमों को प्रयुक्त किया जा सकता है। ये नियम निर्दिष्ट करते हैं कि holds([l|L]) को हटाया जा सकता है यदि भंडार से l=true होता है, और इसे holds(L) के रूप में फिर से लिखा जा सकता है यदि l=false भंडार से अनुसरण करता है। इसी तरह, holds([l]) को l=true से परिवर्तित जा सकता है। इस उदाहरण में, तर्क प्रोग्रामिंग के खंडों का उपयोग करके एक वेरिएबल के लिए मान का चुनाव कार्यान्वित किया जाता है; हालांकि, इसे डिसजंक्टिव कंस्ट्रेंट हैंडलिंग रूल्स या CHR∨ नामक एक्सटेंशन का उपयोग करके बाधा प्रबंधन नियमों में एन्कोड किया जा सकता है।

बॉटम-अप मूल्यांकन

तर्क प्रोग्रामों के मूल्यांकन की मानक रणनीति शीर्ष-नीचे और गहराई-प्रथम है: लक्ष्य से, कई खंडों की पहचान संभवतः लक्ष्य को सिद्ध करने में सक्षम होने के रूप में की जाती है, और उनके एल्गोरिदम के शाब्दिक पर पुनरावर्तन किया जाता है। तथ्यों से शुरू करना और नए तथ्यों को प्राप्त करने के लिए खंडों का उपयोग करना एक वैकल्पिक रणनीति है; इस रणनीति को बॉटम-अप कहा जाता है। इसे टॉप-डाउन से बेहतर माना जाता है जब उद्देश्य किसी एक लक्ष्य को सिद्ध करने के अतिरिक्त किसी दिए गए प्रोग्राम के सभी परिणामों का उत्पादन करना हो। विशेष रूप से, किसी प्रोग्राम के सभी परिणामों को मानक टॉप-डाउन और डेप्थ-फर्स्ट तरीके से खोजना समाप्त नहीं हो सकता है, जबकि बॉटम-अप मूल्यांकन रणनीति समाप्त हो जाती है।

नीचे से ऊपर की मूल्यांकन रणनीति मूल्यांकन के समय अब तक सिद्ध तथ्यों के सेट को बनाए रखती है। यह सेट प्रारंभ में खाली है। प्रत्येक चरण के साथ, सम्मिलित तथ्यों के लिए एक प्रोग्राम क्लॉज प्रयुक्त करके नए तथ्य निकाले जाते हैं, और सेट में जोड़े जाते हैं। उदाहरण के लिए, निम्नलिखित प्रोग्राम के नीचे के मूल्यांकन के लिए दो चरणों की आवश्यकता होती है:

A(q).
B(X):-A(X).

परिणामों का सेट प्रारंभ में खाली है। पहले चरण में, A(q) एकमात्र खंड है जिसका एल्गोरिदम सिद्ध किया जा सकता है (क्योंकि यह खाली है), और A(q) इसलिए परिणामों के वर्तमान सेट में जोड़ा जाता है। दूसरे चरण में, चूँकि A(q) सिद्ध हो चुका है, दूसरे खंड का उपयोग किया जा सकता है और परिणामों में B(q) जोड़ा जाता है। चूंकि {A(q),B(q)} से कोई अन्य परिणाम सिद्ध नहीं किया जा सकता है, निष्पादन समाप्त हो गया है।

ऊपर से नीचे के मूल्यांकन पर नीचे से ऊपर के मूल्यांकन का लाभ यह है कि व्युत्पत्तियों के चक्र एक अनंत लूप का उत्पादन नहीं करते हैं। ऐसा इसलिए है क्योंकि परिणामों के वर्तमान सेट में एक परिणाम जोड़ने से पहले से ही कोई प्रभाव नहीं पड़ता है। एक उदाहरण के रूप में, उपरोक्त प्रोग्राम में तीसरा खंड जोड़ने से शीर्ष-डाउन मूल्यांकन में व्युत्पत्तियों का एक चक्र उत्पन्न होता है:

A(q).
B(X):-A(X).
A(X):-B(X).

उदाहरण के लिए, लक्ष्य A(X) के सभी उत्तरों का मूल्यांकन करते समय, शीर्ष-डाउन रणनीति निम्नलिखित व्युत्पन्न उत्पन्न करेगी:

A(q)
A(q):-B(q), B(q):-A(q), A(q)
A(q):-B(q), B(q):-A(q), A(q):-B(q), B(q):-A(q), A(q)

दूसरे शब्दों में, एकमात्र परिणाम A(q) पहले उत्पन्न होता है, लेकिन फिर एल्गोरिथम उन व्युत्पत्तियों पर चक्र करता है जो किसी अन्य उत्तर का उत्पादन नहीं करते हैं। अधिक आम तौर पर, टॉप-डाउन मूल्यांकन रणनीति संभावित व्युत्पत्तियों पर चक्रित हो सकती है, संभवतः जब अन्य सम्मिलित हों।

बॉटम-अप रणनीति में वही खामी नहीं है, क्योंकि जो परिणाम पहले ही प्राप्त हो चुके हैं, उनका कोई प्रभाव नहीं पड़ता है। उपरोक्त प्रोग्राम पर, बॉटम-अप रणनीति परिणामों के सेट में A(q) को जोड़ना शुरू करती है; दूसरे चरण में,B(X):-A(X) का उपयोग B(q) को प्राप्त करने के लिए किया जाता है; तीसरे चरण में, वर्तमान परिणामों से प्राप्त होने वाले एकमात्र तथ्य A(q) और B(q) हैं, जो पहले से ही परिणामों के सेट में हैं। जिसके परिणाम स्वरूप, एल्गोरिथ्म बंद हो जाता है।

उपरोक्त उदाहरण में, केवल प्रयुक्त तथ्य ग्राउंड लिटरल थे। सामान्य तौर पर, प्रत्येक खंड जिसमें केवल एल्गोरिदम में बाधाएँ होती हैं, एक तथ्य माना जाता है। उदाहरण के लिए, एक खंड A(X):-X>0,X<10 तथ्य भी माना जाता है। तथ्यों की इस विस्तारित परिभाषा के लिए, कुछ तथ्य समतुल्य हो सकते हैं, जबकि वाक्यात्मक रूप से समान नहीं। उदाहरण के लिए, A(q) के बराबर है A(X):-X=q और दोनों के बराबर हैं A(X):-X=Y, Y=q. इस समस्या को हल करने के लिए, तथ्यों को सामान्य रूप में अनुवादित किया जाता है जिसमें सिर में सभी अलग-अलग चरों का एक टपल होता है; दो तथ्य तब समतुल्य होते हैं यदि उनके एल्गोरिदम सिर के वेरिएबल पर समतुल्य होते हैं, अर्थात, इन चरों तक सीमित होने पर उनके समाधान के सेट समान होते हैं।

जैसा कि वर्णन किया गया है, बॉटम-अप दृष्टिकोण में उन परिणामों पर विचार न करने का लाभ है जो पहले ही प्राप्त हो चुके हैं। हालाँकि, यह अभी भी उन परिणामों को प्राप्त कर सकता है जो उनमें से किसी के बराबर नहीं होने के बावजूद पहले से प्राप्त किए गए हैं। एक उदाहरण के रूप में, निम्न प्रोग्राम का नीचे से ऊपर का मूल्यांकन अनंत है:

A(0).
A(X):-X>0.
A(X):-X=Y+1, A(Y).

बॉटम-अप इवैल्यूएशन एल्गोरिद्म सबसे पहले यह निकालता है कि A(X) X=0 और X>0 के लिए सही है। दूसरे चरण में, तीसरे खंड के साथ पहला तथ्य A(1) की व्युत्पत्ति के लिए स्वीकृति देता है। तीसरे चरण में, A(2) व्युत्पन्न होता है, आदि। हालाँकि, ये तथ्य पहले से ही इस तथ्य से जुड़े हुए हैं कि A(X) किसी भी गैर-नकारात्मक X के लिए सत्य है। परिणामों के वर्तमान सेट में जोड़ा गया। यदि नया परिणाम सेट द्वारा पहले से ही उलझा हुआ है, तो उसे इसमें नहीं जोड़ा जाता है। चूंकि तथ्यों को खंड के रूप में संग्रहीत किया जाता है, संभवतः "स्थानीय चर" के साथ, उनके सिर के वेरिएबल पर प्रवेश प्रतिबंधित है।

समवर्ती बाधा तर्क प्रोग्रामिंग

बाधा तर्क प्रोग्रामिंग के समवर्ती संस्करणों का उद्देश्य बाधा संतुष्टि समस्याओं को हल करने के अतिरिक्त समवर्ती प्रक्रियाओं को प्रोग्रामिंग करना है। बाधा तर्क प्रोग्रामिंग में लक्ष्यों का मूल्यांकन समवर्ती रूप से किया जाता है; एक समवर्ती प्रक्रिया इसलिए अनुवादक द्वारा एक लक्ष्य के मूल्यांकन के रूप में क्रमादेशित है।

सांकेतिक रूप से, समवर्ती बाधाएँ तर्क प्रोग्राम गैर-समवर्ती प्रोग्रामों के समान हैं, एकमात्र अपवाद यह है कि खंड में गार्ड सम्मिलित हैं, जो ऐसी बाधाएँ हैं जो कुछ शर्तों के तहत खंड की प्रयोज्यता को अवरुद्ध कर सकती हैं। सिमेंटिक रूप से, समवर्ती बाधा तर्क प्रोग्रामिंग अपने गैर-समवर्ती संस्करणों से अलग है क्योंकि एक लक्ष्य मूल्यांकन का उद्देश्य किसी समस्या का समाधान खोजने के अतिरिक्त एक समवर्ती प्रक्रिया का एहसास करना है। विशेष रूप से, यह अंतर इस बात को प्रभावित करता है कि एक से अधिक खंड प्रयुक्त होने पर अनुवादक कैसे व्यवहार करता है: गैर-समवर्ती बाधा तर्क प्रोग्रामिंग पुनरावर्ती रूप से सभी खंडों का प्रयास करता है; समवर्ती बाधा तर्क प्रोग्रामिंग केवल एक को चुनती है। यह अनुवादक की एक इच्छित दिशात्मकता का सबसे स्पष्ट प्रभाव है, जो पहले से लिए गए किसी विकल्प को संशोधित नहीं करता है। इसके अन्य प्रभाव एक लक्ष्य होने की शब्दार्थिक संभावना है जिसे सिद्ध नहीं किया जा सकता है जबकि संपूर्ण मूल्यांकन विफल नहीं होता है, और एक लक्ष्य और एक खंड शीर्ष के बराबर होने का एक विशेष तरीका है।

अनुप्रयोग

बाधा तर्क प्रोग्रामिंग को कई क्षेत्रों में प्रयुक्त किया गया है, जैसे कि स्वचालित योजना और शेड्यूलिंग,[1] अनुमान टाइप,[2] सिविल इंजीनियरिंग, मैकेनिकल इंजीनियरिंग, डिजिटल परिपथ सत्यापन, हवाई यातायात नियंत्रण, वित्त, और अन्य।[citation needed]

इतिहास

1987 में जफ़र और लासेज़ द्वारा कांस्ट्रेंट तार्किक प्रोग्रामिंग की शुरुआत की गई थी।[3] उन्होंने इस अवलोकन को सामान्यीकृत किया कि शब्द समीकरण और प्रोलॉग II की विषमताएं बाधाओं का एक विशिष्ट रूप थीं, और इस विचार को मनमाना बाधा भाषाओं के लिए सामान्यीकृत किया। इस अवधारणा का पहला कार्यान्वयन प्रोलॉग III, सीएलपी (आर) और सीएचआईपी था।[citation needed]

यह भी देखें

संदर्भ

  • Dechter, Rina (2003). Constraint processing. Morgan Kaufmann. ISBN 1-55860-890-7. ISBN 1-55860-890-7
  • Apt, Krzysztof (2003). Principles of constraint programming. Cambridge University Press. ISBN 0-521-82583-0. ISBN 0-521-82583-0
  • Marriott, Kim; Peter J. Stuckey (1998). Programming with constraints: An introduction. MIT Press. ISBN 0-262-13341-5
  • Frühwirth, Thom; Slim Abdennadher (2003). Essentials of constraint programming. Springer. ISBN 3-540-67623-6. ISBN 3-540-67623-6
  • Jaffar, Joxan; Michael J. Maher (1994). "Constraint logic programming: a survey". Journal of Logic Programming. 19/20: 503–581. doi:10.1016/0743-1066(94)90033-7.
  • Colmerauer, Alain (1987). "Opening the Prolog III Universe". Byte. August.


संदर्भ

  1. Abdennadher, Slim, and Hans Schlenker. "Nurse scheduling using constraint logic programming." AAAI/IAAI. 1999.
  2. Michaylov, Spiro, and Frank Pfenning. "Higher-Order Logic Programming as Constraint Logic Programming." PPCP. Vol. 93. 1993.
  3. Jaffar, Joxan, and J-L. Lassez. "Constraint logic programming." Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. ACM, 1987.