C: picosat SAT求解器的编译优化

Question

我正在尝试优化C程序picosat，这是一个SAT解决程序。我的上一个程序运行了24小时，所以优化可能会让我安全几个小时。

• 皮科星

注意: picosat是单线程的！多线程SAT求解是一个开放的问题。

我的计划是尝试用多个C编译器来编译picosat，看看哪个编译器产生的代码最快。

但是，我没有编译

有什么建议可以优化我的性能吗？到目前为止，我只使用了-O3，而仅仅是为了完善，-O4并没有提高性能。

如果有关系，这是我的CPU：

processor       : 23
vendor_id       : GenuineIntel
cpu family      : 6
model           : 44
model name      : Intel(R) Xeon(R) CPU           X5650  @ 2.67GHz
stepping        : 2
microcode       : 0x10
cpu MHz         : 1596.000
cache size      : 12288 KB
physical id     : 1
siblings        : 12
core id         : 10
cpu cores       : 6
apicid          : 53
initial apicid  : 53
fpu             : yes
fpu_exception   : yes
cpuid level     : 11
wp              : yes
flags           : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx pdpe1gb rdtscp lm constant_tsc arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est tm2 ssse3 cx16 xtpr pdcm pcid dca sse4_1 sse4_2 popcnt aes lahf_lm arat epb dtherm tpr_shadow vnmi flexpriority ept vpid
bogomips        : 5333.19
clflush size    : 64
cache_alignment : 64
address sizes   : 40 bits physical, 48 bits virtual
power management:

Answer 1

正如一些注释所指出的，对于编译来说，优化代码并不是特别容易。如果您希望进行任何重大改进，则需要开始更改代码。力量削减将是一个容易的地方开始，可能会减少几个小时的计算。

Answer 2

早在2012年，我就用MicrosoftVisualStudio2010Express在Windows下编译了Picosat 936。这可不容易。特别是，如果您想要编译64位地址空间，那么内存对齐和地址算法是很棘手的。Linux下的编译应该要容易得多。

你可以看看平岭，一种在同一所大学开发的多线程SAT解算器。

在许多情况下，打板的速度快于(老的)皮卡。

其他快速SAT解算器是Riss3g、隐孢子虫或Z3。

SAT比赛2013很好地概述了SAT解决技术的现状。

如果您的SAT解题运行时间过长，那么改进您的问题编码可能是值得的。本论文综述了成功的SAT编码技术。