（从Math StackExchange复制并进行一些修改，告诉我这是不是正确的地方）
一些背景：我正在考虑使用SAT求解器证明素数的可行性，尤其是梅森素数，通过显示不存在布尔数组d [1]，d [2]，...，d [b']可以代表素数的除数（即UNSAT）。
给定一个布尔列表d [1]，d [2]，...，d [b]，其中d是基数为10的正整数D的基-2表示，是否存在一个计算结果为True的布尔谓词当且仅当2 ^ b-1≡0（mod D）？
（假设1<D<N，因此，b′<b。也假设b是素数。）
任何帮助是极大的赞赏。
我的方法是创建一个乘法器网络电路来找到给定数字的两个因子。然后该电路由bc2cnf翻译成conjunctive normal form (CNF)并提交给SAT解算器，如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 cryptography的银弹。
示例：为了计算第七个Mersenne素数（2 ^ 19-1）^ 2（一个38位数）的平方，SAT求解器Z3需要186s。
相关论文是Satisfy This: An Attempt at Solving Prime Factorization using Satisfiability Solvers。