Делимость, представленная булевой логикой (выполнимость) - PullRequest
Новая
       89

Делимость, представленная булевой логикой (выполнимость)

0 голосов
/ 15 февраля 2019

(Скопировано из Math StackExchange с некоторыми изменениями, скажите мне, если это не то место)

Некоторый контекст: я думал о целесообразности использования решателей SAT для доказательства простоты, особенно простых чисел Мерсенна, показывая, что не существует никакого логического массива d [1], d [2], ..., d [b '], который может представлять делитель простого числа (т. е. UNSAT).

При условии логического значениясписок d [1], d [2], ..., d [b], где d - это представление base-10 натуральных чисел D-10, существует ли булев предикат, который оценивается как True, если и толькоесли 2 ^ b − 1≡0 (mod D)?

(Предположим, 1<D<N и, следовательно, b′<b. Также предположим, что b простое число.)

Любая помощь будет принята с благодарностью.

1 Ответ

0 голосов
/ 15 февраля 2019

Мой подход состоял в том, чтобы создать сетевую схему множителя, чтобы найти два фактора данного числа.Затем схема преобразуется с bc2cnf в конъюнктивную нормальную форму (CNF) и передается в SAT Solver, например Cryptominisat , Clasp или Z3 .

Пример схемы для факторинга 17 ( bc2cnf формат): 

BC1.0
//  P = 17
_t1 := A0 & B0;
_t2 := A1 & B0;
_t3 := A2 & B0;
_t4 := A0 & B1;
_t5 := A1 & B1;
_t6 := A2 & B1;
_t7 := A0 & B2;
_t8 := A1 & B2;
_t9 := A2 & B2;
_t10 := A0 & B3;
_t11 := A1 & B3;
_t12 := A2 & B3;
_t13 := A0 & B4;
_t14 := A1 & B4;
_t15 := A2 & B4;
_t16 := ODD(_t2, _t4);
_t17 := _t2 & _t4;
_t18 := ODD(_t3, _t5);
_t19 := _t3 & _t5;
_t20 := ODD(_t7, _t17);
_t21 := _t7 & _t17;
_t22 := ODD(_t18, _t20);
_t23 := _t18 & _t20;
_t24 := ODD(_t6, _t8);
_t25 := _t6 & _t8;
_t26 := ODD(_t10, _t19);
_t27 := _t10 & _t19;
_t28 := ODD(_t21, _t23);
_t29 := _t21 & _t23;
_t30 := ODD(_t24, _t26);
_t31 := _t24 & _t26;
_t32 := ODD(_t28, _t30);
_t33 := _t28 & _t30;
_t34 := ODD(_t9, _t11);
_t35 := _t9 & _t11;
_t36 := ODD(_t13, _t25);
_t37 := _t13 & _t25;
_t38 := ODD(_t27, _t29);
_t39 := _t27 & _t29;
_t40 := ODD(_t31, _t33);
_t41 := _t31 & _t33;
_t42 := ODD(_t34, _t36);
_t43 := _t34 & _t36;
_t44 := ODD(_t38, _t40);
_t45 := _t38 & _t40;
_t46 := ODD(_t42, _t44);
_t47 := _t42 & _t44;
_t48 := ODD(_t12, _t14);
_t49 := _t12 & _t14;
_t50 := ODD(_t35, _t37);
_t51 := _t35 & _t37;
_t52 := ODD(_t39, _t41);
_t53 := _t39 & _t41;
_t54 := ODD(_t43, _t45);
_t55 := _t43 & _t45;
_t56 := ODD(_t47, _t48);
_t57 := _t47 & _t48;
_t58 := ODD(_t50, _t52);
_t59 := _t50 & _t52;
_t60 := ODD(_t54, _t56);
_t61 := _t54 & _t56;
_t62 := ODD(_t58, _t60);
_t63 := _t58 & _t60;
_t64 := ODD(_t15, _t49);
_t65 := _t15 & _t49;
_t66 := ODD(_t51, _t53);
_t67 := _t51 & _t53;
_t68 := ODD(_t55, _t57);
_t69 := _t55 & _t57;
_t70 := ODD(_t59, _t61);
_t71 := _t59 & _t61;
_t72 := ODD(_t63, _t64);
_t73 := _t63 & _t64;
_t74 := ODD(_t66, _t68);
_t75 := _t66 & _t68;
_t76 := ODD(_t70, _t72);
_t77 := _t70 & _t72;
_t78 := ODD(_t74, _t76);
_t79 := _t74 & _t76;
_t80 := ODD(_t65, _t67);
_t81 := ODD(_t69, _t71);
_t82 := ODD(_t73, _t75);
_t83 := ODD(_t77, _t79);
_t84 := ODD(_t80, _t81);
_t85 := ODD(_t82, _t83);
_t86 := ODD(_t84, _t85);
_aBits := OR(A0, A1, A2);
_bBits := OR(B0, B1, B2, B3, B4);
ASSIGN _aBits, _bBits;
ASSIGN ~_t1, ~_t16, ~_t22, ~_t32, ~_t46, ~_t62, ~_t78, ~_t86;

В моих экспериментах максимальное количество битов вчисло, подлежащее факторированию, довольно мало.Следовательно, решатели SAT не являются серебряной пулей для победы над криптографией RSA .

Пример: Чтобы вычислить квадрат седьмого простого числа Мерсенна (2 ^19-1) ^ 2, 38-битное число, для решения SAT Z3 необходимо 186 с.

Соответствующий документ: Удовлетворить это: Попытка решения факторизации простых чисел с использованием решателей удовлетворенности .

...