public class SatSolverForSat4j extends java.lang.Object implements ISatSolver
修飾子とタイプ | フィールドと説明 |
---|---|
static int |
buffer |
static int |
cIndex |
static boolean |
isParamClause |
boolean |
isusc |
コンストラクタと説明 |
---|
SatSolverForSat4j() |
修飾子とタイプ | メソッドと説明 |
---|---|
void |
add(int lit_or_zero) |
void |
addAssumptions(int[] lits) |
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 |
saveClause(int[] clause) |
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) |
public static int cIndex
public boolean isusc
public static boolean isParamClause
public static int buffer
public java.lang.String getSignature()
getSignature
インタフェース内 ISatSolver
public ISatSolver init()
init
インタフェース内 ISatSolver
public void release()
release
インタフェース内 ISatSolver
public void add(int lit_or_zero)
add
インタフェース内 ISatSolver
public void assume(int lit)
assume
インタフェース内 ISatSolver
public int solve()
solve
インタフェース内 ISatSolver
public int val(int lit)
val
インタフェース内 ISatSolver
public int failed(int lit)
failed
インタフェース内 ISatSolver
public void setTerminate(int value)
setTerminate
インタフェース内 ISatSolver
public java.lang.String getSolverName()
getSolverName
インタフェース内 ISatSolver
public void setVerbosity(int verbosity)
setVerbosity
インタフェース内 ISatSolver
public void setVars(int count)
setVars
インタフェース内 ISatSolver
public int getVars()
getVars
インタフェース内 ISatSolver
public int getClauses()
getClauses
インタフェース内 ISatSolver
public void newVar(int howmany)
newVar
インタフェース内 ISatSolver
public void saveClause(int[] clause)
public void addClause(int[] clause)
addClause
インタフェース内 ISatSolver
public void addClauses(int[][] clauses)
addClauses
インタフェース内 ISatSolver
public void addAssumptions(int[] lits)
addAssumptions
インタフェース内 ISatSolver
public int solve(int[] assumptions)
solve
インタフェース内 ISatSolver
public void addBlockingClause()
addBlockingClause
インタフェース内 ISatSolver
public void addBlockingClause(int[] clause)
addBlockingClause
インタフェース内 ISatSolver
public int addPB(int[] weights, int[] literals, int k, boolean isgeq)
addPB
インタフェース内 ISatSolver
public int addPBWithAssumption(int[] weights, int[] literals, int k, boolean isgeq, int assumption)
addPBWithAssumption
インタフェース内 ISatSolver
public int addAtMost(int[] literals, int k)
addAtMost
インタフェース内 ISatSolver
public int addAtMostWithAssumption(int[] literals, int k, int assumption)
addAtMostWithAssumption
インタフェース内 ISatSolver
public int addAtLeast(int[] literals, int k)
addAtLeast
インタフェース内 ISatSolver
public int addAtLeastWithAssumption(int[] literals, int k, int assumption)
addAtLeastWithAssumption
インタフェース内 ISatSolver
public int addExactly(int[] literals, int k)
addExactly
インタフェース内 ISatSolver
public int addExactlyWithAssumption(int[] literals, int k, int assumption)
addExactlyWithAssumption
インタフェース内 ISatSolver
public void setFrozen(int lit)
setFrozen
インタフェース内 ISatSolver
public boolean isEliminated(int lit)
isEliminated
インタフェース内 ISatSolver
public java.util.BitSet getModel()
getModel
インタフェース内 ISatSolver
public int[] getIntModel()
getIntModel
インタフェース内 ISatSolver
public int[] getFailed(int[] literals)
getFailed
インタフェース内 ISatSolver
public int[] getMUS()
getMUS
インタフェース内 ISatSolver
public void outputModel()
outputModel
インタフェース内 ISatSolver
public double getTime()
getTime
インタフェース内 ISatSolver
public void addNormalizedClause(int[] clause)
addNormalizedClause
インタフェース内 ISatSolver
public void done()
done
インタフェース内 ISatSolver