DNF

Disjunctive Normal Form או הצורה הנורמלית הדיסיונקטיבית - הוא ביטוי המורכב מאוסף פרדיקטים לוגיים המחוברים ביניהם על ידי ביטויי "או" כאשר כל פרדיקט הוא אוסף של ביטויים המחוברים ביניהם על ידי ביטויי "וגם". השימושית מתבטאת בכך שניתן להביא כל ביטוי לוגי לצורת DNF.

ניסוח מילולי

ביטוי מצורת DNF מורכב מאוסף "פסוקיות" המחוברות ביניהן על ידי פעולות "או", כאשר כל פסוקית היא אוסף של ליטרלים (משתנים ושלילות משתנים) המחוברים ביניהם על ידי פעולות "וגם".

העברת נוסחה לצורת DNF

כל נוסחה בתחשיב הפסוקים ניתנת להצגה כנוסחת DNF כך:

1. מציאת כל השמות ערכי האמת המספקות את הנוסחה - בדרך כלל בעזרת טבלת אמת.
2. עבור כל השמה כזו, בניית פסוקית אשר מכילה את כל המשתנים שערכם "אמת", ואת שלילת כל המשתנים המקבלים ערך "שקר"(בהם פעולות "וגם")

דוגמאות

הנוסחאות הבאות במשתנים <math>\ x_1, \ldots, x_n</math> הן בצורת DNF:

<math>x_1 \land x_2</math>

<math>x_1\!</math>

<math>(x_1 \land x_2) \lor x_3</math>

<math>(x_1 \land \neg x_2 \land \neg x_3) \lor (\neg x_4 \land x_5 \land x_6)</math>

ספיקות נוסחה בצורת DNF

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

אלגוריתם לבדיקת הספיקות

תהי <math>\varphi</math> נוסחה בצורת DNF ויהי A אלגוריתם המכריע אם <math>\varphi</math> ספיקה. האלגוריתם יבצע:

1. בדוק אם <math>\varphi</math> היא אכן בצורת DNF (בדיקת תקינות קלט).
2. לכל פסוקית <math>\ C_1, ..., C_m</math> בדוק:
   1. אם הפסוקית אינה מכילה סתירה מהצורה של <math>x_1 \land \neg x_1</math> החזר כי קיימת השמה מספקת.
3. החזר כי לא קיימת השמה מספקת.

בהינתן <math>n</math> משתנים ו-<math>m</math> פסוקיות, זמן ריצת האלגוריתם הוא <math>O(m \times n)</math>.

ראו גם

• CNF (צורה נורמלית קוניוקטיבית)

קישורים חיצוניים

• DNF, באתר MathWorld (באנגלית)