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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/GATSAT.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 //
    00010
    00011 #include "GATSAT.h"
    00012 #include <Mers/Generators/AssignmentGeneratorInterface.h>
    00013 #include <Mers/Solvers/SAT/AssignmentTesterInterface.h>
    00014
    00016
    00017 using namespace Mers::Solvers::SAT::GATSAT;
    00018 using Mers::Generators::AssignmentGeneratorInterface;
    00019 using Mers::Solvers::SAT::AssignmentTesterInterface;
    00020 using Mers::Models::Base::BaseModelClause;
    00021 using Mers::Models::Base::BaseModelAssignmentArray;
    00022 using log4cplus::Logger;
    00023 using std::cerr;
    00024 using std::endl;
    00025
    00027
    00028 Logger GATSAT::m_Logger =
    00029         Logger::getInstance("Mers.Solvers.SAT.GATSAT.GATSAT");
    00030
    00032
    00033 GATSAT::GATSAT() : SATInterface()
    00034 {
    00035         generator = NULL;
    00036         tester = NULL;
    00037 }
    00038
    00040
    00041 GATSAT::GATSAT(AssignmentGeneratorInterface * myGenerator,
    00042         AssignmentTesterInterface * myTester) : SATInterface()
    00043 {
    00044         generator = myGenerator;
    00045         tester = myTester;
    00046 }
    00047
    00049
    00050 GATSAT::~GATSAT()
    00051 {
    00052         if(generator != NULL)
    00053                 delete generator;
    00054         if(tester != NULL)
    00055                 delete tester;
    00056 }
    00057
    00059
    00060 BaseModelClause * GATSAT::findSatisfyingSolution(
    00061         int maximumVisitedStateCount, int maxSize)
    00062 {
    00063         BaseModelClause * solution = NULL;
    00064
    00065         unsigned int minSize = generator->getFullAssignmentSize();
    00066
    00067         do{
    00068                 unsigned int group = 0;
    00069                 BaseModelAssignmentArray conflict(false);
    00070
    00071                 BaseModelAssignmentArray const * candidate =
    00072                         generator->generateBestImplicant(maximumVisitedStateCount,
    00073                                                          maxSize, false);
    00074
    00075                 if(!candidate){
    00076                         // generator is all out of valid solutions
    00077                         LOG4CPLUS_DEBUG_STR(m_Logger,
    00078                                 "Assignment Generator has run out of assignments.");
    00079                         return NULL;
    00080                 }
    00081
    00082                 LOG4CPLUS_DEBUG(m_Logger, "Candidate: " << *candidate);
    00083
    00084                 // Test our candidate.
    00085                 AssignmentTesterInterface::SolutionType status =
    00086                         tester->tryAssignment(candidate, group, true, conflict);
    00087
    00088                 // Add a conflict, if present
    00089                 if(conflict.getLength() > 0) {
    00090                         LOG4CPLUS_DEBUG(m_Logger, "Generated Conflict: " << conflict);
    00091
    00092                         generator->addConflict(conflict);
    00093                 }
    00094
    00095                 // Check our status
    00096                 switch(status){
    00097                         // An UNSATISFIABLE result:            Conflict
    00098                         // A VALID result:           Solution, No-SuperSets
    00099                         // A SATISFIABLE result:     Solution, No-SuperSets
    00100                 case AssignmentTesterInterface::Unsatisfiable:
    00101                         LOG4CPLUS_DEBUG(m_Logger, "Candidate is Unsatisfiable");
    00102
    00103                         // so add as a conflict
    00104                         generator->addConflict(candidate);
    00105                         break;
    00106                 case AssignmentTesterInterface::Valid:
    00107                         LOG4CPLUS_DEBUG(m_Logger, "Candidate is Valid");
    00108
    00109                         // add a solution
    00110                         solution = new BaseModelClause(BaseModelClause::CONJUNCTIVE, true);
    00111                         *solution += (*candidate);
    00112                         // tell the generator to skip any supersets
    00113                         generator->markBestFeasible();
    00114                         break;
    00115                 case AssignmentTesterInterface::Satisfiable:
    00116                         LOG4CPLUS_DEBUG(m_Logger, "Candidate is Satisfiable");
    00117
    00118                         if(candidate->getLength() >= minSize) {
    00119                                 // add a solution
    00120                                 solution = new BaseModelClause(BaseModelClause::CONJUNCTIVE, true);
    00121                                 *solution += (*candidate);
    00122                                 // tell the generator to skip any supersets
    00123                                 generator->markBestFeasible();
    00124                         }
    00125                         break;
    00126                 default:
    00127                         LOG4CPLUS_DEBUG(m_Logger, "Candidate is Unknown");
    00128                         break;
    00129                 }
    00130         }while(solution == NULL);
    00131         return solution;
    00132 }
    00133
    00135
    00136 BaseModelClause * GATSAT::findUnsatisfyingSolution(
    00137                 int maximumVisitedStateCount, int maxSize)
    00138 {
    00139         BaseModelClause * solution = NULL;
    00140
    00141         do{
    00142                 unsigned int group = 0;
    00143                 BaseModelAssignmentArray conflict(false);
    00144
    00145                 BaseModelAssignmentArray const * candidate =
    00146                         generator->generateBestImplicant(maximumVisitedStateCount,
    00147                                 maxSize, false);
    00148
    00149                 if(!candidate){
    00150                         // generator is all out of valid solutions
    00151                         LOG4CPLUS_DEBUG_STR(m_Logger,
    00152                                 "Assignment Generator has run out of assignments.");
    00153
    00154                         return NULL;
    00155                 }
    00156
    00157                 LOG4CPLUS_DEBUG(m_Logger, "Candidate: " << *candidate);
    00158
    00159                 AssignmentTesterInterface::SolutionType status =
    00160                         tester->tryAssignment(candidate, group, false, conflict);
    00161                 // add a conflict, if present
    00162                 if(conflict.getLength() > 0){
    00163                         LOG4CPLUS_DEBUG(m_Logger, "Conflict: " << conflict);
    00164
    00165 #ifdef _DEBUG
    00166                         {
    00167                                 // Verify the conflict.
    00168                                 // Note that this isn't exact.  If the conflicts are correct (should be)
    00169                                 // this may still say satisfiable, but it's good for debugging.
    00170 #if (0)
    00171                                 BaseModelAssignmentArray tmpConflict(false);
    00172                                 AssignmentTesterInterface::SolutionType conflictStatus =
    00173                                         tester->tryAssignment(&conflict, group, false, tmpConflict);
    00174
    00175                                 if(conflictStatus != AssignmentTesterInterface::Valid){
    00176                                         cerr << "GATSAT::findUnsatisfyingSolution: Error: Conflict ";
    00177                                         conflict.printArray(cerr, ", ");
    00178                                         cerr << " was not Valid!" << endl << "  It was ";
    00179                                         switch(conflictStatus){
    00180                                         case AssignmentTesterInterface::Satisfiable:
    00181                                                 cerr << "Satisfiable" << endl;
    00182                                                 break;
    00183                                         case AssignmentTesterInterface::Unsatisfiable:
    00184                                                 cerr << "Unsatisfiable" << endl;
    00185                                                 break;
    00186                                         }
    00187                                         cerr << "Generated Additional Conflict: ";
    00188                                         tmpConflict.printArray(cerr, ", ");
    00189                                         cerr << endl;
    00190                                 }else{
    00191                                         generator->addConflict(conflict);
    00192                                 }
    00193 #else
    00194                                 generator->addConflict(conflict);
    00195 #endif
    00196                         }
    00197 #else
    00198                         generator->addConflict(conflict);
    00199 #endif
    00200                 }
    00201                 switch(status){
    00202                         // An UNSATISFIABLE result:  Solution, No-SuperSets
    00203                         // A VALID result:                     Conflict
    00204                         // A SATISFIABLE result:               Conflict?
    00205                 case AssignmentTesterInterface::Unsatisfiable:
    00206                         // UNSAT -> Solution & we don't want supersets
    00207                         LOG4CPLUS_DEBUG_STR(m_Logger, "Candidate is Unsatisfiable");
    00208
    00209                         // add a solution
    00210                         solution = new BaseModelClause(BaseModelClause::CONJUNCTIVE, true);
    00211                         ((BaseModelAssignmentArray *)solution)->operator +=(*candidate);
    00212                         // tell the generator to skip any supersets
    00213                         generator->markBestFeasible();
    00214                         break;
    00215                 case AssignmentTesterInterface::Valid:
    00216                         // VALID -> Not a solution and will never be a solution.
    00217                         LOG4CPLUS_DEBUG_STR(m_Logger, "Candidate is Valid");
    00218
    00219                         // so add as a conflict
    00220                         generator->addConflict(candidate);
    00221                         break;
    00222                 case AssignmentTesterInterface::Satisfiable:
    00223                 default:
    00224                         // SAT -> Not a solution, add the conflict if we have one.
    00225                         LOG4CPLUS_DEBUG_STR(m_Logger, "Candidate is Satisfiable");
    00226                         break;
    00227                 }
    00228         }while(solution == NULL);
    00229         return solution;
    00230 }
    00231
    00233
    00234 void GATSAT::setDebug(unsigned int state)
    00235 {
    00236         debug = state;
    00237         if(generator != NULL)
    00238                 generator->setDebug(state);
    00239         if(tester != NULL)
    00240                 tester->setDebug(state);
    00241 }
    00242
    00244
    00245 void GATSAT::printStatistics() const
    00246 {
    00247         if(generator != NULL)
    00248                 generator->printStatistics();
    00249         if(tester != NULL)
    00250                 tester->printStatistics();
    00251 }
    00252
    00254
    00255 AssignmentGeneratorInterface * GATSAT::getGenerator()
    00256 {
    00257         return generator;
    00258 }
    00259
    00261
    00262 AssignmentTesterInterface * GATSAT::getTester()
    00263 {
    00264         return tester;
    00265 }
    00266
    00268