0

我正在尝试优化 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:
4

2 回答 2

1

Picosat 936早在 2012 年，我在Windows下使用Microsoft Visual Studio 2010 Express进行编译。这并不容易。尤其是，如果你想编译 64 位地址空间，内存对齐和地址算法就很棘手。在Linux下编译应该容易得多。

您可以查看Plingeling，这是同一所大学开发的多线程 SAT 求解器。

在许多情况下， Plingeling比（年长的）Picosat更快。

其他快速 SAT 求解器是Riss3g、 Cryptominisat或Z3。

SAT Competition 2013很好地概述了 SAT 求解艺术的当前状态。

如果您的 SAT 求解运行时间过长，则可能值得改进您的问题编码。本文回顾了成功的 SAT 编码技术。

于 2014-01-05T14:39:08.657 回答
1

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

于 2013-11-09T15:37:34.713 回答