CDCLSolver

addClause void addClause(Clause clause): 与えられた節をソルバーの制約として追加します。
addConflictClause void addConflictClause(Clause conflict): 与えられた節を学習節として追加します。
addEdge void addEdge(Literal from, Literal to, Clause.ID clauseID): Undocumented in source. Be warned that the author may not have intended to support it.
addNode void addNode(Literal lit, size_t dlevel): Undocumented in source. Be warned that the author may not have intended to support it.
analyzeConflict analyzeConflictResult analyzeConflict(): 矛盾を分析します。
assignLiteral void assignLiteral(T literals): 与えられたリテラルが真になるように変数への真偽値割り当てを行います。
backtrack void backtrack(size_t dlevel): 与えられたレベルまでバックトラックします。具体的には、ソルバーの状態を与えられたレベルのときのソルバーの状態まで復元します。
decideNextBranch void decideNextBranch(): 真偽値が未割り当ての変数を1つ選んで真を割り当てます。
deduce SolverStatus deduce(): 単位伝播を繰り返します。途中で矛盾が生じたら CONFLICT を返します。矛盾なくすべての変数に真偽値を割り当てられたら SAT を返します。それ以外の場合には OK を返します。
generateGraph1 string generateGraph1(bool conflict): implication graph の定義に即した形のグラフを表す DOT 言語のソースを返します。
generateGraph2 string generateGraph2(bool conflict): implication graph を元に、単位伝播で用いられた節も頂点にしたグラフの DOT 言語のソースを返します。
initialize void initialize(parseResult res): 読み込んだ CNF の情報を元にソルバーを初期化します。
newClause Clause newClause(T literals): 与えられたリテラルを含んだ新しい節を作成します。
newClause Clause newClause(Set!T literals): 与えられたリテラルの集合に対応する新しい節を作成します。
nextClauseID Clause.ID nextClauseID(): Undocumented in source. Be warned that the author may not have intended to support it.
removeClausesContaining void removeClausesContaining(Literal lit): 与えられたリテラルを含む節を削除します。
removeLiteralFromClauses void removeLiteralFromClauses(Literal lit): 与えられたリテラルをそれぞれの節の中から削除します。
reset void reset(): ソルバーの状態を、真偽値割り当てがなされていない初期状態にリセットします。初期化時以外で追加された制約はそのまま追加された状態を維持します。
solve CDCLSolverResult solve(): 問題を与えて初期化したソルバーで実行すると、その問題を解いて結果を返します。
toDOT void toDOT(bool conflict): implication graph の状態を DOT 言語で出力します。ファイル名は 1.dot, 2.dot, … のように続きます。

Variables

availClauses auto availClauses;: まだ充足されていない節の ID の集合
clauses Clause[Clause.ID] clauses;: Undocumented in source.
clausesContainingLiteral Set!(Clause.ID)[Literal] clausesContainingLiteral;: Undocumented in source.
conflictCount ulong conflictCount;: Undocumented in source.
currentLevel size_t currentLevel;: implication graph 上の頂点の decision level の最大値
decisionVariables Literal[] decisionVariables;: Undocumented in source.
generateAnotherGraph bool generateAnotherGraph;: Undocumented in source.
generateGraph bool generateGraph;: Undocumented in source.
history CDCLSolver[] history;: ソルバーの状態が各 decision level に対応して保持されている配列
implicationGraph ImplicationGraph implicationGraph;: Undocumented in source.
originalClauses Clause[Clause.ID] originalClauses;: CNF の単純化が適用されていない形の節
preamble Preamble preamble;: Undocumented in source.
restart bool restart;: Undocumented in source.
restartMult double restartMult;: Undocumented in source.
restartThreshold long restartThreshold;: Undocumented in source.
unassignedVariables Set!(long) unassignedVariables;: Undocumented in source.
unitClauses auto unitClauses;: Undocumented in source.

CDCLSolver

Constructors

Members

Aliases

Enums

Functions

Variables

Meta

Source