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

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

# Mers::Solvers::SAT::ValidSAT::ValidSAT Class Reference

`#include <ValidSAT.h>`

Inheritance diagram for Mers::Solvers::SAT::ValidSAT::ValidSAT:

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

[legend]
List of all members.

## Public Member Functions
virtual void | addConstraint (Mers::Models::Base::BaseModelClause const *constraint)
virtual void | addTemporaryConstraint (Mers::Models::Base::BaseModelClause const *constraint)
virtual void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *constraint)
virtual void | clearTemporaryConstraint ()
| ValidSAT (Mers::Models::Base::BaseModelVariableArray const &myAllVariables, Mers::Models::Base::BaseModelVariableArray const &myDecisionVariables, Mers::Models::Base::BaseModelSentence const &myConstraint, bool myTestForValid=true)
virtual | ~ValidSAT ()
virtual SolutionType | tryAssignment (Mers::Models::Base::BaseModelAssignmentArray const *candidate, int group, bool satisfy, Mers::Models::Base::BaseModelAssignmentArray &conflict)
void | printStatistics (bool verbose=false) const
virtual void | setDebug (unsigned int state)
virtual double | getNumberOfSteps () const
## Protected Attributes
Mers::Models::Base::BaseModelSentence | constraint
Mers::Utils::Containers::DynamicArrayTemplate< VSATVariable > | variables
| the list of all variables and their associated domains.
VSATNode * | modelNode
VSATNode * | activeNode
double | numberOfExpandedNodes
unsigned int | validTests
unsigned int | satisfiableTests
unsigned int | unsatisfiableTests
bool | testForValid

## Detailed Description

A ValidSAT object which Tests solutions against a model for their validity (valid, satisfiable, or unsatisfiable)

Author:
  Paul H. Elliott

Definition at line 47 of file ValidSAT.h.

## Constructor & Destructor Documentation

ValidSAT::ValidSAT | ( | Mers::Models::Base::BaseModelVariableArray const & | myAllVariables,
|  | Mers::Models::Base::BaseModelVariableArray const & | myDecisionVariables,
|  | Mers::Models::Base::BaseModelSentence const & | myConstraint,
|  | bool | myTestForValid = `true` |
| ) |  |  |

Creates a new ValidSAT object with the initial model specified by the variables and constraints.

Parameters:

  | myAllVariables | all of the variables used in the constraints of the model. Note that all variables in the constraints must be present in the variable listing but not all variables in myVariables must be present in myConstraint. Also note that this list should be in UID ordering (sorted, with no gaps).
  | myDecisionVariables | a listing of all decision variables. (variables being searched over) This list will be used to restrict extension validity to those variables that are being extended.
  | myConstraint | the constraints of the model being examined.
  | myTestForValid | set to true to test if a solution is valid, setting to false causes ValidSAT to actively establish only satisfiable or unsatisfiable (A solution may still be trivially valid).

Definition at line 32 of file ValidSAT.cpp.

References activeNode, constraint, Mers::Utils::Containers::DynamicArray::getLength(), modelNode, numberOfExpandedNodes, satisfiableTests, testForValid, unsatisfiableTests, validTests, and variables.

Here is the call graph for this function:

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

Deletes this engine and all it's components.

Definition at line 62 of file ValidSAT.cpp.

References activeNode, modelNode, and variables.

## Member Function Documentation

void ValidSAT::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[virtual]`

Adds an additional temporary constraint to the current model constraints. This constraint will be included in all tests until clearTemporaryConstraint is called.

Parameters:

  | constraint | the new constraint being added to the model.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 73 of file ValidSAT.cpp.

References activeNode, Mers::Solvers::SAT::ValidSAT::VSATNode::addConstraint(), and modelNode.

Here is the call graph for this function:

void ValidSAT::addTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[virtual]`

Adds an additional temporary constraint to the current model constraints. This constraint will be included in all tests until clearTemporaryConstraint is called.

Parameters:

  | constraint | the new constraint being added to the model.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 81 of file ValidSAT.cpp.

References activeNode, and Mers::Solvers::SAT::ValidSAT::VSATNode::addConstraint().

Referenced by setTemporaryConstraint().

Here is the call graph for this function:

void ValidSAT::setTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | constraint | ) | `[virtual]`

Replaces the current temporary constraint with the new constraint. This involves a call to clearTemporaryConstraint and addTemporaryConstraint.

Parameters:

  | constraint | the new constraint that will now be the only temporary constraint.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 88 of file ValidSAT.cpp.

References addTemporaryConstraint(), and clearTemporaryConstraint().

Here is the call graph for this function:

void ValidSAT::clearTemporaryConstraint | ( |  | ) | `[virtual]`

Clears all previously set temporary constraints.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 96 of file ValidSAT.cpp.

References activeNode, and modelNode.

Referenced by setTemporaryConstraint().

ValidSAT::SolutionType ValidSAT::tryAssignment | ( | Mers::Models::Base::BaseModelAssignmentArray const * | candidate,
|  | int | group,
|  | bool | satisfy,
|  | Mers::Models::Base::BaseModelAssignmentArray & | conflict |
| ) |  |  | `[virtual]`

This tests the candidate against the model and determines if the candidate is either Unsatisfiable, Satisfiable, or Valid. The result of this test is returned.

Parameters:

  | candidate | The current candidate being tested against the model.
  | group | The UID of the search group that the candidate belongs to. The group should be 0 by default (It is provided by the Assignment Generator). Note that the tester should have either 1 group or the same number of groups as the generator.
  | satisfy | true if this is a satisfaction query, false if it is an unsatisfaction query. This will only effect the conflict returned.
  | conflict | The conflict generated by this test is returned here.

Returns:
  Valid if all extension of the candidate are valid, Unsatisfiable if no solution exists, or Satisfiable if one solution exists, but not all extensions are valid

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 105 of file ValidSAT.cpp.

References activeNode, Mers::Solvers::SAT::AssignmentTesterInterface::debug, Mers::Solvers::SAT::ValidSAT::VSATNode::evaluate(), Mers::Solvers::SAT::ValidSAT::VSATNode::getExpandCount(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Solvers::SAT::ValidSAT::VSATNode::getStatus(), Mers::Solvers::SAT::ValidSAT::VSATNode::getUnsatAssignment(), Mers::Solvers::SAT::ValidSAT::VSATNode::getValidAssignment(), numberOfExpandedNodes, Mers::Utils::Containers::DynamicArray::printArray(), Mers::Solvers::SAT::ValidSAT::VSATNode::propagate(), satisfiableTests, unsatisfiableTests, and validTests.

Here is the call graph for this function:

void ValidSAT::printStatistics | ( | bool | verbose = `false` | ) | const`[virtual]`

Prints out the performance statistics of the assignment tester.

Parameters:

  | verbose | true if detailed statistics should be printed, otherwise only a summary is printed.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 216 of file ValidSAT.cpp.

References numberOfExpandedNodes, satisfiableTests, unsatisfiableTests, and validTests.

void ValidSAT::setDebug | ( | unsigned int | state | ) | `[virtual]`

Sets the debug state of this tester.

Parameters:

  | state | the new debug state of the tester.

Reimplemented from Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 227 of file ValidSAT.cpp.

References activeNode, modelNode, Mers::Solvers::SAT::ValidSAT::VSATNode::setDebug(), and Mers::Solvers::SAT::AssignmentTesterInterface::setDebug().

Here is the call graph for this function:

virtual double Mers::Solvers::SAT::ValidSAT::ValidSAT::getNumberOfSteps | ( |  | ) | const`[inline, virtual]`

Returns the number of steps taken by this interface towards solving the problem.

Implements Mers::Solvers::SAT::AssignmentTesterInterface.

Definition at line 167 of file ValidSAT.h.

References numberOfExpandedNodes.

## Member Data Documentation

Mers::Models::Base::BaseModelSentence Mers::Solvers::SAT::ValidSAT::ValidSAT::constraint`[protected]`

the set of SAT clauses that describe the model of the system being tested against.

Definition at line 174 of file ValidSAT.h.

Referenced by ValidSAT().

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

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