- 注册时间
- 2017-12-7
- 最后登录
- 1970-1-1
- 威望
- 星
- 金币
- 枚
- 贡献
- 分
- 经验
- 点
- 鲜花
- 朵
- 魅力
- 点
- 上传
- 次
- 下载
- 次
- 积分
- 3243
- 在线时间
- 小时
|
马上注册,结交更多好友,享用更多功能,让你轻松玩转社区。
您需要 登录 才可以下载或查看,没有账号?欢迎注册
×
仅供娱乐,实用性仅限于将电脑变成expensive room heater
--
下面的变量都是取值0(false)或1(true)的布尔变量,!0=1,!1=0,
首先,1bit*1bit的乘法(或者说and)可以用4个3-sat表达式进行表达:
x or y or !and // x=0,y=0时!and必然为1,于是and=0
!x or y or !and // x=1,y=0时and=0
x or !y or !and// x=0,y=1时and=0
!x or !y or and // x=1,y=1时and=1
这样,四个表达式可以将and变量限定为1bit乘法x*y的取值
类似地,
x or y or !xor
!x or !y or !xor
!x or y or xor
x or !y or xor
这四个表达式可以计算x与y的xor值
而x+y的个位为x xor y,进位为x and y,这样我们就可以通过3-SAT构造nbit的两个表达式left与right的乘法
把乘法送去跑SAT,就可以得到一个基于SAT的分解因式
生成SAT表达式的程序有些烂,这里只放一个开头(其实只有60个需要确认的比特,准确地说如果会简单的模除法,只需要确认30个bit就能知道分解是否存在,但……)
计算用的公式为- 1xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx1*1xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx1=110000100110100111101000100101001110110010001110100000001011011 // 2614647029*3004108631,二进制的读法是小端序,最左边是“个位”
复制代码
得到的因数为
- c [Constant(true), Node(1), Node(2), Node(3), Node(4), Node(5), Node(6), Node(7), Node(8), Node(9), Node(10), Node(11), Node(12), Node(13), Node(14), Node(15), Node(16), Node(17), Node(18), Node(19), Node(20), Node(21), Node(22), Node(23), Node(24), Node(25), Node(26), Node(27), Node(28), Node(29), Node(30), Constant(true)]
- c [Constant(true), Node(31), Node(32), Node(33), Node(34), Node(35), Node(36), Node(37), Node(38), Node(39), Node(40), Node(41), Node(42), Node(43), Node(44), Node(45), Node(46), Node(47), Node(48), Node(49), Node(50), Node(51), Node(52), Node(53), Node(54), Node(55), Node(56), Node(57), Node(58), Node(59), Node(60), Constant(true)]
复制代码
结果如下:
计算SAT的是https://github.com/arminbiere/kissat
算了一天,真的是难为我家电脑了…… |
|