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

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

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

`#include <VSATNode.h>`

Collaboration diagram for Mers::Solvers::SAT::ValidSAT::VSATNode:

[legend]
List of all members.

## Public Types
enum | SolutionType { Unsatisfiable, Satisfiable, Valid, Unsatisfiable, Satisfiable, Valid, Unknown }
## Public Member Functions
| VSATNode (Mers::Utils::Containers::DynamicArrayTemplate< VSATVariable > const &myVariables, Mers::Models::Base::BaseModelSentence const &myConstraint, bool myTestForValid)
| VSATNode (VSATNode const &other)
virtual | ~VSATNode ()
void | addConstraint (Mers::Models::Base::BaseModelClause const *newConstraint)
void | propagate (Mers::Models::Base::BaseModelAssignment const &asg, bool positive, bool ignoreConstraint=true, bool unitPropagate=true)
SolutionType | getStatus ()
SolutionType | evaluate ()
double | getExpandCount ()
Mers::Models::Base::BaseModelAssignmentArray & | getUnsatAssignment ()
Mers::Models::Base::BaseModelAssignmentArray & | getValidAssignment ()
virtual void | setDebug (unsigned int state)
## Protected Member Functions
void | adjustValidAssignment ()
## Protected Attributes
Mers::Utils::Containers::DynamicArrayTemplate< Mers::Models::Base::BaseModelAssignmentArray > | domains
Mers::Utils::Containers::DynamicArrayTemplate< VSATVariable > | allVariables
| the list of all variables corresponding to all domains.
Mers::Utils::Containers::IntegerArray | unassignedVariableIndex
Mers::Utils::Containers::DynamicArrayTemplate< VSATVariable > | unassignedVariables
Mers::Models::Base::BaseModelSentence | constraints
SolutionType | solutionStatus
| the current known status of the node.
bool | notValid
double | numberOfExpandedNodes
bool | testForValid
Mers::Models::Base::BaseModelAssignmentArray | validAssignment
| The valid assignment for this node.
Mers::Models::Base::BaseModelAssignmentArray | unsatAssignment
| The unsat assignment for this node.
unsigned int | debug
| The current debug state.

## Detailed Description

A VSATNode contains information related to a single search state within the VSAT engine.

Author:
  Paul H. Elliott

Definition at line 41 of file VSATNode.h.

## Member Enumeration Documentation

enum Mers::Solvers::SAT::ValidSAT::VSATNode::SolutionType

The VSATNode Solution Status type. As it determines the status of it's search, it updates this value.

Definition at line 46 of file VSATNode.h.

## Constructor & Destructor Documentation

VSATNode::VSATNode | ( | Mers::Utils::Containers::DynamicArrayTemplate< VSATVariable > const & | myVariables,
|  | Mers::Models::Base::BaseModelSentence const & | myConstraint,
|  | bool | myTestForValid |
| ) |  |  |

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

Parameters:

  | myVariables | 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.
  | myConstraint | the constraints of the model being examined.
  | myTestForValid | set to true to test if a solution is valid, setting to false causes VSATNode to actively establish only satisfiable or unsatisfiable (A solution may still be trivially valid).

Definition at line 32 of file VSATNode.cpp.

References allVariables, constraints, domains, Mers::Utils::Containers::DynamicArray::getLength(), notValid, numberOfExpandedNodes, Mers::Models::Base::BaseModelAssignmentArray::pushBack(), Mers::Utils::Containers::DynamicArray::resize(), solutionStatus, testForValid, unassignedVariableIndex, and unassignedVariables.

Here is the call graph for this function:

VSATNode::VSATNode | ( | VSATNode const & | other | ) |

Creates a new VSATNode object with the same current configuration as the provided other VSATNode object. This makes an identical copy of the interal data structure.

Parameters:

  | other | the other object being copied as the initial contents of this object.

Definition at line 84 of file VSATNode.cpp.

References notValid, numberOfExpandedNodes, solutionStatus, and testForValid.

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

Destroys this object

Definition at line 103 of file VSATNode.cpp.

## Member Function Documentation

void VSATNode::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | newConstraint | ) |

Adds an additional constraint to this node.

Parameters:

  | newConstraint | the additional constraint being added to this node.

Definition at line 109 of file VSATNode.cpp.

References constraints, Mers::Models::Base::BaseModelClause::getClauseType(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Models::Base::BaseModelClauseArray::pushBack(), and Mers::Models::Base::BaseModelAssignmentArray::pushBack().

Referenced by Mers::Solvers::SAT::ValidSAT::ValidSAT::addConstraint(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::addTemporaryConstraint().

Here is the call graph for this function:

void VSATNode::propagate | ( | Mers::Models::Base::BaseModelAssignment const & | asg,
|  | bool | positive,
|  | bool | ignoreConstraint = `true`,
|  | bool | unitPropagate = `true` |
| ) |  |  |

Applies the specified domain restriction and unit propogates the resulting domain restriction as appropriate. The procedure terminates when either an inconsistency is discovered or when all unit clauses and domains have been propogated.

Parameters:

  | asg | the assignment either being asserted (positive = true) or being removed (positive = false).
  | positive | true if the assignment should constrain the domain of the assigned variable to the value of the assignment, or false if the value should instead be removed from the domain of the variable.
  | ignoreConstraint | if set to true, then the propogation does not set the notValid flag when reducing the domain of a design variable. This indicates that the assigned value is a normal assignment, rather than a unit propagation. When set to false, a constraint applied to a design variable will make the node not Valid, though it may still be satisfiable.
  | unitPropagate | Set to true to indicate that the routine should unit propagate when it is able to, otherwise it will wait to unit propagate until more information has been propagated. This is used to enter a group of candidates that should not be allowed to unit propagate a value of a candidate assignment to some value until after it has already been assigned its fixed value.

Definition at line 122 of file VSATNode.cpp.

References adjustValidAssignment(), allVariables, constraints, debug, domains, Mers::Utils::Containers::DynamicArray::getLength(), Mers::Models::Base::BaseModelAssignment::getValue(), Mers::Models::Base::BaseModelAssignment::getVariable(), Mers::Solvers::SAT::ValidSAT::VSATVariable::isDesignVariable(), Mers::Utils::Containers::DynamicArray::makeEmpty(), notValid, Mers::Models::Base::BaseModelAssignmentArray::popBack(), Mers::Models::Base::BaseModelClauseArray::popBack(), Mers::Models::Base::BaseModelAssignmentArray::pushBack(), Mers::Utils::Containers::DynamicArray::resize(), solutionStatus, unassignedVariableIndex, unassignedVariables, unsatAssignment, and validAssignment.

Referenced by evaluate(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

Here is the call graph for this function:

SolutionType Mers::Solvers::SAT::ValidSAT::VSATNode::getStatus | ( |  | ) | `[inline]`

Retrieves the current status of the search process which reflects what is known about the current suggested solution.

Returns:
  the current information known about the solution

Definition at line 134 of file VSATNode.h.

References solutionStatus.

Referenced by Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

VSATNode::SolutionType VSATNode::evaluate | ( |  | ) |

Determines the actual status of the chosen variable configuration, by branching on possible solutions as necessary. The current information known about the solution is updated by this evaluation, if it was not known already.

Returns:
  the current information known about the solution, which should be the evaluated solution

Definition at line 365 of file VSATNode.cpp.

References adjustValidAssignment(), allVariables, constraints, debug, evaluate(), getExpandCount(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Models::Base::BaseModelAssignment::getOperator(), getUnsatAssignment(), getValidAssignment(), Mers::Models::Base::BaseModelAssignment::getVariable(), Mers::Utils::Containers::DynamicArray::makeEmpty(), notValid, numberOfExpandedNodes, Mers::Utils::Containers::DynamicArray::printArray(), propagate(), solutionStatus, testForValid, unsatAssignment, and validAssignment.

Referenced by evaluate(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

Here is the call graph for this function:

double VSATNode::getExpandCount | ( |  | ) |

Returns the number of nodes expanded while searching for the Valid/SAT/UNSAT status.

Returns:
  the number of nodes expanded during evaluation (including this node, so always >= 1.

Definition at line 565 of file VSATNode.cpp.

References numberOfExpandedNodes.

Referenced by evaluate(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

BaseModelAssignmentArray & VSATNode::getUnsatAssignment | ( |  | ) |

Returns the current unsat conflict, which is the current valid solution.

Returns:
  The current conflict.

Definition at line 572 of file VSATNode.cpp.

References unsatAssignment.

Referenced by evaluate(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

BaseModelAssignmentArray & VSATNode::getValidAssignment | ( |  | ) |

Returns the current valid conflict, which is the current unsat solution.

Returns:
  The current conflict.

Definition at line 579 of file VSATNode.cpp.

References validAssignment.

Referenced by evaluate(), and Mers::Solvers::SAT::ValidSAT::ValidSAT::tryAssignment().

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

Sets the debug state of this branch of testing the solution.

Parameters:

  | state | the new debug state for this node.

Definition at line 181 of file VSATNode.h.

References debug.

Referenced by Mers::Solvers::SAT::ValidSAT::ValidSAT::setDebug().

void VSATNode::adjustValidAssignment | ( |  | ) | `[protected]`

Adjusts the validAssignment so it correctly corresponds to the actual validAssignment for this node based on those domains that were constrained.

Definition at line 586 of file VSATNode.cpp.

References domains, Mers::Solvers::SAT::ValidSAT::VSATVariable::getAssignments(), Mers::Utils::Containers::DynamicArray::getLength(), Mers::Solvers::SAT::ValidSAT::VSATVariable::getUID(), Mers::Models::Base::BaseModelAssignmentArray::pushBack(), unassignedVariables, and validAssignment.

Referenced by evaluate(), and propagate().

Here is the call graph for this function:

## Member Data Documentation

Mers::Utils::Containers::DynamicArrayTemplate<Mers::Models::Base::BaseModelAssignmentArray> Mers::Solvers::SAT::ValidSAT::VSATNode::domains`[protected]`

the list of all possible domain assignments still available.

Definition at line 197 of file VSATNode.h.

Referenced by adjustValidAssignment(), propagate(), and VSATNode().

Mers::Utils::Containers::IntegerArray Mers::Solvers::SAT::ValidSAT::VSATNode::unassignedVariableIndex`[protected]`

index mapping from allVariables to unassignedVariables (UID -> unassigned var Index).

Definition at line 204 of file VSATNode.h.

Referenced by propagate(), and VSATNode().

Mers::Utils::Containers::DynamicArrayTemplate<VSATVariable> Mers::Solvers::SAT::ValidSAT::VSATNode::unassignedVariables`[protected]`

the list of unassigned variables (a variable is unassigned so long as it has not been unit propogated/assigned a value).

Definition at line 209 of file VSATNode.h.

Referenced by adjustValidAssignment(), propagate(), and VSATNode().

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

the constraints imposed by the model that have not already been satisfied.

Definition at line 213 of file VSATNode.h.

Referenced by addConstraint(), evaluate(), propagate(), and VSATNode().

bool Mers::Solvers::SAT::ValidSAT::VSATNode::notValid`[protected]`

set to true if the domain of some design variable was constrainted. The solutionStatus will not be Valid if this flag is set.

Definition at line 221 of file VSATNode.h.

Referenced by evaluate(), propagate(), and VSATNode().

double Mers::Solvers::SAT::ValidSAT::VSATNode::numberOfExpandedNodes`[protected]`

the number of nodes expanded to determine the status of this node.

Definition at line 225 of file VSATNode.h.

Referenced by evaluate(), getExpandCount(), and VSATNode().

bool Mers::Solvers::SAT::ValidSAT::VSATNode::testForValid`[protected]`

true if we're testing for Valid, false if we're just testing for sat/unsat.

Definition at line 229 of file VSATNode.h.

Referenced by evaluate(), and VSATNode().

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

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