- Main Page
- Namespaces
- Classes
- Files
- Related Pages

- Alphabetical List
- Class List
- Class Hierarchy
- Class Members

# Mers::Solvers::SAT::SATInterface Class Reference

`#include <SATInterface.h>`

Inheritance diagram for Mers::Solvers::SAT::SATInterface:

[legend]
List of all members.

## Public Member Functions
virtual Mers::Models::Base::BaseModelClauseArray * | findSatisfyingSolutions (unsigned int count, int maximumVisitedStateCount, int maxSize)
virtual Mers::Models::Base::BaseModelClause * | findSatisfyingSolution (int maximumVisitedStateCount, int maxSize)=0
virtual Mers::Models::Base::BaseModelClauseArray * | findUnsatisfyingSolutions (unsigned int count, int maximumVisitedStateCount, int maxSize)
virtual Mers::Models::Base::BaseModelClause * | findUnsatisfyingSolution (int maximumVisitedStateCount, int maxSize)=0
virtual void | setDebug (unsigned int state)
## Protected Member Functions
| SATInterface ()
virtual | ~SATInterface ()
## Protected Attributes
unsigned int | debug
| true if debug printing is enabled

## Detailed Description

SATInterface defines an default SAT engine interface.

Author:
  Paul H. Elliott

Definition at line 30 of file SATInterface.h.

## Constructor & Destructor Documentation

Mers::Solvers::SAT::SATInterface::SATInterface | ( |  | ) | `[inline, protected]`

Creates a new sat engine.

Parameters:

  | myGenerator | the generator that should be used by this engine. This object assumes ownership of the generator and will destroy it upon it's own destruction.
  | myTester | the tester that should be used by this engine. This object assumes ownership of the generator and will destroy it upon it's own destruction.

Definition at line 48 of file SATInterface.h.

References debug.

virtual Mers::Solvers::SAT::SATInterface::~SATInterface | ( |  | ) | `[inline, protected, virtual]`

Destroys the sat engine.

Definition at line 60 of file SATInterface.h.

## Member Function Documentation

virtual Mers::Models::Base::BaseModelClauseArray* Mers::Solvers::SAT::SATInterface::findSatisfyingSolutions | ( | unsigned int | count,
|  | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[inline, virtual]`

Finds the count best remaining solutions that are satisfiable, or as many as are left.

Parameters:

  | count | the number of solutions to look for.
  | maximumVisitedStateCount | the maximum number of states to examine before giving up.
  | maxSize | the largest number of states that can be kept resident in memory.

Returns:
  a new list of up to count solutions. Maybe be NULL or of length zero if no other solutions exist.

Definition at line 84 of file SATInterface.h.

References debug, findSatisfyingSolution(), and Mers::Models::Base::BaseModelClauseArray::pushBack().

Here is the call graph for this function:

virtual Mers::Models::Base::BaseModelClause* Mers::Solvers::SAT::SATInterface::findSatisfyingSolution | ( | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[pure virtual]`

Finds the best remaining solution that is satisfiable, if any.

Parameters:

  | count | the number of solutions to look for.
  | maximumVisitedStateCount | the maximum number of states to examine before giving up.
  | maxSize | the largest number of states that can be kept resident in memory.

Returns:
  a new list of up to count solutions. Maybe be NULL or of length zero if no other solutions exist.

Implemented in Mers::Solvers::SAT::GATSAT::GATSAT.

Referenced by findSatisfyingSolutions().

virtual Mers::Models::Base::BaseModelClauseArray* Mers::Solvers::SAT::SATInterface::findUnsatisfyingSolutions | ( | unsigned int | count,
|  | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[inline, virtual]`

Finds the count best remaining solutions that are unsatisfiable, or as many as are left.

Parameters:

  | count | the number of solutions to look for.
  | maximumVisitedStateCount | the maximum number of states to examine before giving up.
  | maxSize | the largest number of states that can be kept resident in memory.

Returns:
  a new list of up to count solutions. Maybe be NULL or of length zero if no other solutions exist.

Definition at line 145 of file SATInterface.h.

References debug, findUnsatisfyingSolution(), and Mers::Models::Base::BaseModelClauseArray::pushBack().

Here is the call graph for this function:

virtual Mers::Models::Base::BaseModelClause* Mers::Solvers::SAT::SATInterface::findUnsatisfyingSolution | ( | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[pure virtual]`

Finds the best remaining solution that is unsatisfiable, if any.

Parameters:

  | count | the number of solutions to look for.
  | maximumVisitedStateCount | the maximum number of states to examine before giving up.
  | maxSize | the largest number of states that can be kept resident in memory.

Returns:
  a new list of up to count solutions. Maybe be NULL or of length zero if no other solutions exist.

Implemented in Mers::Solvers::SAT::GATSAT::GATSAT.

Referenced by findUnsatisfyingSolutions().

virtual void Mers::Solvers::SAT::SATInterface::setDebug | ( | unsigned int | state | ) | `[inline, virtual]`

Sets the debug level. A value of 0 turns off debugging, a value greater than zero increases the verbosity of the debug information.

Parameters:

  | state | the new debug level.

Reimplemented in Mers::Solvers::SAT::GATSAT::GATSAT.

Definition at line 198 of file SATInterface.h.

References debug.

The documentation for this class was generated from the following file:

- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/SATInterface.h