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

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

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

`#include <Opsat.h>`

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

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

[legend]
List of all members.

## Public Types
typedef Mers::Utils::Containers::DynamicArrayTemplate< Mers::Models::Base::BaseModelSentence const > | GuardArray
## Public Member Functions
| Opsat (Mers::Models::Base::BaseModelVariableArray const &designVariables, Mers::Generators::BFIG::BFIGObjectiveFunction const *ocspObjectiveFunction, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll=true, double cutoffCost=1e10)
| Opsat (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, bool use_dpll, double cutoffCost)
| Opsat (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, bool use_dpll=true)
| Opsat (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll, double cutoffCost)
| Opsat (Mers::Models::CCA::CCAVariables const &designVariables, Mers::Models::CCA::CCAModel const &model, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll=true)
| Opsat (Mers::Models::Base::BaseModelVariableArray const &designVariables, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll, double cutoffCost)
| Opsat (Mers::Models::Base::BaseModelVariableArray const &designVariables, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll=true)
| Opsat (Mers::Models::Base::BaseModelVariableArray const &variableSet, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelSentence const &constraintSet, double cutoffCost)
| Opsat (Mers::Models::Base::BaseModelVariableArray const &variableSet, Mers::Utils::Containers::IntegerArray const &valueMap, std::vector< double > const &designVarProbs, Mers::Models::Base::BaseModelSentence const &constraintSet)
| Opsat (Mers::Generators::AssignmentGeneratorInterface *myGenerator, Mers::Models::Base::BaseModelVariableArray const &searchVariables, Mers::Models::Base::BaseModelVariableArray const &allVariables, Mers::Models::Base::BaseModelSentence const &constraintSet, bool use_dpll=true)
| ~Opsat ()
void | setTemporaryConstraint (Mers::Models::Base::BaseModelClause const *c)
void | constrainByReachability ()
void | constrainByNextState ()
void | clearTemporaryConstraint ()
void | addConstraint (Mers::Models::Base::BaseModelClause const *c)
void | skipExpanding (bool doSkip)
## Protected Member Functions
void | testTheory ()
## Friends
std::ostream & | operator<< (std::ostream &out, Opsat const &other)

## Detailed Description

This class represents the toplevel interface to the OpSAT reasoning engine. OpSAT is an acronym for: Optimal Propositional SATisfiability.

It produces, in best first order, solutions to problems represented as propositional constraints (the theory).

Definition at line 62 of file Opsat.h.

## Constructor & Destructor Documentation

Opsat::Opsat | ( | Mers::Models::Base::BaseModelVariableArray const & | designVariables,
|  | Mers::Generators::BFIG::BFIGObjectiveFunction const * | ocspObjectiveFunction,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll = `true`,
|  | double | cutoffCost = `1e10` |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | ocspObjectiveFunction | the OCSP objective function to be used with BFIG to enumerate the solutions to the OCSP in best-first order.
  | allVariables | the set of all variables in the model and constraint set.
  | constraintSet | The set of constraints to use with ISAT.
  | use_dpll | true if it should use DPLL.
  | cutoffCost | The cost above which candidates are no longer considered.

Definition at line 63 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Opsat::Opsat | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | bool | use_dpll,
|  | double | cutoffCost |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with Opsat. Opsat will extract the constraints and the probability model from this model and use them to create ISAT and BFIG.
  | use_dpll | true if it should use DPLL.
  | ord | The ordering that BFIG should use when deciding which variables to use next.
  | cutoffCost | The cost above which candidates are no longer considered.

Definition at line 82 of file Opsat-for-zchaff.cpp.

References Mers::Models::CCA::CCAModel::get_all_constraints(), Mers::Models::CCA::CCAModel::get_variables_p(), Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Opsat::Opsat | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | bool | use_dpll = `true` |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with Opsat. Opsat will extract the constraints and the probability model from this model and use them to create ISAT and BFIG.
  | use_dpll | true if it should use DPLL.
  | ord | The ordering that BFIG should use when deciding which variables to use next.

Definition at line 101 of file Opsat-for-zchaff.cpp.

References Mers::Models::CCA::CCAModel::get_all_constraints(), Mers::Models::CCA::CCAModel::get_variables_p(), Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Opsat::Opsat | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll,
|  | double | cutoffCost |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with Opsat. Opsat will extract the probability model from this model and use it to create BFIG.
  | constraintSet | The set of constraints to use with ISAT.
  | use_dpll | true if it should use DPLL.
  | ord | The ordering that BFIG should use when deciding which variables to use next.
  | cutoffCost | The cost above which candidates are no longer considered.

Definition at line 120 of file Opsat-for-zchaff.cpp.

References Mers::Models::CCA::CCAModel::get_variables_p(), Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Opsat::Opsat | ( | Mers::Models::CCA::CCAVariables const & | designVariables,
|  | Mers::Models::CCA::CCAModel const & | model,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll = `true` |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | designVariables | These are the variables that will be generated over and returned as solutions. The solutions are projected onto these variables.
  | model | The CCA model being used with Opsat. Opsat will extract the probability model from this model and use it to create BFIG.
  | constraintSet | The set of constraints to use with ISAT.
  | use_dpll | true if it should use DPLL.
  | ord | The ordering that BFIG should use when deciding which variables to use next.

Definition at line 138 of file Opsat-for-zchaff.cpp.

References Mers::Models::CCA::CCAModel::get_variables_p(), Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::Opsat | ( | Mers::Models::Base::BaseModelVariableArray const & | designVariables,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll,
|  | double | cutoffCost |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | cutoffCost | The cost above which candidates are no longer considered.

Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::Opsat | ( | Mers::Models::Base::BaseModelVariableArray const & | designVariables,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll = `true` |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::Opsat | ( | Mers::Models::Base::BaseModelVariableArray const & | variableSet,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | double | cutoffCost |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Parameters:

  | cutoffCost | The cost above which candidates are no longer considered.

Mers::Solvers::SAT::GATSAT::OpSAT::Opsat::Opsat | ( | Mers::Models::Base::BaseModelVariableArray const & | variableSet,
|  | Mers::Utils::Containers::IntegerArray const & | valueMap,
|  | std::vector< double > const & | designVarProbs,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet |
| ) |  |  |

Creates a new Opsat object using the ISAT and BFIG components.

Opsat::Opsat | ( | Mers::Generators::AssignmentGeneratorInterface * | myGenerator,
|  | Mers::Models::Base::BaseModelVariableArray const & | searchVariables,
|  | Mers::Models::Base::BaseModelVariableArray const & | allVariables,
|  | Mers::Models::Base::BaseModelSentence const & | constraintSet,
|  | bool | use_dpll = `true` |
| ) |  |  |

Creates an new opsat object using ISAT and the supplied generator.

Parameters:

  | myGenerator | the assignment generator to be used by this opsat engine.
  | searchVariables | the set of all variables in the model that are being searched over.
  | allVariables | the set of all variables in the model and constraint set.
  | constraintSet | the set of all SAT constraints that describe the system
  | use_dpll | true if it should use DPLL

Definition at line 258 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::SATInterface::debug, Mers::Solvers::SAT::GATSAT::GATSAT::generator, Mers::Solvers::SAT::ISAT::ISATTester::setDPLLFlag(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

## Member Function Documentation

void Opsat::setTemporaryConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) |

This method is used to specify the current temporary constraint. Temporary constraints are those which are not expected to persist throughout the life of the engine. For example, an anti-goal may be asserted as a temporary constraint.

Caution should be exercised when modifying temporary constraints, as doing so may disrupt the support tree for other clauses or other cached data. This in turn may lead to inefficiency.

Parameters:

  | c | The temporary constraint to set.

Definition at line 292 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::setTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

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

Here is the call graph for this function:

void Opsat::constrainByReachability | ( |  | ) |

Calling this method causes the engine to produce temporary constraints prohibiting assigments that are not reachable from the current state.

In this context, I believe "reachable" really refers to "reachable via an explicit command". In other words, fault transitions or transitions whose guard clause contains observations would technically not be reachable.

WARNING: This method should not be called twice in succession, as it will introduce redundant constraints.

Definition at line 311 of file Opsat-for-zchaff.cpp.

void Opsat::constrainByNextState | ( |  | ) |

This method is a direct pass through to VSAT::constrainByNextValue(). It is used to specify the value of a variable in the "next" state (e.g. for observations, whose "next" value is known).

Definition at line 319 of file Opsat-for-zchaff.cpp.

void Opsat::clearTemporaryConstraint | ( |  | ) |

Invoking this method clears/removes the temporary constraint. See the comment for setTemporaryConstraint() with regard to efficiency.

Definition at line 327 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::clearTemporaryConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

void Opsat::addConstraint | ( | Mers::Models::Base::BaseModelClause const * | c | ) |

Inserts a new (non-temporary) constraint into the theory. A wrapper around VSAT::addConstraint().

Parameters:

  | c | The constraint to add

Definition at line 301 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::AssignmentTesterInterface::addConstraint(), and Mers::Solvers::SAT::GATSAT::GATSAT::tester.

Here is the call graph for this function:

void Opsat::testTheory | ( |  | ) | `[protected]`

Tests the theory to see if it's consistent.

Definition at line 334 of file Opsat-for-zchaff.cpp.

References Mers::Solvers::SAT::GATSAT::GATSAT::tester, and Mers::Solvers::SAT::AssignmentTesterInterface::tryAssignment().

Here is the call graph for this function:

## Friends And Related Function Documentation

std::ostream& operator<< | ( | std::ostream & | out,
|  | Opsat const & | other |
| ) |  |  | `[friend]`

Prints out the current state of opsat.

Parameters:

  | out | the ostream being written to.
  | other | The opsat being printed.

Returns:
  the out ostream.

Definition at line 358 of file Opsat-for-zchaff.cpp.

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

- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat.h
- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat-for-zchaff.cpp
- /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/OpSAT/Opsat.cpp