Отрицание через дизъюгкцию

[Sinoid]

Здравствуйте! Попалась такая задача:

Это что, формализацию, к примеру, места условия "$A$ не тождественно $X$" надо делать так: $(A=\text{Ж})\vee(A=\text{У})\vee(A=\text{Т})$? Просто у меня есть склонность к откапыванию ненужно сложных решений. Есть подозрение, что и в этом случае идея неоправданно сложная.

[arseniiv]

Т. е. подразумевается, что первые четыре попарно не равны и вторые четыре тоже попарно неравны, но при этом каждый первый равен кому-то из вторых (и требуется найти, какой какому)? Тогда так, как вы написали, по крайней мере можно делать. Насколько продуктивно, не знаю.

[Sinoid]

arseniiv в сообщении #1248193 писал(а):

Т. е. подразумевается, что первые четыре попарно не равны и вторые четыре тоже попарно неравны, но при этом каждый первый равен кому-то из вторых (и требуется найти, какой какому)

Дык вот об этом можно только догадываться, что подразумевается, а что нет.

-- 16.09.2017, 23:17 --

Сейчас пришло в голову. Еще вот это

Sinoid в сообщении #1248179 писал(а):

"$A$ не тождественно $X$"

можно еще и трактовать как "$X$ не тождественно $A$" - дополнительные конъюнкты...

[Sender]

Если совсем формально подходить, можно каждому возможному тождеству сопоставить свою булеву переменную:
А=Ж - x1
А=Х - x2
А=У - x3
А=Т - x4

В=Ж - x5
В=Х - x6,
...
Д=Т - x16.

Потом выписать все условия, которым они должны удовлетворять. Так, помимо условий 1-5, явно указанных в задаче, необходимо указать, что, к примеру, из всех переменных 1-й группы x1 - x4 истинное значение может принимать одна и только одна, x1 и x5 не могут быть истинными одновременно и т.д.
Ну и в конечном счёте преобразовать полученную формулу в ДНФ, чтобы увидеть все решения. Эту часть, на мой взгляд, лучше поручить компьютеру.

[Sinoid]

Sender в сообщении #1248391 писал(а):

Ну и в конечном счёте преобразовать полученную формулу в ДНФ, чтобы увидеть все решения. Эту часть, на мой взгляд, лучше поручить компьютеру.

И ответ стопудово не совпадет с книжным: задача еще из советской книги, тогда доступ к компам был ограничен, так что, наверняка, задача рассчитана на ручное решение.

(Оффтоп)

Sender в сообщении #1248391 писал(а):

Эту часть, на мой взгляд, лучше поручить компьютеру.

А вы знаете софт, который выдает СДНФ, СКНФ и т. п.? Только не онлайновый.

[Aritaborian]

Sinoid в сообщении #1248511 писал(а):

А вы знаете софт, который выдает СДНФ, СКНФ и т. п.?

Wolfram Mathematica: BooleanConvert.

[Sender]

Sinoid в сообщении #1248511 писал(а):

И ответ стопудово не совпадет с книжным

Думаете, в советское время пользовались какой-то другой логикой?

Конечно, можно и вручную решить. Возможных вариантов соответствия не так много - всего-то 24. Тут применять матпакет было бы и впрямь из пушки по воробьям, а так можно взять любой, способный управляться с символьными вычислениями в булевой алгебре.

Для решения вручную можно применить что-то вроде перебора с возвратом, только желательно выбирать предположения, отсекающие побольше вариантов.

[Sinoid]

Aritaborian в сообщении #1248515 писал(а):

Wolfram Mathematica: BooleanConvert
.

Там же покупать надо...

Sender в сообщении #1248518 писал(а):

Думаете, в советское время пользовались какой-то другой логикой?

Как раз так я не думаю. Я думаю, что с первого раза из-за допущения довольно-таки вольной трактовки условия задачи ответ не совпадет, прокапаюсь где-то день с эквивалентными преобразованиями вариантов, а с матпакетом бы за 5 сек.

-- 17.09.2017, 22:32 --

Sender в сообщении #1248518 писал(а):

а так можно взять любой, способный управляться с символьными вычислениями в булевой алгебре.

Так а вы конкретно какой-нибудь можете порекомендовать? (Бесплатный).

[Aritaborian]

Sinoid в сообщении #1248524 писал(а):

Там же покупать надо

Надо было сразу уточнять, что хотите бесплатный. И потом, можно скачать пробную версию на 15 дней. Не говоря уж о возможных дальнейших, хм, незаконных с ней манипуляциях

[Sinoid]

Aritaborian в сообщении #1248527 писал(а):

И потом, можно скачать пробную версию на 15 дней. Не говоря уж о возможных дальнейших, хм, незаконных с ней манипуляциях

Но, к сожалению, не мне. Мне бы ваши навыки, да математику arseniiv'а.

[Sender]

Sinoid в сообщении #1248524 писал(а):

Так а вы конкретно какой-нибудь можете порекомендовать? (Бесплатный).

Ну вот чтобы далеко не ходить, есть онлайновая wolframalpha, например. А так - SymPy вроде что-то такое умеет.

-- Вс сен 17, 2017 23:04:26 --

Руками посчитать и впрямь может оказаться проще.

[arseniiv]

Sinoid в сообщении #1248511 писал(а):

И ответ стопудово не совпадет с книжным

Ну давайте сравним.

(Тут ответ и решение.)

(* Wolfram Mathematica 8 *)
abcd = {a, b, c, d};  (* АБСД *)
wxyz = {w, x, y, z};  (* ЖХУТ (кажется очевидным, что это WXYZ) *)

(* все возможные варианты в виде списка списков пар равных атомов *)
arrangements = Table[MapThread[{#1, #2} &, {abcd, wxyzn}],
    {wxyzn, Permutations[wxyz]}];

(* возможные равенства атомов (список пар) *)
possibilities = Join @@ Table[{i, j}, {i, abcd}, {j, wxyz}];

(* неявные ограничения на равенства и неравенства атомов *)
eqs0 = Or @@ Map[And @@ # &, 
    Table[If[MemberQ[arr, p], e @@ p, ! e @@ p],
        {arr, arrangements}, {p, possibilities}]];

(* все ограничения, включая явные *)
eqs = eqs0 &&
    (! e[a, x] \[Implies] ! e[c, y]) &&
    (e[b, y] || e[b, z] \[Implies] e[a, x]) &&
    (! e[c, w] \[Implies] e[b, z]) &&
    (e[d, y] \[Implies] ! e[b, x]) &&
    (! e[d, x] \[Implies] e[b, x]);  (* в редакторе \[Implies] выглядит как ⇒ *)
eqs // LogicalExpand // Resolve
(* в выбранном мною пути без LogicalExpand не срабатывает, читайте предложение Aritaborian *)
(* зато с этим Resolve удачно выдаёт СДНФ (кажется, иногда не выдаёт, не помню) *)

Ответ:

e[a, y] && e[b, x] && e[c, w] && e[d, z] &&
    ! e[a, w] && ! e[a, x] && ! e[a, z] && ! e[b, w] &&
    ! e[b, y] && ! e[b, z] && ! e[c, x] && ! e[c, y] &&
    ! e[c, z] && ! e[d, w] && ! e[d, x] && ! e[d, y]

То есть, в наших терминах, А = У, Б = Х, С = Ж, Д = Т.

P. S. Знаю, что это в текущем контексте не совсем уместно, но уже переписал сюда код (а написал я его днём, заинтересовавшись единственностью и существованием решения), когда увидел новые ответы, а удалять не хочется… Вообще приводилку к СДНФ можно довольно быстро написать (заодно попрактиковавшись в понимании алгоритма в учебнике!). Вот задавать ей исходную формулу вручную я бы постеснялся, а чтобы генерировать её, нужно или добавлять к приводилке нехилый скриптовый движок, или, что выглядит разумнее, сгенерировать задание на том же языке, на котором написана она сама. Но любая смена задании тогда потребует перекомпиляции, если язык компилирующийся. Если б я хорошо разбирался в Python, посоветовал бы его — там и DSL должно быть легко сделать, чтобы вводить куски формул красиво и легко.

[Sinoid]

arseniiv, ответ-то правильный, только мне ваш код, к сожалению, вставить некуда (не для этой задачи, а на будущее).

[arseniiv]

Да это я просто кому интересно.

[Sinoid]

Sender в сообщении #1248518 писал(а):

Конечно, можно и вручную решить. Возможных вариантов соответствия не так много - всего-то 24

А, вы вот к чему. Нет, задача явно рассчитана не на этот способ решения, она дана после изучения равносильности формул.