0

SAT ソルバーである C プログラム picosat を最適化しようとしています。私の最後のプログラムは 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

一部のコメントが指摘しているように、そのコードは、コンパイルが最適化するのが特に簡単ではありません。大幅な改善を検討している場合は、コードの変更を開始する必要があります。強度の削減は簡単に開始でき、おそらく計算時間を数時間短縮できます。

于 2013-11-09T15:37:34.713 に答える
1

2012 年に、私はMicrosoft Visual Studio 2010 Expressを使用してWindowsPicosat 936でコンパイルしました。簡単ではありませんでした。特に、64 ビットのアドレス空間用にコンパイルする場合、メモリの配置とアドレスの計算はトリッキーでした。Linuxでのコンパイルははるかに簡単です。

同じ大学で開発されたマルチスレッド SAT ソルバー であるPlingelingを見ることができます。

多くの場合、 Plingelingは (古い) Picosatよりも高速です。

他の高速な SAT ソルバーは、 Riss3g、 CryptominisatまたはZ3です。

SAT コンペティション 2013では、SAT ソルビング アートの現状を概観できます。

SAT の解法の実行に時間がかかりすぎる場合は、問題のエンコーディングを改善する価値があるかもしれません。成功したSAT符号化技術は、この論文でレビューされます。

于 2014-01-05T14:39:08.657 に答える