Caidicalのポート

メモリ削減アイデアの検証用ソルバとして、Cadicalをポートします。

Cadicalは、KissatのC++バージョンです。Kissatは、未だにincrementalではないし、Maxsatでは必須のassumptionもサポートしていません。その点Cadicalは、Kissatに比べればメモリは、3倍位食いますが、最先端のソルバでありながら、全てのMaxSAT必要条件を満たします。大規模用の整数化ソルバとしてメタヒューリスティクスを検討していましたが、SATソルバでも上手く行けば、大規模でも性能を発揮できる可能性がある、と考えました。

コテコテのLinuxソースなのでWindowsポートは大変です。

#ifdef _WIN32

#define cadical_putc_unlocked _putc_nolock

#define cadical_getc_unlocked _getc_nolock

#else

#define cadical_putc_unlocked putc_unlocked

#define cadical_getc_unlocked getc_unlocked

#endif

#define NBUILD;__WIN32;NOGDI;

__builtin_clz  ⇒pal-winの中のunistdh　にマクロ

#ifdef _WIN32

    Strict=2

#else

    STRICT = 2,

#endif