CNF

CNF היא דרך לכתוב נוסחאות לוגיות. הנוסחה מורכבת מפסוקיות שמחוברות ב'ו'. קוניונקציה זה 'ו'. כל פסוקית היא קבוצה של ליטרלים. ליטרל הוא משתנה או לא שלו. בתוך הפסוקית משתמשים ב'או'. דיסיונקציה זה 'או'. לדוגמה: (x1 או לא x3) ו-(x2) ו-(x2 או x5 או לא x6 או xn). כדי להעביר נוסחה ל-CNF אפשר למצוא את כ...