संयोजक सामान्य रूप

Not to be confused with Chomsky normal form.

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

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

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

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

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

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

उदाहरण और गैर-उदाहरण

निम्नलिखित सभी सूत्र चर में हैं $A,B,C,D,E$, और $F$ संयोजक सामान्य रूप में हैं:

• $(A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)$
• $(A\lor B)\land (C)$
• $(A\lor B)$
• $(A)$

स्पष्टता के लिए, विभक्ति उपवाक्य ऊपर कोष्ठक के अंदर लिखे गए हैं। कोष्ठक में रखे गए संयोजक उपवाक्यों के साथ विच्छेदात्मक सामान्य रूप में, अंतिम मामला वही है, लेकिन अंतिम से अगला है $(A)\lor (B)$. स्थिरांक सत्य और असत्य को खाली संयुक्ताक्षर और खाली विच्छेद से युक्त एक खंड द्वारा दर्शाया जाता है, लेकिन आम तौर पर स्पष्ट रूप से लिखा जाता है। निम्नलिखित सूत्र संयोजक सामान्य रूप में नहीं हैं:

• $\neg (B\lor C)$, क्योंकि एक OR एक NOT के भीतर निहित है
• $(A\land B)\lor C$
• $A\land (B\lor (D\land E))$, चूँकि AND एक OR के भीतर निहित है

प्रत्येक सूत्र को संयोजक सामान्य रूप में एक सूत्र के रूप में समान रूप से लिखा जा सकता है। सीएनएफ में तीन गैर-उदाहरण हैं:

• $(\neg B)\land (\neg C)$
• $(A\lor C)\land (B\lor C)$
• $(A)\land (B\lor D)\land (B\lor E).$

सीएनएफ में रूपांतरण

प्रत्येक प्रस्तावात्मक सूत्र को तार्किक तुल्यता सूत्र में परिवर्तित किया जा सकता है जो सीएनएफ में है। यह परिवर्तन तार्किक तुल्यता के नियमों पर आधारित है: दोहरा निषेध उन्मूलन, डी मॉर्गन के नियम और वितरणात्मक कानून।

चूंकि सभी प्रस्तावक सूत्रों को संयोजक सामान्य रूप में समकक्ष सूत्र में परिवर्तित किया जा सकता है, इसलिए प्रमाण अक्सर इस धारणा पर आधारित होते हैं कि सभी सूत्र सीएनएफ हैं। हालाँकि, कुछ मामलों में सीएनएफ में यह रूपांतरण सूत्र के तेजी से विस्फोट का कारण बन सकता है। उदाहरण के लिए, निम्नलिखित गैर-सीएनएफ सूत्र को सीएनएफ में अनुवाद करने से एक सूत्र तैयार होता है $2^{n}$ खंड:

$(X_{1}\wedge Y_{1})\vee (X_{2}\wedge Y_{2})\vee \dots \vee (X_{n}\wedge Y_{n}).$

विशेष रूप से, उत्पन्न सूत्र है:

$(X_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee X_{2}\vee \cdots \vee X_{n})\wedge (X_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge (Y_{1}\vee Y_{2}\vee \cdots \vee X_{n})\wedge \cdots \wedge (Y_{1}\vee Y_{2}\vee \cdots \vee Y_{n}).$

इस सूत्र में शामिल है $2^{n}$ खंड; प्रत्येक खंड में या तो शामिल है $X_{i}$ या $Y_{i}$ प्रत्येक के लिए $i$.

सीएनएफ में ऐसे परिवर्तन मौजूद हैं जो तार्किक तुल्यता के बजाय बूलियन संतुष्टि समस्या को संरक्षित करके आकार में तेजी से वृद्धि से बचते हैं। ये परिवर्तन केवल सूत्र के आकार को रैखिक रूप से बढ़ाने की गारंटी देते हैं, लेकिन नए चर पेश करते हैं। उदाहरण के लिए, उपरोक्त सूत्र को वेरिएबल जोड़कर सीएनएफ में बदला जा सकता है $Z_{1},\ldots ,Z_{n}$ निम्नलिखित नुसार:

$(Z_{1}\vee \cdots \vee Z_{n})\wedge (\neg Z_{1}\vee X_{1})\wedge (\neg Z_{1}\vee Y_{1})\wedge \cdots \wedge (\neg Z_{n}\vee X_{n})\wedge (\neg Z_{n}\vee Y_{n}).$

एक व्याख्या (तर्क) इस सूत्र को तभी संतुष्ट करती है जब कम से कम एक नया चर सत्य हो। यदि यह वेरिएबल है $Z_{i}$, फिर दोनों $X_{i}$ और $Y_{i}$ सच भी हैं. इसका मतलब यह है कि प्रत्येक मॉडल सिद्धांत जो इस सूत्र को संतुष्ट करता है वह मूल सिद्धांत को भी संतुष्ट करता है। दूसरी ओर, मूल सूत्र के केवल कुछ मॉडल ही इसे संतुष्ट करते हैं: चूंकि $Z_{i}$ मूल सूत्र में उल्लिखित नहीं हैं, उनके मूल्य इसकी संतुष्टि के लिए अप्रासंगिक हैं, जो कि अंतिम सूत्र में मामला नहीं है। इसका मतलब यह है कि मूल सूत्र और अनुवाद का परिणाम समतुल्यता है लेकिन तार्किक समतुल्यता नहीं है।

एक वैकल्पिक अनुवाद, त्सेइटिन परिवर्तन में खंड भी शामिल हैं $Z_{i}\vee \neg X_{i}\vee \neg Y_{i}$. इन उपवाक्यों से सूत्र का तात्पर्य है $Z_{i}\equiv X_{i}\wedge Y_{i}$; इस सूत्र को अक्सर परिभाषित करने के लिए माना जाता है $Z_{i}$ के लिए एक नाम होना $X_{i}\wedge Y_{i}$.

प्रथम-क्रम तर्क

पहले क्रम के तर्क में, तार्किक सूत्र के उपवाक्य सामान्य रूप को प्राप्त करने के लिए संयोजक सामान्य रूप को आगे ले जाया जा सकता है, जिसका उपयोग प्रथम-क्रम तर्क में संकल्प (तर्क)#रिज़ॉल्यूशन करने के लिए किया जा सकता है|प्रथम-क्रम संकल्प। रिज़ॉल्यूशन-आधारित स्वचालित प्रमेय-सिद्ध करने में, एक CNF सूत्र

$($

$l_{11}$

$\lor$

$\ldots$

$\lor$

$l_{1n_{1}}$

$)$

$\land$

$\ldots$

$\land$

$($

$l_{m1}$

$\lor$

$\ldots$

$\lor$

$l_{mn_{m}}$

$)$

, with $l_{ij}$ literals, is commonly represented as a set of sets

$\{$

$\{$

$l_{11}$

$,$

$\ldots$

$,$

$l_{1n_{1}}$

$\}$

$,$

$\ldots$

$,$

$\{$

$l_{m1}$

$,$

$\ldots$

$,$

$l_{mn_{m}}$

$\}$

$\}$

.

उदाहरण के लिए #कन्वर्टिंग_फ्रॉम_फर्स्ट-ऑर्डर_लॉजिक देखें।

कम्प्यूटेशनल जटिलता

कम्प्यूटेशनल जटिलता सिद्धांत में समस्याओं के एक महत्वपूर्ण सेट में संयोजक सामान्य रूप में व्यक्त बूलियन सूत्र के चर के लिए असाइनमेंट ढूंढना शामिल है, जैसे कि सूत्र सत्य है। K-SAT समस्या CNF में व्यक्त बूलियन सूत्र के लिए एक संतोषजनक असाइनमेंट खोजने की समस्या है जिसमें प्रत्येक वियोजन में अधिकतम k चर होते हैं। बूलियन संतुष्टि समस्या|3-SAT एनपी-पूर्ण है (k>2 के साथ किसी भी अन्य k-SAT समस्या की तरह) जबकि 2-संतोषजनकता|2-SAT को बहुपद समय में समाधान के लिए जाना जाता है। एक परिणाम के रूप में, संतुष्टि को बनाए रखते हुए किसी सूत्र को डिसजंक्टिव सामान्य रूप में परिवर्तित करने का कार्य एनपी कठिन है; बूलियन बीजगणित#द्वैत सिद्धांत, सीएनएफ में परिवर्तित करना, संतुष्टि और वैधता को संरक्षित करना, एनपी-हार्ड भी है; इसलिए डीएनएफ या सीएनएफ में समतुल्य-संरक्षण रूपांतरण फिर से एनपी-हार्ड है।

इस मामले में विशिष्ट समस्याओं में 3CNF में सूत्र शामिल होते हैं: संयोजक सामान्य रूप जिसमें प्रति संयोजन तीन से अधिक चर नहीं होते हैं। व्यवहार में आने वाले ऐसे सूत्रों के उदाहरण बहुत बड़े हो सकते हैं, उदाहरण के लिए 100,000 चर और 1,000,000 संयोजन के साथ।

CNF में एक सूत्र को प्रत्येक संयोजन को k से अधिक चर के साथ प्रतिस्थापित करके kCNF (k≥3 के लिए) में एक समतुल्य सूत्र में परिवर्तित किया जा सकता है। $X_{1}\vee \cdots \vee X_{k}\vee \cdots \vee X_{n}$ दो संयोजकों द्वारा $X_{1}\vee \cdots \vee X_{k-1}\vee Z$ और $\neg Z\vee X_{k}\cdots \vee X_{n}$ साथ Z एक नया चर, और जितनी बार आवश्यक हो दोहराना।

प्रथम-क्रम तर्क से परिवर्तित करना

प्रथम-क्रम तर्क को CNF में बदलने के लिए:

1. निषेध को सामान्य रूप में बदलें।
   1. निहितार्थ और तुल्यताएँ हटाएँ: बार-बार बदलें $P\rightarrow Q$ साथ $\lnot P\lor Q$; बदलना $P\leftrightarrow Q$ साथ $(P\lor \lnot Q)\land (\lnot P\lor Q)$. अंततः, यह की सभी घटनाओं को समाप्त कर देगा $\rightarrow$ और $\leftrightarrow$.
   2. डी मॉर्गन के नियम|डी मॉर्गन के नियम को बार-बार लागू करके नोट को अंदर की ओर ले जाएं। विशेष रूप से, प्रतिस्थापित करें $\lnot (P\lor Q)$ साथ $(\lnot P)\land (\lnot Q)$; बदलना $\lnot (P\land Q)$ साथ $(\lnot P)\lor (\lnot Q)$; और बदलें $\lnot \lnot P$ साथ $P$; बदलना $\lnot (\forall xP(x))$ साथ $\exists x\lnot P(x)$; $\lnot (\exists xP(x))$ साथ $\forall x\lnot P(x)$. उसके बाद, ए $\lnot$ विधेय चिह्न के ठीक पहले ही घटित हो सकता है।
2. वेरिएबल का मानकीकरण करें
   1. जैसे वाक्यों के लिए $(\forall xP(x))\lor (\exists xQ(x))$ जो एक ही वेरिएबल नाम का दो बार उपयोग करते हैं, उनमें से एक वेरिएबल का नाम बदल देते हैं। इससे बाद में क्वांटिफायर छोड़ते समय भ्रम की स्थिति से बचा जा सकता है। उदाहरण के लिए, $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists y\mathrm {Loves} (y,x)]$ का नाम बदल दिया गया है $\forall x[\exists y\mathrm {Animal} (y)\land \lnot \mathrm {Loves} (x,y)]\lor [\exists z\mathrm {Loves} (z,x)]$.
3. स्कोलेम सामान्य कथन है
   1. क्वांटिफायर को बाहर की ओर ले जाएं: बार-बार बदलें $P\land (\forall xQ(x))$ साथ $\forall x(P\land Q(x))$; बदलना $P\lor (\forall xQ(x))$ साथ $\forall x(P\lor Q(x))$; बदलना $P\land (\exists xQ(x))$ साथ $\exists x(P\land Q(x))$; बदलना $P\lor (\exists xQ(x))$ साथ $\exists x(P\lor Q(x))$. ये प्रतिस्थापन समतुल्यता को संरक्षित करते हैं, क्योंकि पिछले परिवर्तनीय मानकीकरण चरण ने यह सुनिश्चित किया था $x$ में नहीं होता है $P$. इन प्रतिस्थापनों के बाद, एक क्वांटिफ़ायर केवल सूत्र के प्रारंभिक उपसर्ग में हो सकता है, लेकिन कभी भी a के अंदर नहीं $\lnot$, $\land$, या $\lor$.
   2. बार-बार बदलना $\forall x_{1}\ldots \forall x_{n}\;\exists y\;P(y)$ साथ $\forall x_{1}\ldots \forall x_{n}\;P(f(x_{1},\ldots ,x_{n}))$, कहाँ $f$ एक नया है $n$-एरी फ़ंक्शन प्रतीक, एक तथाकथित स्कोलेम सामान्य रूप। यह एकमात्र कदम है जो समतुल्यता के बजाय केवल संतुष्टि को बरकरार रखता है। यह सभी अस्तित्व संबंधी परिमाणकों को समाप्त कर देता है।
4. सभी सार्वभौमिक परिमाणकों को हटा दें।
5. ANDs के ऊपर ORs को अंदर वितरित करें: बार-बार बदलें $P\lor (Q\land R)$ साथ $(P\lor Q)\land (P\lor R)$.

एक उदाहरण के रूप में, सूत्र कहता है कि जो कोई भी सभी जानवरों से प्यार करता है, उसे बदले में कोई और भी प्यार करता है, उसे सीएनएफ (और बाद में अंतिम पंक्ति में खंड (तर्क) रूप में) में परिवर्तित किया जाता है (प्रतिस्थापन नियम रिडेक्स को हाइलाइट करना) ${\color {red}{\text{red}}}$):

$\forall x$

$($

$\forall y$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\rightarrow$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

$\forall x$

$($

$\forall y$

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\rightarrow$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.1

$\forall x$

$\color {red}\lnot$

$($

${\color {red}{\forall y}}$

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.1

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$($

$\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\color {red}\lor$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

$\exists y$

$\color {red}\lnot$

$\color {red}\lnot$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\exists$

$y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$($

$\color {red}\exists$

$\color {red}y$

$\mathrm {Loves} ($

$y$

$,x)$

$)$

by 1.2

$\forall x$

$($

$\exists y$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$($

$\color {red}\exists$

$\color {red}z$

$\mathrm {Loves} ($

$z$

$,x)$

$)$

by 2

$\forall x$

$\exists z$

$($

${\color {red}{\exists y}}$

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$z$

$,x)$

by 3.1

$\forall x$

${\color {red}{\exists z}}$

$\exists y$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$z$

$,x)$

by 3.1

$\forall x$

${\color {red}{\exists y}}$

$($

$\mathrm {Animal} ($

$y$

$)$

$\land$

$\lnot$

$\mathrm {Loves} (x,$

$y$

$)$

$)$

$\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

by 3.2

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\land$

$\lnot$

$\mathrm {Loves} (x,$

$f(x)$

$)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

by 4

$($

$\mathrm {Animal} ($

$f(x)$

$)$

$\color {red}\lor$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$)$

$\color {red}\land$

$($

$\lnot \mathrm {Loves} (x,f(x))$

$\color {red}\lor$

$\mathrm {Loves} (g(x),x)$

$)$

by 5

$\{$

$\{$

$\mathrm {Animal} ($

$f(x)$

$)$

$,$

$\mathrm {Loves} ($

$g(x)$

$,x)$

$\}$

$,$

$\{$

$\lnot \mathrm {Loves} (x,f(x))$

$,$

$\mathrm {Loves} (g(x),x)$

$\}$

$\}$

(clause representation)

अनौपचारिक रूप से, स्कोलेम फ़ंक्शन $g(x)$ जिसके द्वारा उस व्यक्ति को उपज देने के रूप में सोचा जा सकता है $x$ प्यार किया जाता है, जबकि $f(x)$ पशु को (यदि कोई हो तो) वही प्राप्त होता है $x$ प्यार नहीं करता. नीचे से तीसरी अंतिम पंक्ति इस प्रकार है$x$ जानवर से प्यार नहीं करता $f(x)$, वरना $x$ से प्यार किया जाता है $g(x)$.

ऊपर से दूसरी अंतिम पंक्ति, $(\mathrm {Animal} (f(x))\lor \mathrm {Loves} (g(x),x))\land (\lnot \mathrm {Loves} (x,f(x))\lor \mathrm {Loves} (g(x),x))$, सीएनएफ है।

यह भी देखें

• बीजगणितीय सामान्य रूप
• विच्छेदनात्मक सामान्य रूप
• हॉर्न उपवाक्य
• क्वीन-मैक्लुस्की एल्गोरिथम

संदर्भ

• J. Eldon Whitesitt (24 May 2012). Boolean Algebra and Its Applications. Courier Corporation. ISBN 978-0-486-15816-7.
• Hans Kleine Büning; Theodor Lettmann (28 August 1999). Propositional Logic: Deduction and Algorithms. Cambridge University Press. ISBN 978-0-521-63017-7.
• Paul Jackson, Daniel Sheridan: Clause Form Conversions for Boolean Circuits. In: Holger H. Hoos, David G. Mitchell (Eds.): Theory and Applications of Satisfiability Testing, 7th International Conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3542, Springer 2005, pp. 183–198
• G.S. Tseitin: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian), pp. 115–125. Steklov Mathematical Institute (1968)

बाहरी संबंध

• "Conjunctive normal form", Encyclopedia of Mathematics, EMS Press, 2001 [1994]
• Java tool for converting a truth table into CNF and DNF
• Java applet for converting to CNF and DNF, showing laws used