PUZZLEUP 2015

newkid · 发表于 2015-9-4 04:15

〇〇发表于 2015-9-3 06:31
1*1 2*2 3*3分别几次

规律就是每个步骤都选中标准棋盘中那个黑色的方格。
3X3没有答案。
按此规律8X8应该是32步。但要怎么证明呢？

lugionline · 发表于 2015-9-4 06:48

newkid 发表于 2015-9-4 04:14
不知道，有证明估计也看不懂。
棋盘那个能证明吗？

说的就是棋盘那个阿，那个解太平凡了阿

lugionline · 发表于 2015-9-4 07:18

估计SQL也做不出来，我贴答案了

这次的代码有点长，但最后一句证明了只有一个解，求解SAT，我完全不了解SAT是怎么算的，但是不影响我用这个工具

In[10]:= B = 8;
X = Table[x[i, j], {i, B}, {j, B}];
target1 = Table[Mod[i + j, 2] == 1, {i, B}, {j, B}];
target1 = Table[Mod[i + j, 2] == 0, {i, B}, {j, B}];
chesses = Table[If[m == i || n == j, True, False], {i, B}, {j, B}, {m, B}, {n, B}];
CHESSES = Table[X[[Quotient[i, B] + 1, Mod[i, B] + 1]]
&& (chesses[[m, n]][[Quotient[i, B] + 1, Mod[i, B] + 1]]),
{m, B}, {n, B}, {i, 0, B*B - 1}];
EQUATION = Apply[And, MapThread[Xor, {Flatten@target1, Flatten@Apply[Xor, CHESSES, {2}]}]];
SOL = Count[(X /. FindInstance[EQUATION, Flatten@X]), True, 3]
SatisfiabilityCount[EQUATION, Flatten@X]

Out[17]= 32

Out[18]= 1

lugionline · 发表于 2015-9-4 07:21

基本原理如下：

In[20]:= FindInstance[a || b || c, {a, b, c}]
SatisfiabilityCount[a || b || c, {a, b, c}]

Out[20]= {{a -> True, b -> True, c -> True}}

Out[21]= 7

lugionline · 发表于 2015-9-4 07:31

暴力求解只能到4

In[1]:= board = Table[0, {4}, {4}];
target1 = Table[Mod[i + j, 2], {i, 4}, {j, 4}];
target2 = Table[Mod[i + j + 1, 2], {i, 4}, {j, 4}];
chesses = Table[If[m == i || n == j, 1, 0], {i, 4}, {j, 4}, {m, 4}, {n, 4}];
digits[n_] := Flatten@Position[Reverse@IntegerDigits[n, 2], 1] - 1;
chess[n_] := Map[chesses[[Quotient[#, 4] + 1, Mod[#, 4] + 1]] &, digits[n]];
solution[k_] := Fold[MapThread[BitXor[#1, #2] &, {#1, #2}, 2] &, board, chess[k]];
display[n_] := Table[If[BitAnd[n, 2^(i*4 + j)] == 0, 0, 1], {i, 0, 3}, {j, 0, 3}];
display /@ Select[Range[2^16 - 1], ((# == target1 || # == target2) &)[solution[#]] &]

Out[9]= {{{0, 1, 0, 1}, {1, 0, 1, 0}, {0, 1, 0, 1}, {1, 0, 1, 0}}, {{1, 0, 1, 0}, {0, 1, 0, 1}, {1, 0, 1, 0}, {0, 1, 0, 1}}}

newkid · 发表于 2015-9-4 09:29

lugionline 发表于 2015-9-4 06:48
说的就是棋盘那个阿，那个解太平凡了阿

是很平凡但是你能证明吗?
140那个图是上一题的吧，怎么全是直线，难道曲线的限制是可以去除的？

你的代码太高大了，SAT是啥？就是SatisfiabilityCount?
除了最后那个1有具体的输出吗？
现在我用SQL能解6X6, 花了17秒，8X8的还要再优化。

lugionline · 发表于 2015-9-4 09:55

本帖最后由 lugionline 于 2015-9-4 10:03 编辑

曲线应当是不必要的

自然可以输出好看点的格式，那就要贴图片

我就是构造64个布尔代数方程，然后把这些方程and起来去求解，不过我的True/False好像反了因为要XOR原始的False值，但是对结果没影响，算8*8大概10秒这样

里面构造CHESSES的方法有点笨，应当一遍就能算好的，矩阵操作还不是很懂

SatisfiabilityCount 可以算出这个方程有多少个解，这个返回1，那就是用程序方式证明了只有一个解

https://en.wikipedia.org/wiki/Boolean_satisfiability_problem