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

Question

我正在尝试优化 C 程序 picosat，它是一个 SAT 求解器。我的上一个程序运行了 24 小时，因此优化可以节省我的时间。

• picosat

注意: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

正如一些评论指出的那样，编译优化代码并不是特别容易。如果您希望进行任何重大改进，则需要开始更改代码。强度降低将是一个简单的起点，并且可能会减少您的计算时间。