public class SatSolverForNative extends ISatLibrary implements ISatSolver
修飾子とタイプ | クラスと説明 |
---|---|
static interface |
SatSolverForNative.ICallback |
class |
SatSolverForNative.UserCallback |
ISatLibrary.IPASIR, ISatLibrary.ISATLIB
コンストラクタと説明 |
---|
SatSolverForNative(java.lang.String name) |
修飾子とタイプ | メソッドと説明 |
---|---|
void |
add_a_clause(int[] clause)
Adds a clause to SAT solver.
|
void |
add(int lit_or_zero)
Adds a literal to SAT solver or finalizes the clause with a "0".
|
void |
addAssumptions(int[] literals)
Adds assumption literals to SAT solver.
|
int |
addAtLeast(int[] literals,
int k)
Adds an at least k constraint to SAT solver.
|
int |
addAtLeastWithAssumption(int[] literals,
int k,
int assumption)
Adds an at least k constraint to SAT solver as a relaxed constraint.
|
int |
addAtMost(int[] literals,
int k)
Adds an at most k constraint to SAT solver.
|
int |
addAtMostWithAssumption(int[] literals,
int k,
int assumption)
Adds an at most k constraint to SAT solver as a relaxed constraint.
|
void |
addBlockingClause()
Adds a blocking clause to SAT solver.
|
void |
addBlockingClause(int[] clause)
Adds a blocking clause to SAT solver.
|
void |
addClause(int[] clause)
Adds a clause to SAT solver.
|
void |
addClauses(int[][] clauses)
Adds clauses to SAT solver.
|
int |
addExactly(int[] literals,
int k)
Adds an exact k constraint to SAT solver.
|
int |
addExactlyWithAssumption(int[] literals,
int k,
int assumption)
Adds an exact k constraint to SAT solver as a relaxed constraint.
|
void |
addNormalizedClause(int[] lits)
Adds multiple clauses to SAT solver at a time.
|
int |
addPB(int[] weights,
int[] literals,
int k,
boolean isgeq)
Adds a pseudo boolean constraint to SAT solver.
|
int |
addPBWithAssumption(int[] weights,
int[] literals,
int k,
boolean isgeq,
int assumption)
Adds a pseudo boolean constraint to SAT solver.
|
void |
assume(int lit)
Adds an assumption.
|
void |
done()
Adds rest clauses in buffer to SAT solver.
|
int |
failed(int lit)
Checks if the given assumption was used to prove UNSAT in the last search.
|
int[] |
get_int_model_by_binary()
Gets SAT solution (assignments to SAT variables) by binary integer array.
|
int |
getClauses()
Gets the number of clauses in SAT solver.
|
int[] |
getFailed(int[] literals)
Get results of assumption literals if used proving unsatisfiability.
|
int[] |
getIntModel()
Gets SAT solution (assignments to SAT variables) by integer array.
|
java.util.BitSet |
getModel()
Gets SAT solution (assignments to SAT variables) by bitset.
|
int[] |
getMUS() |
java.lang.String |
getSignature()
Gets a signature of SAT solver.
|
java.lang.String |
getSolverName()
Gets a name of SAT solver.
|
double |
getTime()
Gets total time of invocation of SAT solver.
|
int |
getVars()
Gets the number of variables in SAT solver.
|
SatSolverForNative |
init()
Constructs a new SAT solver.
|
boolean |
isEliminated(int lit)
Checks if the literal is frozen.
|
int[] |
makeBuffer()
Makes an array for buffering clauses.
|
void |
newVar(int howmany) |
void |
outputModel()
Outputs SAT solution on standard output.
|
void |
release()
Releases the solver.
|
void |
setBufferSize(int size)
Sets a number of clauses added to SAT solver at a time.
|
void |
setFrozen(int lit)
Excludes a literal from the simplification of SAT solver.
|
void |
setTerminate(int value)
Sets a callback function requiring a termination of solving to the solver.
|
void |
setVars(int count) |
void |
setVerbosity(int verbosity)
Sets the verbosity of SAT solver's output.
|
int |
solve()
Solves a SAT problem.
|
int |
solve(int[] assumptions)
Solves a SAT problem with assumption.
|
int |
val(int lit)
Gets the truth value of the given literal in the assignment.
|
public java.lang.String getSignature()
getSignature
インタフェース内 ISatSolver
public SatSolverForNative init()
init
インタフェース内 ISatSolver
public void release()
release
インタフェース内 ISatSolver
public void add(int lit_or_zero)
add
インタフェース内 ISatSolver
lit_or_zero
- a literal or "0"public void assume(int lit)
assume
インタフェース内 ISatSolver
lit
- the assumptionpublic int solve()
solve
インタフェース内 ISatSolver
public int val(int lit)
val
インタフェース内 ISatSolver
lit
- the literalpublic int failed(int lit)
failed
インタフェース内 ISatSolver
lit
- the assumption literalpublic void setTerminate(int value)
setTerminate
インタフェース内 ISatSolver
value
- if nonzero, set terminationpublic void setBufferSize(int size)
size
- the number of clauses added to SAT solver at a timepublic int[] makeBuffer()
public void setVerbosity(int verbosity)
setVerbosity
インタフェース内 ISatSolver
verbosity
- the verbosity of SAT solver's outputpublic 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 add_a_clause(int[] clause)
clause
- a clause to add to SAT solverpublic void addNormalizedClause(int[] lits)
addNormalizedClause
インタフェース内 ISatSolver
lits
- array of literalspublic void addClause(int[] clause)
addClause
インタフェース内 ISatSolver
clause
- clause to add to SAT solverpublic void addClauses(int[][] clauses)
addClauses
インタフェース内 ISatSolver
clauses
- clauses to add to SAT solverpublic void addAssumptions(int[] literals)
addAssumptions
インタフェース内 ISatSolver
literals
- literals to be assumptionpublic void done()
done
インタフェース内 ISatSolver
public int solve(int[] assumptions)
solve
インタフェース内 ISatSolver
assumptions
- assumptionpublic void addBlockingClause(int[] clause)
addBlockingClause
インタフェース内 ISatSolver
clause
- the clause required to blockpublic void addBlockingClause()
addBlockingClause
インタフェース内 ISatSolver
public int addPB(int[] weights, int[] literals, int k, boolean isgeq)
addPB
インタフェース内 ISatSolver
weights
- each coefficient of literalsliterals
- literalsk
- integer of right side of PB constraintisgeq
- true if added constraint is [... greater than or equal to k], false otherwisepublic int addPBWithAssumption(int[] weights, int[] literals, int k, boolean isgeq, int assumption)
addPBWithAssumption
インタフェース内 ISatSolver
weights
- each coefficient of literalsliterals
- literalsk
- integer of right side of PB constraintisgeq
- true if added constraint is [... greater than or equal to k], false otherwisepublic int addAtMost(int[] literals, int k)
addAtMost
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic int addAtMostWithAssumption(int[] literals, int k, int assumption)
addAtMostWithAssumption
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic int addAtLeast(int[] literals, int k)
addAtLeast
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic int addAtLeastWithAssumption(int[] literals, int k, int assumption)
addAtLeastWithAssumption
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic int addExactly(int[] literals, int k)
addExactly
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic int addExactlyWithAssumption(int[] literals, int k, int assumption)
addExactlyWithAssumption
インタフェース内 ISatSolver
literals
- literalsk
- integer of right side of at least constraintpublic void setFrozen(int lit)
setFrozen
インタフェース内 ISatSolver
lit
- the literal required to freezepublic boolean isEliminated(int lit)
isEliminated
インタフェース内 ISatSolver
lit
- the literal required to check if frozenpublic java.util.BitSet getModel()
getModel
インタフェース内 ISatSolver
public int[] get_int_model_by_binary()
public int[] getIntModel()
getIntModel
インタフェース内 ISatSolver
public int[] getFailed(int[] literals)
getFailed
インタフェース内 ISatSolver
literals
- assumption literalspublic int[] getMUS()
getMUS
インタフェース内 ISatSolver
public void outputModel()
outputModel
インタフェース内 ISatSolver
public double getTime()
getTime
インタフェース内 ISatSolver
public java.lang.String getSolverName()
getSolverName
インタフェース内 ISatSolver