6.1.1. העברת הפסוקים לצורת CNF - הרעיון
בגדול: ביטוי מצורת CNF זהו
ביטוי מהצורה:
![plot:\[\begin{gathered}
\left( {{L_{11}} \vee {L_{12}} \vee
...{L_{1{n_1}}}} \right) \wedge \hfill \\
... \hfill \\
\left( {{L_{m1}} \vee {L_{m2}} \vee
...{L_{m{n_m}}}} \right) \hfill \\
\end{gathered} \]](/documentResources/208/plot_212.png)
כאשר
הוא פסוק אטומי או שלילת פסוק אטומי.
כל אחת מהשורות הנ"ל נקראת פסוקית
(clause).
לנוסחה הנ"ל מתייחסים כקבוצת
פסוקיות. לכל פסוקית מתייחסים כקבוצת ליטרלים:
![plot:\[\left\{
{\left\{ {{L_{11}},{L_{12}},...,{L_{1{n_1}}}} \right\},...,\left\{
{{L_{m1}},{L_{m2}},...,{L_{m{n_m}}}} \right\}} \right\}\]](/documentResources/208/plot_213.png)
קיים אלגוריתם להמרת כל נוסחה לנוסחה
מצורת CNF.
אבל הוא עדיין לא נפתח...