ele*_*ora 5 algorithm performance logic
[与2013年9月27日https://codegolf.stackexchange.com/questions/12664/implement-superoptimizer-for-addition相关]
我对如何编写超级优化器感兴趣.特别是找到比特和的小逻辑公式.之前这是对codegolf的挑战,但它似乎比人们想象的要困难得多.
我想编写代码,找到最小可能的命题逻辑公式,以检查y二进制0/1变量的总和是否等于某个值x.让我们调用变量x1,x2,x3,x4等.在最简单的方法中,逻辑公式应该等于和.也就是说,当且仅当和等于x时,逻辑公式才应该为真.
这是一种天真的方式.假设y = 15且x = 5.选择所有3003种不同的方式来选择5个变量,并为每个变量创建一个带有这些变量的AND的新子句和剩余变量否定的AND.你最终会得到3003个条款,每个条款的长度恰好为15个,总费用为45054.
但是,如果允许您在解决方案中引入新变量,那么通过消除常见的子公式可以大大减少这一点.所以在这种情况下,你的逻辑公式由y二元变量x和一些新变量组成.当且仅当y变量的总和等于x时,整个公式才是可满足的.唯一允许的运营商是and,or和not.
事实证明,当x = 1时,有一种解决这个问题的聪明方法,至少在理论上是这样.但是,我正在寻找一种计算密集型方法来搜索小型解决方案.
How can you make a superoptimizer for this problem?
例子.举两个变量作为一个例子,我们想要一个逻辑公式,当它们总和为1时就是True.一个可能的答案是:
(((not y0) and (y1)) or ((y0) and (not y1)))
为了引入新的变量成式如z0以表示y0 and not y1那么我们可以引入新的条款 (y0 and not y1) or not z0和更换y0 and not y1通过z0贯穿式的其余部分.当然,在这个例子中这是没有意义的,因为它使表达更长.