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

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

    00001 //========================================================================================
    00002 //
    00003 // Copyright (c) 2001           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 (MERS) group
    00007 // does not assume any responsibility.
    00008 //
    00009 // Author:                      Seung H. Chung
    00010 //
    00011 // Organization:        Model-based Embedded and Robotic Systems Group
    00012 //                                      Massachusetts Institute of Technology
    00013 //
    00014 // File:                        ISATTheory.h
    00015 //
    00016 // Description:         Circularly linked list of clause pointers. It follows the C++
    00017 //                                      Standard Template Library specifications. It is in charge of
    00018 //                                      deallocating the clauses.
    00019 //
    00020 // Acronyms:
    00021 //
    00022 //
    00023 //========================================================================================
    00024
    00025 #if !defined(ISAT_THEORY)
    00026 #define ISAT_THEORY
    00027
    00028 #if defined _MSC_VER
    00029 #pragma warning(disable:4786)
    00030 #endif // #if defined _MSC_VER
    00031
    00032 #include <iostream>
    00033 #include "ISATLiteral.h"
    00034 #include "ISATPropositionDB.h"
    00035
    00036 namespace Mers {
    00037         namespace Solvers {
    00038                 namespace SAT {
    00039                         namespace ISAT {
    00040
    00041                                 class ISATPropositionDescription;
    00042                                 class ISATProposition;
    00043                                 class ISATPropositions;
    00044                                 class ISATUnassignedPropositions;
    00045                                 class ISATClause;
    00046                                 class ISATClauses;
    00047                                 class ISATUnitClauses;
    00048                                 class ISATInconsistentClauses;
    00049                                 class ISATClauseDB;
    00050                                 class ISATClausesSet;
    00051
    00052
    00053                                 //#class ISATTheory : protected ISATClauseDB
    00054
    00058                                 class ISATTheory : public ISATPropositionDB
    00059                                 {
    00060                                 public:
    00061                                         //------------------------------------------------------------------------------------
    00062                                         // Public Type Definitions, Constants, & Class Declarations
    00063                                         //------------------------------------------------------------------------------------
    00064
    00065                                         enum ConsistencyType    {CONSISTENT, INCONSISTENT, INDETERMINATE};
    00066
    00067                                         friend std::ostream &operator <<(std::ostream &stream, ISATTheory const &theory);
    00068                                         friend std::ostream &operator <<(std::ostream &stream,
    00069                                                                                                 ISATTheory::ConsistencyType const &theory_consistency);
    00070
    00071                                         //------------------------------------------------------------------------------------
    00072                                         // Public Constructors, Copy Constructors, & Destructors
    00073                                         //------------------------------------------------------------------------------------
    00074
    00075                                         ISATTheory();
    00076                                         ISATTheory(ISATTheory const &other);
    00077                                         virtual ~ISATTheory();
    00078
    00079                                         //------------------------------------------------------------------------------------
    00080                                         // Public Function Members
    00081                                         //------------------------------------------------------------------------------------
    00082
    00083                                         ConsistencyType                 get_consistency(bool use_DPLL);
    00084                                         ISATClausesSet const *  get_SAT_conflicts_p(bool use_DPLL);
    00085                                         ISATClausesSet const *  get_SAT_conflicts_p_using_fact(
    00086                                                                                                 bool use_DPLL, ISATClauses *clauses_p = NULL);
    00087                                         ISATClausesSet const *  get_UNSAT_conflicts_p(bool use_DPLL);
    00088                                         ISATClausesSet const *  get_UNSAT_conflicts_p_using_fact(
    00089                                                                                                 bool use_DPLL, ISATClauses *clauses_p = NULL);
    00090
    00091                                         ConsistencyType                 get_current_consistency() const;
    00092
    00093                                         ISATClause *                    insert_new_empty_clause();
    00094
    00095                                         void                                    add_literal_to_new_clause(
    00096                                                                                                 ISATPropositionDescription *description_p,
    00097                                                                                                 ISATLiteral::PolarityType polarity);
    00098
    00099                                         void                                    remove_clause(ISATClause *clause_p);
    00100                                         void                                    activate_clause(ISATClause *clause_p);
    00101                                         void                                    deactivate_clause(ISATClause *clause_p);
    00102
    00103                                         ISATPropositionDB const *get_propositions_p() const;
    00104                                         ISATInconsistentClauses const *get_inconsistent_clauses_p() const;
    00105                                         ISATUnassignedPropositions const *get_unassigned_propositions_p() const;
    00106
    00107                                         //All propagation takes places in this fuction: propagate_unit_clauses and DPLL
    00108                                         void                                    propagate_clauses(bool use_DPLL);
    00109
    00110                                         void                                    propagate_using_DPLL();
    00111                                         void                                    clear_DPLL_search();
    00112
    00113                                         // Propagates the unit clauses of the theory until the set of unit clauses becomes
    00114                                         // empty, or an inconsistency is detected. If the set of unit  clauses becomes empty,
    00115                                         // then all propositions have truth values that are "unit propagation entailed" by
    00116                                         // the theory. If no unit clauses are provided, it defaults to the thoery's list of
    00117                                         // unit clauses.
    00118                                         void                                    propagate_unit_clauses(ISATUnitClauses *unit_clauses_p = NULL);
    00119
    00120                                         double                                  assign_proposition_count;
    00121                                         double                                  unassign_proposition_count;
    00122
    00123                                         double                                  total_time;
    00124
    00125                                 #if defined(_DEBUG)
    00126                                         void                                    set_debug_level(int debug_level_numb);
    00127                                 #endif // #if defined(_DEBUG)
    00128
    00129                                 protected:
    00130                                         //------------------------------------------------------------------------------------
    00131                                         // Protected Function Members
    00132                                         //------------------------------------------------------------------------------------
    00133
    00134                                         ISATClauses const *             get_supporting_clauses_p(
    00135                                                                                                 ISATProposition *proposition_p) const;
    00136                                         ISATClauses const *             get_supporting_clauses_p(ISATClause *clause_p) const;
    00137
    00138
    00139
    00140                                         //....................................................................................
    00141
    00142                                         // Propagates the unit clause.
    00143                                         void                                    propagate_unit_clause(ISATClause *clause_p);
    00144                                         void                                    unpropagate_clause(ISATClause *clause_p);
    00145
    00146                                         ISATUnitClauses *               assign_proposition_truth_value(ISATProposition *proposition_p,
    00147                                                                                                                                                 bool truth_value);
    00148
    00149                                         ISATUnitClauses *               assign_proposition_true(ISATProposition *proposition_p);
    00150                                         ISATUnitClauses *               assign_proposition_false(ISATProposition *proposition_p);
    00151                                         void                                    unassign_proposition(ISATProposition *proposition_p);
    00152
    00153                                         //------------------------------------------------------------------------------------
    00154                                         // Protected Object & Data Members
    00155                                         //------------------------------------------------------------------------------------
    00156
    00157                                         ISATClauseDB *                                  clause_database_p;
    00158
    00159                                         ISATClause *                                    new_clause_p;
    00160
    00161                                         ISATPropositions *                              searched_propositions_p;
    00162                                         long int                                                searched_path_length;
    00163
    00164                                         // "unassigned_propositions" is a list of propositions that have not yet been
    00165                                         // assigned a truth value by the satisfiability procedure.
    00166                                         ISATUnassignedPropositions *    unassigned_propositions_p;
    00167
    00168                                         // "unit_clauses" is a list of unit clauses in theory. A unit clause is any clauses
    00169                                         // that has one unassigned literal, with all other literals assigned false. This list
    00170                                         // is updated as truth assignments of propositions are changed by unit propagation.
    00171                                         // "unit_clauses" is used as a stack in which the unit clauses are pushed and poped
    00172                                         // from the front.
    00173                                         ISATUnitClauses *                               unit_clauses_p;
    00174
    00175                                         // "inconsistent_clauses" is a list of clauses in theory that have all false
    00176                                         // literals. This list is updated as the truth assignments of propositions are changed
    00177                                         // by unit propagation.
    00178                                         ISATInconsistentClauses *               inconsistent_clauses_p;
    00179
    00180                                         ISATClausesSet *                                        SAT_conflicts_p;
    00181                                         ISATClausesSet *                                        UNSAT_conflicts_p;
    00182
    00183                                 #if defined _DEBUG
    00184                                         int                                                             debug_level;
    00185                                 #endif // #if defined _DEBUG
    00186
    00187                                 };
    00188                         }
    00189                 }
    00190         }
    00191 }
    00192
    00193 #endif // !defined (ISAT_THEORY)
    00194
    00195
    00196 //      ISATProposition const * get_propostion_p(
    00197 //                                                              ISATPropositionDescription const *description_p);
    00198
    00199 //      ISATProposition const * get_proposition_p(ISATPropositionDescription const *description_p);
    00200
    00201 //      void                                    insert_clause(ISATClause *clause_p);
    00202 //      void                                    insert_clauses(ISATClauses *clauses_p);
    00203
    00204         // Undoes all current truth assignments and support that resulted from propagating
    00205         // "clause_p" in theory. It also updates any clause status of the theory that has
    00206         // changed.
    00207
    00208
    00209         // "proposition_database" is a database of propositions. This database contains all
    00210         // propositions that apear in the theory.
    00211 //      ISATPropositionDB *             proposition_database_p;
    00212
    00213         // "assigned_propositions" is a list of propositions that have been assigned a truth
    00214         // value by the satisfiability procedure.
    00215 //      ISATPropositions *              assigned_propositions_p;