public interface ISatSolver
修飾子とタイプ | メソッドと説明 |
---|---|
void |
add(int lit_or_zero) |
void |
addAssumptions(int[] assumptions) |
int |
addAtLeast(int[] literals,
int k) |
int |
addAtLeastWithAssumption(int[] literals,
int k,
int assumption) |
int |
addAtMost(int[] literals,
int k) |
int |
addAtMostWithAssumption(int[] literals,
int k,
int assumption) |
void |
addBlockingClause() |
void |
addBlockingClause(int[] clause) |
void |
addClause(int[] clause) |
void |
addClauses(int[][] clauses) |
int |
addExactly(int[] literals,
int k) |
int |
addExactlyWithAssumption(int[] literals,
int k,
int assumption) |
void |
addNormalizedClause(int[] clause) |
int |
addPB(int[] weights,
int[] literals,
int k,
boolean isgeq) |
int |
addPBWithAssumption(int[] weights,
int[] literals,
int k,
boolean isgeq,
int assumption) |
void |
assume(int lit) |
void |
done() |
int |
failed(int lit) |
int |
getClauses() |
int[] |
getFailed(int[] literals) |
int[] |
getIntModel() |
java.util.BitSet |
getModel() |
int[] |
getMUS() |
java.lang.String |
getSignature() |
java.lang.String |
getSolverName() |
double |
getTime() |
int |
getVars() |
ISatSolver |
init() |
boolean |
isEliminated(int lit) |
void |
newVar(int howmany) |
void |
outputModel() |
void |
release() |
void |
setFrozen(int lit) |
void |
setTerminate(int value) |
void |
setVars(int count) |
void |
setVerbosity(int verbosity) |
int |
solve() |
int |
solve(int[] assumptions) |
int |
val(int lit) |
java.lang.String getSignature()
ISatSolver init()
void release()
void add(int lit_or_zero)
void assume(int lit)
int solve()
int val(int lit)
int failed(int lit)
void setTerminate(int value)
java.lang.String getSolverName()
void setVerbosity(int verbosity)
int getVars()
int getClauses()
void newVar(int howmany)
void addClause(int[] clause)
void addClauses(int[][] clauses)
void addAssumptions(int[] assumptions)
int solve(int[] assumptions)
void addBlockingClause()
void addBlockingClause(int[] clause)
int addPB(int[] weights, int[] literals, int k, boolean isgeq)
int addPBWithAssumption(int[] weights, int[] literals, int k, boolean isgeq, int assumption)
int addAtMost(int[] literals, int k)
int addAtMostWithAssumption(int[] literals, int k, int assumption)
int addAtLeast(int[] literals, int k)
int addAtLeastWithAssumption(int[] literals, int k, int assumption)
int addExactly(int[] literals, int k)
int addExactlyWithAssumption(int[] literals, int k, int assumption)
void setFrozen(int lit)
boolean isEliminated(int lit)
java.util.BitSet getModel()
int[] getIntModel()
int[] getFailed(int[] literals)
void outputModel()
double getTime()
void addNormalizedClause(int[] clause)
void done()
void setVars(int count)
int[] getMUS()