BOINC年度会议小结【图片已更新】

fwjmath · 发表于 2013-10-3 23:48:22

超哥不郁闷发表于 2013-10-3 17:16
又找到一点机械证明的相关资料（http://hi.baidu.com/haventhair/item/34f063f9c3857713ce9f32c2） ...

我看了一下，基本上如果是有算法的，证定理基本不需要太大的计算量，因为本来开发算法的目的就是减少计算量……自动搜寻定理的话，其中一个缺陷就是不知道搜出来的定理是不是足够有趣，如果只是为搜而搜的话，没太大意思……而且我觉得我们论坛也没多少人懂这个，没这个技术力量……

其实基本方向应该是找那些无论如何都没有太好的算法的那种问题，猜想验证是一种，NP完全问题是一种，有复杂的逻辑背景的问题也是一种（其实NP完全问题也可以算在这种内），穷举打表也是一种。四种类别的例子分别有奇异奇数搜索、SAT@home、RamseyX和Numberfields@home。前三个其实学数学的会点编程或者学编程的会点数学就能搞出来，后一个稍复杂些，但是查点资料也能搞出来，按图索骥的话。我觉得这些才是找题材比较好的方向，而且还要找那些之前做过的人不多的，不是随便找个跟计算相关的都可以的。

arthur200000 · 发表于 2013-10-4 00:22:36

ZizhengTai 发表于 6 天前
看起来好厉害的样子！什么时候我也能去围观一下就好了T T...

破纪录很好的样子我也要（带显卡不来自: iPhone客户端

DrEason7-11 · 发表于 2013-10-4 01:02:26

楼主，我是医学院毕业的，也做过生命科学方面的实验，对于文献阅读没有问题，志愿帮助WCG校对和翻译，如有需要请随时和我联系

Stella · 发表于 2013-10-4 01:40:03

acp134 发表于 2013-10-3 12:33
我随口说个三体问题……
我真的是随口说的

没记错的话milkyway部分包的后缀里有N-body这个词。或许Milkyway已经开始做相关的东西了

acp134 · 发表于 2013-10-4 09:13:43

Stella 发表于 2013-10-4 01:40
没记错的话milkyway部分包的后缀里有N-body这个词。或许Milkyway已经开始做相关的东西了
...

或许吧

JUST · 发表于 2013-10-4 12:00:15

fwjmath 发表于 2013-10-3 23:48
我看了一下，基本上如果是有算法的，证定理基本不需要太大的计算量，因为本来开发算法的目的就是减少计算 ...

我现在的组就是做formal method的，不过他们主要做model checking，本质就是搜索model checking做分布式计算是可以，也很有意义，比如能支持CSP
不过工程上相当复杂，网络传输也很大，未必适合BOINC

自动定理证明这个东西也算是formal的一个方向，已经有很多tool
总的来说是first-order表达的问题自动证明没啥问题，higher-order的自动证明很局限
现在可行的都是靠人来指导证明，也就是交互式证明interactive theorem proving，人来决定证明的方向，机器来推导

超哥不郁闷 · 发表于 2013-10-4 13:36:03

JUST 发表于 2013-10-4 12:00
我现在的组就是做formal method的，不过他们主要做model checking，本质就是搜索model checking做分布式 ...

也就是说这个方向有希望啰？

fwjmath · 发表于 2013-10-4 13:50:00

JUST 发表于 2013-10-4 12:00
我现在的组就是做formal method的，不过他们主要做model checking，本质就是搜索model checking做分布式 ...

model checking上分布式的困难可以详细讲讲吗？如果只是搜索的话手头上应该有些办法的。

JUST · 发表于 2013-10-4 14:09:36

fwjmath 发表于 2013-10-4 13:50
model checking上分布式的困难可以详细讲讲吗？如果只是搜索的话手头上应该有些办法的。

...

搜索是图的搜索，所以每个子任务分配时并不知道边界节点
当然这个还是能分布式的，只是算法不好效率很低，可能重复计算

最主要的瓶颈在网络
需要用分布式来算的模型一定很大，整个图可能上亿个节点，每个节点至少几KB的信息
就算每个chunk几百万的节点，也是上GB的信息需要upload到服务器

目前情况是能单节点并行就不错了，分布式一般也是cluster，在Internet分布式目前应该没有

JUST · 发表于 2013-10-4 14:13:41

超哥不郁闷发表于 2013-10-4 13:36
也就是说这个方向有希望啰？

定理证明除非特定类型命题基本不可自动证明，更谈不上分布式了
目前都是人脑+电脑的模式

gameboybf2142 · 发表于 2013-10-4 14:20:40

JUST 发表于 2013-10-3 22:13
定理证明除非特定类型命题基本不可自动证明，更谈不上分布式了
目前都是人脑+电脑的模式
...

如果重新开始计算pi的话可不可以分享一下源码？万分感谢

JUST · 发表于 2013-10-4 14:25:07

还有个相关的，或许大家感兴趣
就是代码综合，就是你给一堆输入和输出，然后自动把code生成出来
比如
input: 1, output:1
input: 2, output:1
input: 3, output:2
input: 4, output:3
input: 5, output:5
理论上应该能给出个斐波那契的程序

其实这些都很有意思，也是不缺数据的
但都不是有现成算法的东西，真做出来能用的够两个master毕业了

JUST · 发表于 2013-10-4 14:26:49

gameboybf2142 发表于 2013-10-4 14:20
如果重新开始计算pi的话可不可以分享一下源码？万分感谢

旧的代码是公开的
新的我打算是开源

fwjmath · 发表于 2013-10-4 14:55:19

JUST 发表于 2013-10-4 14:09
搜索是图的搜索，所以每个子任务分配时并不知道边界节点
当然这个还是能分布式的，只是算法不好效率很低 ...

……数据密集的话现在没啥好办法……那这个还是先放着吧……

gameboybf2142 · 发表于 2013-10-4 15:05:29

JUST 发表于 2013-10-3 22:26
旧的代码是公开的
新的我打算是开源

请教一下旧的源码用的是什么算法呢？如果新的算法用BBP公式可以吗？

		自动登录	找回密码
密码			新注册用户