打印
[FPGA]

大家来讨论一下这样一个简单的局部搜索算法

[复制链接]
1080|6
手机看帖
扫描二维码
随时随地手机跟帖
跳转到指定楼层
楼主
可木|  楼主 | 2015-10-14 21:39 | 只看该作者 回帖奖励 |倒序浏览 |阅读模式
ip, ps, AN, se, TI
本帖最后由 可木 于 2015-10-22 21:09 编辑

大家来讨论一下这样一个简单的局部搜索算法,在FPGA中实现如何在最短的时间内获得解?

WSAT(F,MAX-TRIES , MAX-FLIPS)
{
   for (i = 0; i < MAX-TRIES; i++) {
         T = randomly generated truth assignment;
         for (j = 0; j < MAX-FLIPS; j++) {
             if T satisfies F return T;
            c = an unsatisfied clause selected at random;
            v = a variable in c chosen by the Heuristic(c);
            T = T with v flipped;
           }
    }
}
简单说明一下F为CNF公式,如F(x1,x2,x3)=C1 | C2 | C3 | C4=(¬x1 & x2) | (¬x2 &¬x3) | (x1 &¬x2 & x3) | (x1 &¬x3),MAX-TRIES为给公式赋初值的次数,MAX-FLIPS为赋值T不满足F的情况下,翻转变量最大次数。以上算法过程是这样的:1.给定F和一组随机初值,如{x1,x2,x3}={1,1,1},可知C2=0,因此F=0.
2.选择C2,随机或利用启发式选择某一变量进行取反,假设选择X2,即{x1,x2,x3}={1,0,1},可知C2=1,但是C1=0,以此F=0,继续翻转变量。
3选择C1,随机或利用启发式选择某一变量进行取反,假设选择X1,即{x1,x2,x3}={0,0,1},可知C1=1,但是C4=0,以此F=0,继续翻转变量。
当尝试MAX-FLIPS次后任然没有找到一组赋值使F=1,则跳出此循环,重新赋一组初值继续上面循环,直到找到F=1的一组赋值。
不知道我是否表达清楚,有兴趣的兄弟可以一起探讨一下。F中可以有N个子句C,每个C最多包含三个X。




相关帖子

沙发
可木|  楼主 | 2015-10-16 23:55 | 只看该作者
没人有兴趣么??

使用特权

评论回复
板凳
drentsi| | 2015-10-18 14:41 | 只看该作者
这是用来干什么的,有C语音代码不,变量是整数还是布尔型

使用特权

评论回复
地板
可木|  楼主 | 2015-10-19 14:54 | 只看该作者
本帖最后由 可木 于 2015-10-19 14:58 编辑
drentsi 发表于 2015-10-18 14:41
这是用来干什么的,有C语音代码不,变量是整数还是布尔型

这个属于芯片形式化验证领域的,就是常说的可满足性问题,变量是布尔型。算法的最终目的就是在参数MAX-TRIES 和MAX-FLIPS规定的次数下试图寻找x1~xn的一个布尔集合,使公式F满足(=1)或者不满足(=0)。C语言代码没有~~:'(

使用特权

评论回复
5
可木|  楼主 | 2015-10-22 21:10 | 只看该作者
:(完全没反应了。。

使用特权

评论回复
6
feihufuture| | 2015-10-23 10:59 | 只看该作者
可木 发表于 2015-10-22 21:10
完全没反应了。。

理论性太强了,另外很少有人搞你这个专业,我也帮不了你

使用特权

评论回复
7
可木|  楼主 | 2015-10-25 10:36 | 只看该作者
feihufuture 发表于 2015-10-23 10:59
理论性太强了,另外很少有人搞你这个专业,我也帮不了你

确实是。。。。:'(

使用特权

评论回复
发新帖 我要提问
您需要登录后才可以回帖 登录 | 注册

本版积分规则

个人签名:A person afraid of loneliness, afraid to live up to two people !

26

主题

469

帖子

0

粉丝