Да, для метода резолюций обязательно делать СКНФ. 2

СКНФ формулы можно получить либо из таблицы истинности, используя закон двойственности, либо с помощью равносильных преобразований. 1

Алгоритм получения СКНФ с помощью равносильных преобразований: 1

1. Получить любую КНФ формулы. 1
2. Если в КНФ формулы имеется элементарная дизъюнкция D, не содержащая xi, её заменить на D Ú xi & xi. 1
3. Если в КНФ формулы имеется две одинаковых элементарных дизъюнкции D, то одну из них отбросить. 1
4. Если в некоторую элементарную дизъюнкцию D в КНФ формулы переменная xi входит дважды, то одну из них отбросить. 1
5. Если некоторая элементарная дизъюнкция D в КНФ формулы содержит высказывание вида xi Ú xi, то эту элементарную дизъюнкцию отбросить. 1

Также СКНФ можно построить по таблице истинности: 4

1. Выделить в таблице истинности все строки, в которых функция принимает значения 0. 4
2. Для каждого выбранного набора записать элементарные дизъюнкции, содержащие переменные: если значение переменной равно 0, то записывается сама переменная, если значение переменной равно 1, то записывается инверсия этой переменной. 4
3. Соединить элементарные дизъюнкции знаком конъюнкции. 4