ISatSolver

java.lang.Object
- iSATLibrary.ISatLibrary
- - iSATLibrary.ISatSolver

```
public class ISatSolver
extends ISatLibrary
```
This class is for using incremental SAT library API (IPASIR) and its extended API available from Java. This wraps these APIs. Use the methods of this class when using incremental SAT APIs.

作成者:

Tatsuya Sako

ネストされたクラスのサマリー
- クラスから継承されたネストされたクラス/インタフェース iSATLibrary.ISatLibrary
  ISatLibrary.IPASIR, ISatLibrary.ISATLIB

コンストラクタのサマリー

コンストラクタ
コンストラクタと説明

ISatSolver(java.lang.String name)

コンストラクタ
コンストラクタと説明
`ISatSolver(java.lang.String name)`

メソッドのサマリー

All Methods Instance Methods Concrete Methods
修飾子とタイプ	メソッドと説明
`void`	`add_a_clause(int[] clause)` Adds a clause to SAT solver.
`void`	`add_blocking_clause()` Adds a blocking clause to SAT solver.
`void`	`add_blocking_clause(int[] clause)` Adds a blocking clause to SAT solver.
`void`	`add_clause(int[] clause)` Adds a clause to SAT solver.
`void`	`addNormalizedClause(int[] lits)` Adds multiple clauses to SAT solver at a time.
`void`	`done()` Adds rest clauses in buffer to SAT solver.
`int[]`	`get_int_model()` Gets SAT solution (assignments to SAT variables) by integer array.
`java.util.BitSet`	`get_model()` Gets SAT solution (assignments to SAT variables) by bitset.
`double`	`get_solve_time()` Gets time that SAT solver used on this solving.
`java.lang.String`	`get_solver_name()` Gets a name of SAT solver.
`double`	`get_time()` Gets total time of invocation of SAT solver.
`int`	`get_vars()` Gets the number of variables in SAT solver.
`void`	`ipasir_add(int lit_or_zero)` Adds a literal to SAT solver or finarizes the clause with a "0".
`void`	`ipasir_assume(int lit)` Adds an assumption.
`int`	`ipasir_failed(int lit)` Checks if the given assumption was used to prove UNSAT in the last search.
`ISatSolver`	`ipasir_init(java.lang.String name)` Constructs a new SAT solver.
`void`	`ipasir_release()` Releases the solver.
`java.lang.String`	`ipasir_signature()` Gets a signature of SAT solver.
`int`	`ipasir_solve()` Solves a SAT problem.
`int`	`ipasir_val(int lit)` Gets the truth value of the given literal in the assignment.
`boolean`	`is_eliminated(int literal)` Checks if the literal is frozen.
`int[]`	`makeBuffer()` Makes an array for buffering clauses.
`int[]`	`model()` Gets SAT solution (assignments to SAT variables) by binary integer array.
`void`	`output_model()` Outputs SAT solution on standard output.
`void`	`set_frozen(int literal)` Excludes a literal from the simplification of SAT solver.
`void`	`set_Limit(int limit)` Sets a number of clauses added to SAT solver at a time.
`void`	`set_verbosity(int verbosity)` Sets the verbosity of SAT solver's output.
`boolean`	`solve()` Solves a SAT problem.
`boolean`	`solve(int[] assumption)` Solves a SAT problem with assumption.

クラスから継承されたメソッド java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- コンストラクタの詳細
  - ISatSolver
```
public ISatSolver(java.lang.String name)
```
- メソッドの詳細
  - ipasir_signature
```
public java.lang.String ipasir_signature()
```
    Gets a signature of SAT solver.
    
    戻り値:
    
    the signature of SAT solver
  - ipasir_init
```
public ISatSolver ipasir_init(java.lang.String name)
```
    Constructs a new SAT solver.
    
    パラメータ:
    
    name - the name of SAT solver
    
    戻り値:
    
    solver's object
  - ipasir_release
```
public void ipasir_release()
```
    Releases the solver.
  - ipasir_add
```
public void ipasir_add(int lit_or_zero)
```
    Adds a literal to SAT solver or finarizes the clause with a "0".
    
    パラメータ:
    
    lit_or_zero - a literal or "0"
  - ipasir_assume
```
public void ipasir_assume(int lit)
```
    Adds an assumption.
    
    パラメータ:
    
    lit - the assumption
  - ipasir_solve
```
public int ipasir_solve()
```
    Solves a SAT problem.
    
    戻り値:
    
    true (if the problem is SAT), false (UNSAT).
  - ipasir_val
```
public int ipasir_val(int lit)
```
    Gets the truth value of the given literal in the assignment.
    
    パラメータ:
    
    lit - the literal
    
    戻り値:
    
    the truth value of the given literal
  - ipasir_failed
```
public int ipasir_failed(int lit)
```
    Checks if the given assumption was used to prove UNSAT in the last search.
    
    パラメータ:
    
    lit - the assumption literal
    
    戻り値:
    
    1 (used), 0 (otherwise)
  - set_Limit
```
public void set_Limit(int limit)
```
    Sets a number of clauses added to SAT solver at a time. Default value : 1000
    
    パラメータ:
    
    limit - the number of clauses added to SAT solver at a time
  - makeBuffer
```
public int[] makeBuffer()
```
    Makes an array for buffering clauses. This method appends a new clause to the end of the buffer.
    
    戻り値:
    
    appended buffer
  - set_verbosity
```
public void set_verbosity(int verbosity)
```
    Sets the verbosity of SAT solver's output. If you set "0", solver's output isn't displayed.
    
    パラメータ:
    
    verbosity - the verbosity of SAT solver's output
  - get_vars
```
public int get_vars()
```
    Gets the number of variables in SAT solver.
    
    戻り値:
    
    number of variables
  - add_a_clause
```
public void add_a_clause(int[] clause)
```
    Adds a clause to SAT solver. You must add "0" to the end of the array "clause".
    
    パラメータ:
    
    clause - clause
  - addNormalizedClause
```
public void addNormalizedClause(int[] lits)
```
    Adds multiple clauses to SAT solver at a time. Clauses are temporally buffered.
    
    パラメータ:
    
    lits - array of literals
  - add_clause
```
public void add_clause(int[] clause)
```
    Adds a clause to SAT solver.
    
    パラメータ:
    
    clause - clause
  - done
```
public void done()
```
    Adds rest clauses in buffer to SAT solver. This method is called before solving a SAT problem.
  - solve
```
public boolean solve()
```
    Solves a SAT problem.
    
    戻り値:
    
    true (if the problem is SAT), false (UNSAT).
  - solve
```
public boolean solve(int[] assumption)
```
    Solves a SAT problem with assumption.
    
    パラメータ:
    
    assumption - assumption
    
    戻り値:
    
    true (if the problem is satisfiable(SAT) ), false (otherwise).
  - add_blocking_clause
```
public void add_blocking_clause(int[] clause)
```
    Adds a blocking clause to SAT solver.
    
    パラメータ:
    
    clause - the clause required to block
  - add_blocking_clause
```
public void add_blocking_clause()
```
    Adds a blocking clause to SAT solver. This blocking clause contains all SAT variables and blocks obtained solution only.
  - set_frozen
```
public void set_frozen(int literal)
```
    Excludes a literal from the simplification of SAT solver. This method is available only when SAT solver uses simplification process. If you use the SAT solver which does "simplification", you should freeze the literal.
    
    パラメータ:
    
    literal - the literal required to freeze
  - is_eliminated
```
public boolean is_eliminated(int literal)
```
    Checks if the literal is frozen. This method is available only when SAT solver uses simplification process.
    
    パラメータ:
    
    literal - the literal required to check if frozen
    
    戻り値:
    
    true (if the literal is frozen), false (otherwise)
  - get_model
```
public java.util.BitSet get_model()
```
    Gets SAT solution (assignments to SAT variables) by bitset. If you need to decode to CSP solution by Sugar, you should use this method.
    
    戻り値:
    
    the model of solution by bitset
  - model
```
public int[] model()
```
    Gets SAT solution (assignments to SAT variables) by binary integer array.
    
    戻り値:
    
    the model of solution by binary integer array (true:1, false:0)
  - get_int_model
```
public int[] get_int_model()
```
    Gets SAT solution (assignments to SAT variables) by integer array.
    
    戻り値:
    
    the model of solution by integer array
  - output_model
```
public void output_model()
```
    Outputs SAT solution on standard output.
  - get_solve_time
```
public double get_solve_time()
```
    Gets time that SAT solver used on this solving.
    
    戻り値:
    
    solving time
  - get_time
```
public double get_time()
```
    Gets total time of invocation of SAT solver.
    
    戻り値:
    
    elapsed time
  - get_solver_name
```
public java.lang.String get_solver_name()
```
    Gets a name of SAT solver.
    
    戻り値:
    
    the name of SAT solver

クラス ISatSolver

ネストされたクラスのサマリー

クラスから継承されたネストされたクラス/インタフェース iSATLibrary.ISatLibrary

コンストラクタのサマリー

メソッドのサマリー

クラスから継承されたメソッド java.lang.Object

コンストラクタの詳細

ISatSolver

メソッドの詳細

ipasir_signature

ipasir_init

ipasir_release

ipasir_add

ipasir_assume

ipasir_solve

ipasir_val

ipasir_failed

set_Limit

makeBuffer

set_verbosity

get_vars

add_a_clause

addNormalizedClause

add_clause

done

solve

solve

add_blocking_clause

add_blocking_clause

set_frozen

is_eliminated

get_model

model

get_int_model

output_model

get_solve_time

get_time

get_solver_name