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

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

# Mers::Solvers::SAT::GATSAT::GATSAT Class Reference

`#include <GATSAT.h>`

Inheritance diagram for Mers::Solvers::SAT::GATSAT::GATSAT:

[legend]
Collaboration diagram for Mers::Solvers::SAT::GATSAT::GATSAT:

[legend]
List of all members.

## Public Member Functions
| GATSAT ()
| GATSAT (Mers::Generators::AssignmentGeneratorInterface *myGenerator, Mers::Solvers::SAT::AssignmentTesterInterface *myTester)
virtual | ~GATSAT ()
virtual Mers::Models::Base::BaseModelClause * | findSatisfyingSolution (int maximumVisitedStateCount, int maxSize)
virtual Mers::Models::Base::BaseModelClause * | findUnsatisfyingSolution (int maximumVisitedStateCount, int maxSize)
virtual void | setDebug (unsigned int state)
virtual void | printStatistics () const
virtual Mers::Generators::AssignmentGeneratorInterface * | getGenerator ()
virtual Mers::Solvers::SAT::AssignmentTesterInterface * | getTester ()
## Protected Attributes
Mers::Generators::AssignmentGeneratorInterface * | generator
| the generator being used by this sat engine.
Mers::Solvers::SAT::AssignmentTesterInterface * | tester
| the tester being used by this sat engine.

## Detailed Description

GATSAT defines a default SAT engine interface for an engine that uses generate and test methods.

Author:
  Paul H. Elliott

Definition at line 44 of file GATSAT.h.

## Constructor & Destructor Documentation

GATSAT::GATSAT | ( |  | ) |

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 33 of file GATSAT.cpp.

References generator, and tester.

GATSAT::GATSAT | ( | Mers::Generators::AssignmentGeneratorInterface * | myGenerator,
|  | Mers::Solvers::SAT::AssignmentTesterInterface * | myTester |
| ) |  |  |

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 41 of file GATSAT.cpp.

References generator, and tester.

GATSAT::~GATSAT | ( |  | ) | `[virtual]`

Destroys the sat engine.

Definition at line 50 of file GATSAT.cpp.

References generator, and tester.

## Member Function Documentation

BaseModelClause * GATSAT::findSatisfyingSolution | ( | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[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.

Implements Mers::Solvers::SAT::SATInterface.

Definition at line 60 of file GATSAT.cpp.

References Mers::Generators::AssignmentGeneratorInterface::addConflict(), Mers::Generators::AssignmentGeneratorInterface::generateBestImplicant(), generator, Mers::Generators::AssignmentGeneratorInterface::getFullAssignmentSize(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Generators::AssignmentGeneratorInterface::markBestFeasible(), tester, and Mers::Solvers::SAT::AssignmentTesterInterface::tryAssignment().

Referenced by Mers::Solvers::Entailment::GI::GoalInterpreter::generateGoalState(), and Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::testGATSAT().

Here is the call graph for this function:

BaseModelClause * GATSAT::findUnsatisfyingSolution | ( | int | maximumVisitedStateCount,
|  | int | maxSize |
| ) |  |  | `[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.

Implements Mers::Solvers::SAT::SATInterface.

Definition at line 136 of file GATSAT.cpp.

References Mers::Generators::AssignmentGeneratorInterface::addConflict(), Mers::Generators::AssignmentGeneratorInterface::generateBestImplicant(), generator, Mers::Utils::Containers::DynamicArray::getLength(), Mers::Generators::AssignmentGeneratorInterface::markBestFeasible(), Mers::Utils::Containers::DynamicArray::printArray(), tester, and Mers::Solvers::SAT::AssignmentTesterInterface::tryAssignment().

Referenced by Mers::Solvers::Entailment::GI::GoalInterpreter::generateGoalState(), and Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::testGATSAT().

Here is the call graph for this function:

void GATSAT::setDebug | ( | unsigned int | state | ) | `[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 from Mers::Solvers::SAT::SATInterface.

Definition at line 234 of file GATSAT.cpp.

References Mers::Solvers::SAT::SATInterface::debug, generator, Mers::Solvers::SAT::AssignmentTesterInterface::setDebug(), Mers::Generators::AssignmentGeneratorInterface::setDebug(), and tester.

Referenced by Mers::Solvers::Entailment::GI::GoalInterpreter::setDebug().

Here is the call graph for this function:

void GATSAT::printStatistics | ( |  | ) | const`[virtual]`

Prints the current statistics of the sat search.

Definition at line 245 of file GATSAT.cpp.

References generator, Mers::Solvers::SAT::AssignmentTesterInterface::printStatistics(), Mers::Generators::AssignmentGeneratorInterface::printStatistics(), and tester.

Here is the call graph for this function:

AssignmentGeneratorInterface * GATSAT::getGenerator | ( |  | ) | `[virtual]`

Returns the generator for this SAT engine.

Definition at line 255 of file GATSAT.cpp.

References generator.

Referenced by Mers::Solvers::Entailment::GI::GoalInterpreter::generateGoalState(), and Mers::Solvers::Entailment::GI::GoalInterpreter::updateReachableStates().

AssignmentTesterInterface * GATSAT::getTester | ( |  | ) | `[virtual]`

Returns the tester for this SAT engine.

Definition at line 262 of file GATSAT.cpp.

References tester.

Referenced by Mers::Solvers::SAT::GATSAT::unit_tests::GatsatTester::testGATSAT().

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

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