DNF

Disjunctive Normal Form (DNF) או הצורה הנורמלית הדיסיונקטיבית היא ביטוי לוגי שמורכב מפסוקיות המחוברות ב'או'.

בפי DNF כל ביטוי מחולק לפסוקיות (clauses). כל פסוקית היא אוסף ליטרלים (literal, משתנה או שלילה של משתנה) המחוברים ביניהם על ידי 'וגם' (AND).

כל נוסחה בתחשיב הפסוקים ניתנת לייצוג כ-DNF. שיטה נפוצה היא להשתמש בטבלת אמת: למצוא את כל השמת ערכי האמת שעושות את הנוסחה לאמת. עבור כל השמה כזו בונים פסוקית שמכילה את המשתנים ששווים אמת ואת השלילות של המשתנים ששווים שקר. חיבור ה'או' של כל הפסוקיות האלו נותן את הנוסחה ב‑DNF.

דוגמאות פשוטות בצורת DNF: x1 ∧ x2 ; x1 ; (x1 ∧ x2) ∨ x3. דוגמה ארוכה יותר: (x1 ∧ ¬x2 ∧ ¬x3) ∨ (¬x4 ∧ x5 ∧ x6).

שאלה מרכזית היא האם קיימת השמת ערכים שהופכת את הנוסחה לאמת (ספיקות). בניגוד למקרים כלליים בתחשיב הפסוקים, עבור נוסחאות ב‑DNF אפשר לקבוע זאת ביעילות פולינומית.

ניתן לבדוק ספיקות על ידי בדיקה פשוטה של כל פסוקית: אם פסוקית אינה מכילה סתירה פנימית מסוג x ו‑¬x, אז היא ניתנת להשמה מספקת, ומכך הנוסחה כולה ספיקה. בבדיקה על m פסוקיות עם n משתנים זמן הריצה הוא מהסדר O(m×n).

DNF או הצורה הנורמלית הדיסיונקטיבית היא דרך לכתוב ביטויים לוגיים. ביטוי כזה הוא רשימה של חלקים שמחוברים ב'או'.

כל חלק נקרא פסוקית. פסוקית היא קבוצת ליטרלים. ליטרל הוא משתנה (סימן שיכול להיות אמת או שקר) או שלילה שלו.

כדי להכניס נוסחה ל‑DNF מוצאים את כל השיפוצים של המשתנים שהופכים את הנוסחה לאמת. לכל השמה כזו בונים פסוקית: כותבים את המשתנים שאמיתיים ואת השלילות של אלה ששקריים. ואז מחברים את כל הפסוקיות ב'או'.

x1 ∧ x2 הוא DNF. גם (x1 ∧ x2) ∨ x3 הוא DNF.

כדי לבדוק אם נוסחה ב‑DNF יכולה להיות אמת, בודקים כל פסוקית. אם יש פסוקית בלי סתירה פנימית כמו x ו‑¬x, אז אפשר לבחור השמה והנוסחה תהיה אמת. אפשר לבצע את הבדיקה במהירות יחסית לפי מספר הפסוקיות ומספר המשתנים.