ClauseDatabaseInterface (JaCoP 4.9.0 API)

All Known Implementing Classes:

AbstractClausesDatabase, BinaryClausesDatabase, DatabasesStore, DefaultClausesDatabase, DomainClausesDatabase, LongClausesDatabase, TernaryClausesDatabase, UnaryClausesDatabase
```
public interface ClauseDatabaseInterface
```
Interface for clause databases or database stores. Any entity that contains clauses and can perform different operations on them.

Version:

4.9

Author:

Simon Cruanes and Radoslaw Szymanek

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`int`	`addClause(int[] clause, boolean isModelClause)` It adds a clause to the database.
`void`	`assertLiteral(int literal)` It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.
`void`	`backjump(int level)` Do everything needed to return to the given level.
`boolean`	`canRemove(int clauseId)` It tells if the implementation of ClausesDatabase can remove clauses or not
`void`	`removeClause(int clauseId)` It removes the clause which unique ID is @param clauseId.
`MapClause`	`resolutionWith(int clauseIndex, MapClause clause)` It returns the clause obtained by resolution between clauseIndex and clause.
`int`	`size()` size of the database
`void`	`toCNF(BufferedWriter output)` It writes the clauses of the databases in cnf format to the specified writer.

- Method Detail
  - addClause
```
int addClause(int[] clause,
              boolean isModelClause)
```
    It adds a clause to the database. This can change the state of the solver, for example if the clause is unsatisfiable in the current trail affectation, the solver will get in the conflict state.
    
    Parameters:
    
    clause - the clause to add
    
    isModelClause - defined if the clause is model clause
    
    Returns:
    
    the unique ID referring to the clause
  - assertLiteral
```
void assertLiteral(int literal)
```
    It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.
    
    Parameters:
    
    literal - the literal that is set
  - removeClause
```
void removeClause(int clauseId)
```
    It removes the clause which unique ID is @param clauseId.
    
    Parameters:
    
    clauseId - clause id
  - canRemove
```
boolean canRemove(int clauseId)
```
    It tells if the implementation of ClausesDatabase can remove clauses or not
    
    Parameters:
    
    clauseId - the unique Id of the clause
    
    Returns:
    
    true iff removal of clauses is possible
  - resolutionWith
```
MapClause resolutionWith(int clauseIndex,
                         MapClause clause)
```
    It returns the clause obtained by resolution between clauseIndex and clause. It will also modify in place the given SetClause (avoid allocating).
    
    Parameters:
    
    clauseIndex - the unique id of the clause
    
    clause - an explanation clause that is modified by resolution
    
    Returns:
    
    the clause obtained by resolution
  - backjump
```
void backjump(int level)
```
    Do everything needed to return to the given level.
    
    Parameters:
    
    level - the level to return to. Must be < solver.getCurrentLevel().
  - size
```
int size()
```
    size of the database
    
    Returns:
    
    the number of clauses in the database
  - toCNF
```
void toCNF(BufferedWriter output)
    throws IOException
```
    It writes the clauses of the databases in cnf format to the specified writer.
    
    Parameters:
    
    output - the output writer to which all the clauses will be written to.
    
    Throws:
    
    IOException - execption from java.io package

Interface ClauseDatabaseInterface

Method Summary

Method Detail

addClause

assertLiteral

removeClause

canRemove

resolutionWith

backjump

size

toCNF