Система традиционно решается методом битовых масок, так как для Х-ов это хорошо известная верхнетреугольная матрица и остается подсчитать число решений для каждой из ее строк , что не представляет особой трудности для 4 импликаций , но для 9 импликаций с соответсвующей матрицей из 10 строк уже станет несколько утомительно (вручную).
Ниже следует решение основанное на построении полного графа системы с последующим примением техники предложеной Е.А.Мирончик [ 1 ] .
Рассмотрим систему, где использование битовых масок потребует большого количества вычислений и конвертируем ее следующим образом
(x1=>x2)^(x2=>x3)^(x3=>x4)(x4=>x5)^(x5=>x6)^(x6=>x7)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x7^¬y7^z7) v (x7^y7^¬z7)) =1
Конвертированная система
(x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
(x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
(x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
(x4=>x5)^((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
(x5=>x6)^((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
(x6=>x7)^((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x7^¬y7^z7) v (x7^y7^¬z7)) =1
Замети, что пример Р-34 из ege23.doc в момент написания этого текста повидимому содержит опечатку либо неточность
Думаю, что правильная версия системы в образце - следующая
Строим полный граф для последней системы.В отличие от битовых масок увеличение размеров матрицы обрабатывется без длинных вычислений.
Тестируем на сервере Полякова
Решаем систему с 9 импликациями и матрицой из 10 строк.
Для этой системы битовая матрица для строк будет уже иметь
глубину 10, но для нашего подхода это не имеет нникакого
значения
Конвертируем систему :-
(x1=>x2)^(x2=>x3)^(x3=>x4)^(x4=>x5)^(x5=>x6)^(x6=>x7)^
^(x7=>x8)^(x8=>x9)^(x9=>x10)=1
((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1
Строим полный граф системы ( просто еще три "fork" иттерации )
(x1=>x2)^((¬x1^y1^z1) v (x1^¬y1^z1) v (x1^y1^¬z1)) =1
(x2=>x3)^((¬x2^y2^z2) v (x2^¬y2^z2) v (x2^y2^¬z2)) =1
(x3=>x4)^((¬x3^y3^z3) v( x3^¬y3^z3) v (x3^y3^¬z3)) =1
(x4=>x5)^((¬x4^y4^z4) v (x4^¬y4^z4) v (x4^y4^¬z4)) =1
(x5=>x6)^((¬x5^y5^z5) v (x5^¬y5^z5) v (x4^y5^¬z5)) =1
(x6=>x7)^((¬x6^y6^z6) v (x6^¬y6^z6) v (x6^y6^¬z6)) =1
(x7=>x8)^((¬x7^y7^z7) v (x6^¬y6^z7) v (x7^y7^¬z7)) =1
(x8=>x9)^((¬x8^y8^z8) v (x8^¬y8^z8) v (x8^y8^¬z8)) =1
(x9=>x10)^((¬x9^y9^z9) v (x9^¬y9^z9) v (x9^y9^¬z9)) =1
((¬x10^y10^z10) v (x10^¬y10^z10) v (x10^y10^¬z10)) =1
