הצגת המקור של הדף "CNF"

'''Conjunctive Normal Form''' או '''הצורה הנורמלית הקוניוקטיבית''' הוא ביטוי המורכב מאוסף "פסוקיות" המחוברות ביניהן על ידי [[קוניונקציה]], כלומר, פעולות [[וגם (לוגיקה)|וגם]]. כל פסוקית היא אוסף של ליטרלים (משתנים ושלילות משתנים) המחוברים ביניהם על ידי פעולות [[או (לוגיקה)|או]] (דיסיונקציה).

'''דוגמה''':

נוסחת CNF במשתנים <math>\ x_1, \ldots, x_n</math> בעלת צורה כגון
<math display="block">(x_1\lor \overline{x_3})\land(x_2)\land(x_2\lor x_5 \lor \overline{x_6} \lor x_n)</math>

== העברת נוסחה לצורת CNF ==
כל נוסחה ב[[תחשיב פסוקים|תחשיב הפסוקים]] ניתנת להצגה כנוסחת CNF כך:
# מציאת כל השמות ערכי האמת שאינן מספקות את הנוסחה.
# עבור כל השמה כזו, בניית פסוקית אשר מכילה את כל המשתנים שערכם "שקר", ואת שלילת כל המשתנים המקבלים שערכם "אמת", וביניהם פעולות "או". 
# הנוסחה הרצויה היא קוניונקציה של כל הפסוקיות שנמצאו.

== ספיקות נוסחה בצורת CNF ==
{{ערך מורחב|בעיית הספיקות}}

בהינתן נוסחה בצורת CNF המורכבת מהפסוקיות <math>\ C_1, ..., C_m</math>, ניתן לשאול האם קיימת השמת ערכי אמת המספקת אותה. מתברר שבעיה זו (המכונה [[בעיית הספיקות בתחשיב הפסוקים]]) היא [[NP-שלמה]], ולכן נראה שלא ניתן לענות עליה באופן אוטומטי בזמן סביר (פולינומי ביחס לגודל הקלט במקום אלגוריתם מעריכי שיש כיום לפתרון בעיות כאלה).

== ראו גם ==
* [[DNF]] (צורה נורמלית דיסיונקטיבית)


[[קטגוריה:ערכים שבהם תבנית בריטניקה אינה מתאימה]]
[[קטגוריה:אלגברה בוליאנית]]