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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/SATInterface.h

    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 #ifndef SATInterfaceHeaderFile
    00015 #define SATInterfaceHeaderFile
    00016
    00017 #include <cstdlib>
    00018
    00019 #include <Mers/Models/Base/BaseModelClauseArray.h>
    00020
    00021 namespace Mers {
    00022         namespace Solvers {
    00023                 namespace SAT {
    00024
    00030                         class SATInterface
    00031                         {
    00032                         protected:
    00034                                 // Constructors
    00036
    00048                                 SATInterface()
    00049                                 {
    00050                                         debug = 0;
    00051                                 }
    00052
    00054                                 // Destructors
    00056
    00060                                 virtual ~SATInterface()
    00061                                 {
    00062                                 }
    00063
    00064                         public:
    00066                                 // Functions
    00068
    00084                                 virtual Mers::Models::Base::BaseModelClauseArray * findSatisfyingSolutions(unsigned int count,
    00085                                                                                                                                                                                                                                                          int maximumVisitedStateCount, int maxSize)
    00086                                 {
    00087                                         Mers::Models::Base::BaseModelClauseArray * solutions = NULL;
    00088
    00089                                         ConditionalDebugOut(debug >= 1,
    00090                                                                                                                         printf("SAT looking for %d solutions.\n", count);
    00091                                                                                                                         );
    00092                                         for(unsigned int x = 0; x < count; x++){
    00093                                                 Mers::Models::Base::BaseModelClause * solution =
    00094                                                         findSatisfyingSolution(maximumVisitedStateCount, maxSize);
    00095
    00096                                                 if(solution == NULL){
    00097                                                         ConditionalDebugOut(debug >= 1,
    00098                                                                                                                                         printf("Found %d/%d SAT solutions.\n", x, count);
    00099                                                                                                                                         );
    00100                                                         return solutions;
    00101                                                 }
    00102
    00103                                                 if(solutions == NULL)
    00104                                                         solutions = new Mers::Models::Base::BaseModelClauseArray(true);
    00105                                                 solutions->pushBack(solution);
    00106                                         }
    00107                                         ConditionalDebugOut(debug >= 1,
    00108                                                                                                                         printf("Found %d/%d SAT solutions.\n", count, count);
    00109                                                                                                                         );
    00110                                         return solutions;
    00111                                 }
    00112
    00127                                 virtual Mers::Models::Base::BaseModelClause * findSatisfyingSolution(
    00128                                                                                                                                                                                                                                  int maximumVisitedStateCount, int maxSize) = 0;
    00129
    00145                                 virtual Mers::Models::Base::BaseModelClauseArray * findUnsatisfyingSolutions(unsigned int count,
    00146                                                                                                                                                                                                                                                                  int maximumVisitedStateCount, int maxSize)
    00147                                 {
    00148                                         Mers::Models::Base::BaseModelClauseArray * solutions = NULL;
    00149
    00150                                         ConditionalDebugOut(debug >= 1,
    00151                                                                                                                         printf("UNSAT looking for %d solutions.\n", count);
    00152                                                                                                                         );
    00153                                         for(unsigned int x = 0; x < count; x++){
    00154                                                 Mers::Models::Base::BaseModelClause * solution =
    00155                                                         findUnsatisfyingSolution(maximumVisitedStateCount, maxSize);
    00156
    00157                                                 if(solution == NULL){
    00158                                                         ConditionalDebugOut(debug >= 1,
    00159                                                                                                                                         printf("Found %d/%d UNSAT solutions.\n", x, count);
    00160                                                                                                                                         );
    00161                                                         return solutions;
    00162                                                 }
    00163
    00164                                                 if(solutions == NULL)
    00165                                                         solutions = new Mers::Models::Base::BaseModelClauseArray(true);
    00166                                                 solutions->pushBack(solution);
    00167                                         }
    00168                                         ConditionalDebugOut(debug >= 1,
    00169                                                                                                                         printf("Found %d/%d UNSAT solutions.\n", count, count);
    00170                                                                                                                         );
    00171                                         return solutions;
    00172                                 }
    00173
    00188                                 virtual Mers::Models::Base::BaseModelClause * findUnsatisfyingSolution(
    00189                                                                                                                                                                                                                                          int maximumVisitedStateCount, int maxSize) = 0;
    00190
    00198                                 virtual void setDebug(unsigned int state)
    00199                                 {
    00200                                         debug = state;
    00201                                 }
    00202
    00203                         protected:
    00205                                 // Data
    00207
    00209                                 unsigned int debug;
    00210                         };
    00211                 }
    00212         }
    00213 }
    00214
    00215 #endif //ndef SATInterfaceHeaderFile
    00216