Solver 變數和函式
阿新 • • 發佈：2020-10-10
型別
|
變數名
|
初始化 |
功能 |
| int | incremental |
static BoolOption opt_incremental(_cat, "incremental", "Use incremental SAT solving", false);
incremental(opt_incremental)
|
Use incremental SAT solving |
| vec<lbool> | model | vec() : data(NULL), sz(0), cap(0) {} | If problem is satisfiable, this vector contains the model |
| vec<Lit> | conflict | vec() : data(NULL), sz(0), cap(0) {} | If problem is unsatisfiable，this vector represent the final conflict clause expressed in the assumptions. |
| uint64_t | solves | 初始化為0 | 目前沒發現什麼用處 |
| uint64_t |
starts |
初始化為0 | 統計重啟次數？ |