布尔逻辑表示的可除性（可满足性）答案

【问题标题】：Divisibility represented by Boolean logic (satisfiability)布尔逻辑表示的可除性（可满足性）
【发布时间】：2019-07-09 02:43:32
【问题描述】：

（从 Math StackExchange 复制并进行了一些修改，如果这不是正确的地方，请告诉我）

一些背景：我正在考虑使用 SAT 求解器来证明素数的可行性，尤其是梅森素数，通过证明不存在布尔数组 d[1],d[2],...,d[b '] 可以表示素数的除数（即 UNSAT）。

给定一个布尔列表 d[1],d[2],...,d[b]，其中 d 是 base-10 正整数 D 的 base-2 表示，是否存在一个布尔谓词当且仅当 2^b−1≡0(mod D) 时计算结果为 True？

（假设1<D<N，因此，b′<b。还假设 b 是素数。）

非常感谢任何帮助。

【问题讨论】：

标签： boolean boolean-logic boolean-expression satisfiability

【解决方案1】：

我的方法是创建一个乘数网络电路来找到给定数字的两个因子。然后电路由bc2cnf 转换为conjunctive normal form (CNF) 并提交给Cryptominisat、Clasp 或Z3 等SAT Solver。

因式分解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 cryptography 的灵丹妙药。

示例：要分解第七个梅森素数 (2^19-1)^2（一个 38 位数字）的平方，SAT 求解器 Z3 需要 186 秒。

【讨论】：