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

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

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00009 // Organization:        Model-based Embedded and Robotic Systems Group
    00010 //                                      Massachusetts Institute of Technology
    00011 //
    00013
    00014 #include "ValidSAT.h"
    00015
    00016 #include <Mers/Models/Base/BaseModelVariableArray.h>
    00017
    00019
    00020 using namespace Mers::Solvers::SAT::ValidSAT;
    00021 using Mers::Models::Base::BaseModelVariableArray;
    00022 using Mers::Models::Base::BaseModelAssignmentArray;
    00023 using Mers::Models::Base::BaseModelSentence;
    00024 using Mers::Models::Base::BaseModelClause;
    00025 using std::cout;
    00026 using std::endl;
    00027
    00029 // Construction/Destruction
    00031
    00032 ValidSAT::ValidSAT(BaseModelVariableArray const &myAllVariables,
    00033         BaseModelVariableArray const &myDecisionVariables,
    00034         BaseModelSentence const &myConstraint,
    00035         bool myTestForValid)
    00036         : constraint(BaseModelSentence::CNF, true), variables(true)
    00037 {
    00038         unsigned int x, y;
    00039         for(x = 0, y = 0; x < myAllVariables.getLength(); x++){
    00040                 if(y < myDecisionVariables.getLength() &&
    00041                         myDecisionVariables[y]->getUID() == x){
    00042                         variables.pushBack(new VSATVariable(myAllVariables[x], true));
    00043                         y++;
    00044                 }else{
    00045                         variables.pushBack(new VSATVariable(myAllVariables[x], false));
    00046                 }
    00047         }
    00048
    00049         testForValid = myTestForValid;
    00050         constraint = myConstraint;
    00051         modelNode = new VSATNode(variables, constraint, testForValid);
    00052         activeNode = new VSATNode(*modelNode);
    00053         // 1 for the initial node being expanded
    00054         numberOfExpandedNodes = 1;
    00055         validTests = 0;
    00056         satisfiableTests = 0;
    00057         unsatisfiableTests = 0;
    00058 }
    00059
    00061
    00062 ValidSAT::~ValidSAT()
    00063 {
    00064         variables.makeEmpty();
    00065         if(modelNode)
    00066                 delete modelNode;
    00067         if(activeNode)
    00068                 delete activeNode;
    00069 }
    00070
    00072
    00073 void ValidSAT::addConstraint(BaseModelClause const * newConstraint)
    00074 {
    00075         modelNode->addConstraint(newConstraint);
    00076         activeNode->addConstraint(newConstraint);
    00077 }
    00078
    00080
    00081 void ValidSAT::addTemporaryConstraint(BaseModelClause const * newConstraint)
    00082 {
    00083         activeNode->addConstraint(newConstraint);
    00084 }
    00085
    00087
    00088 void ValidSAT::setTemporaryConstraint(BaseModelClause const * newConstraint)
    00089 {
    00090         clearTemporaryConstraint();
    00091         addTemporaryConstraint(newConstraint);
    00092 }
    00093
    00095
    00096 void ValidSAT::clearTemporaryConstraint()
    00097 {
    00098         delete activeNode;
    00099         activeNode = new VSATNode(*modelNode);
    00100 }
    00101
    00103
    00104 ValidSAT::SolutionType
    00105 ValidSAT::tryAssignment(BaseModelAssignmentArray const * candidate, int group,
    00106         bool satisfy, BaseModelAssignmentArray &conflict)
    00107 {
    00108         (void) group;
    00109         VSATNode searchNode(*activeNode);
    00110
    00111         if(candidate != NULL){
    00112                 unsigned int asgIter;
    00113                 for(asgIter = 0; asgIter < candidate->getLength() &&
    00114                         searchNode.getStatus() == VSATNode::Unknown; asgIter++)
    00115                 {
    00116                         if(asgIter == candidate->getLength() - 1)
    00117                                 searchNode.propagate(*((*candidate)[asgIter]), true, true, true);
    00118                         else
    00119                                 searchNode.propagate(*((*candidate)[asgIter]), true, true, false);
    00120                 }
    00121         }
    00122
    00123         switch(searchNode.getStatus()){
    00124         case VSATNode::Valid:
    00125                 validTests++;
    00126
    00127                 ConditionalDebugOut(debug >= 6,
    00128                         cout << "Valid Assignment: ";
    00129                         searchNode.getValidAssignment().printArray(cout, ", ");
    00130                         cout << endl << "Unsat Assignment: ";
    00131                         searchNode.getUnsatAssignment().printArray(cout, ", ");
    00132                         cout << endl;
    00133                 );
    00134
    00135                 return Valid;
    00136         case VSATNode::Satisfiable:
    00137                 satisfiableTests++;
    00138
    00139                 ConditionalDebugOut(debug >= 6,
    00140                         cout << "Valid Assignment: ";
    00141                         searchNode.getValidAssignment().printArray(cout, ", ");
    00142                         cout << endl << "Unsat Assignment: ";
    00143                         searchNode.getUnsatAssignment().printArray(cout, ", ");
    00144                         cout << endl;
    00145                 );
    00146
    00147                 if(satisfy)
    00148                         conflict = searchNode.getUnsatAssignment();
    00149                 else
    00150                         conflict = searchNode.getValidAssignment();
    00151
    00152                 ConditionalDebugOut(debug >= 2,
    00153                         cout << "Conflict: ";
    00154                         conflict.printArray(cout, ", ");
    00155                         cout << endl;
    00156                 );
    00157
    00158                 return Satisfiable;
    00159         case VSATNode::Unsatisfiable:
    00160                 unsatisfiableTests++;
    00161
    00162                 ConditionalDebugOut(debug >= 6,
    00163                         cout << "Valid Assignment: ";
    00164                         searchNode.getValidAssignment().printArray(cout, ", ");
    00165                         cout << endl << "Unsat Assignment: ";
    00166                         searchNode.getUnsatAssignment().printArray(cout, ", ");
    00167                         cout << endl;
    00168                 );
    00169
    00170                 return Unsatisfiable;
    00171         case VSATNode::Unknown:
    00172         default:
    00173                 {
    00174                         VSATNode::SolutionType solStatus = searchNode.evaluate();
    00175                         numberOfExpandedNodes += searchNode.getExpandCount();
    00176                         ConditionalDebugOut(debug >= 6,
    00177                                 cout << ">> VSAT Valid Assignment: ";
    00178                                 searchNode.getValidAssignment().printArray(cout, ", ");
    00179                                 cout << endl << ">> VSAT Unsat Assignment: ";
    00180                                 searchNode.getUnsatAssignment().printArray(cout, ", ");
    00181                                 cout << endl;
    00182                         );
    00183
    00184                         switch(solStatus){
    00185                         case VSATNode::Valid:
    00186                                 validTests++;
    00187                                 return Valid;
    00188                         case VSATNode::Satisfiable:
    00189                                 satisfiableTests++;
    00190                                 if(satisfy)
    00191                                         conflict = searchNode.getUnsatAssignment();
    00192                                 else
    00193                                         conflict = searchNode.getValidAssignment();
    00194
    00195                                 ConditionalDebugOut(debug >= 2,
    00196                                         cout << "Conflict: ";
    00197                                         conflict.printArray(cout, ", ");
    00198                                         cout << endl;
    00199                                 );
    00200
    00201                                 return Satisfiable;
    00202                         case VSATNode::Unsatisfiable:
    00203                                 unsatisfiableTests++;
    00204                                 return Unsatisfiable;
    00205                         default:
    00206                                 fprintf(stderr, "Error, VSAT search could "
    00207                                         "not establish Sat/Unsat/Valid\n");
    00208                                 return Unsatisfiable;
    00209                         }
    00210                 }
    00211         }
    00212 }
    00213
    00215
    00216 void ValidSAT::printStatistics(bool verbose) const
    00217 {
    00218         (void) verbose;
    00219         fprintf(stdout, "Valid-Testing Clause Directed Assignment Tester\n");
    00220         fprintf(stdout, "  Branch Nodes Visited: %f\n", numberOfExpandedNodes);
    00221         fprintf(stdout, "  Results: %u Valid, %u SAT, %u UNSAT\n", validTests,
    00222                 satisfiableTests, unsatisfiableTests);
    00223 }
    00224
    00226
    00227 void ValidSAT::setDebug(unsigned int state)
    00228 {
    00229         AssignmentTesterInterface::setDebug(state);
    00230
    00231         modelNode->setDebug(state);
    00232         activeNode->setDebug(state);
    00233 }
    00234