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

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISATClause.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:                        ISATClause.h
    00015 //
    00016 // DESCRIPTION:         Circularly linked list of literal pointers. It follows the C++
    00017 //                                      Standard Template Library specifications. It is in charge of
    00018 //                                      deallocating the literals.
    00019 //
    00020 // DEFINITIONS:
    00021 //
    00022 //      Clause                  A set of disjunction of literals.
    00023 //
    00024 //      Consistent              A clause is consistent if at least one literal is true.
    00025 //
    00026 //      Inconsistent    A clause is inconsistent if all literals are false.
    00027 //
    00028 //      Unit                    A clause with one unassigned literal and all other literals
    00029 //                                      with the value of false.
    00030 //
    00031 //      Unit Resolved   A clause whose last unassigned literal was evaluated by unit
    00032 //                                      resolution (i.e. if a clause is a unit clause, then the one
    00033 //                                      unassigned literal's truth value must be true for the clause
    00034 //                                      to be consistent -- this process of evaluating the truth value
    00035 //                                      of a unit clause is unit resolution).
    00036 //
    00037 //      Consequent              The literal that was evaluated by unit resolution.
    00038 //
    00039 //      Satisfying              Any literal in the clause that is assigned true, thus satisfying
    00040 //                                      the clause.
    00041 //
    00042 //      Resolved                The truth value is known (i.e. if a literal has been resolved,
    00043 //                                      the truth value of the literal is either true or false).
    00044 //
    00045 //      Unresolved              The truth value is unknown (i.e. if a literal is unresolved,
    00046 //                                      the truth value of the literal is unknown)
    00047 //
    00048 //========================================================================================
    00049 #if !defined (ISAT_CLAUSE)
    00050 #define ISAT_CLAUSE
    00051
    00052 #if defined _MSC_VER
    00053 #pragma warning(disable:4786)
    00054 #endif // #if defined _MSC_VER
    00055
    00056 #include <cstdio>
    00057 #include <iostream>
    00058 #include <list>
    00059 #include "ISATLiterals.h"
    00060
    00061 namespace Mers {
    00062         namespace Solvers {
    00063                 namespace SAT {
    00064                         namespace ISAT {
    00065
    00066                                 class ISATLiteral;
    00067                                 class ISATTheory;
    00068
    00069
    00077                                 class ISATClause : public std::list<ISATLiteral *>
    00078                                 {
    00079                                 public:
    00080                                         //------------------------------------------------------------------------------------
    00081                                         // Public Type Definitions, Constants, & Class Declarations
    00082                                         //------------------------------------------------------------------------------------
    00083
    00084                                         enum ConsistencyType    {CONSISTENT, INCONSISTENT, INDETERMINATE};
    00085
    00086                                         //------------------------------------------------------------------------------------
    00087                                         // Friends
    00088                                         //------------------------------------------------------------------------------------
    00089
    00090                                         friend class ISATTheory;
    00091                                         friend std::ostream &   operator <<	(std::ostream &stream, ISATClause const &clause);
    00092                                         friend std::ostream &operator<<(std::ostream &stream,
    00093                                                                                                 ISATClause::ConsistencyType const &clause_consistency);
    00094
    00095                                         //------------------------------------------------------------------------------------
    00096                                         // Public Constructors, Copy Constructors, & Destructors
    00097                                         //------------------------------------------------------------------------------------
    00098
    00099                                         ISATClause();
    00100                                         ISATClause(ISATClause const &other);
    00101                                         virtual ~ISATClause();
    00102
    00103                                         //------------------------------------------------------------------------------------
    00104                                         // Public Function Members
    00105                                         //------------------------------------------------------------------------------------
    00106
    00107                                         // Returns true if this clause is inconsistent (i.e. a clause with all literals
    00108                                         // assigned FALSEVAL) otherwise returns false.
    00109                                         bool                            is_inconsistent() const;
    00110                                         bool                            is_consistent() const;
    00111                                         // Returns the consistency of the clause. A clause may be CONSISTENT, INCONSISTENT,
    00112                                         // or INDETERMINATE.
    00113                                         //
    00114                                         //     o CONSISTENT:    At least one literal is true.
    00115                                         //     o INCONSISTENT:  ALL literals are false.
    00116                                         //     o INDETERMINATE: There are no true literals, but some unknown literals as well.
    00117                                         ConsistencyType         get_consistency() const;
    00118
    00119                                         // Returns true if this clause is a unit clause (i.e. a clause with one unassigned
    00120                                         // literal and all other literals assigned FALSEVAL) otherwise return false.
    00121                                         bool                            is_unit_clause() const;
    00122
    00123                                         // Returns true if this clause was unit resolved otherwise returns false.
    00124                                         bool                            was_unit_resolved() const;
    00125
    00126                                         // Returns the literal whose truth value was assinged by unit resolution of the
    00127                                         // clause (i.e. a consequent is the literal that satisfies the clause if the clasue
    00128                                         // was unit resolved). If the clause was not unit resolved it returns NULL.
    00129                                         ISATLiteral const * get_consequent_literal_p() const;
    00130
    00131                                         ISATLiteral const *     get_unresolved_literal_p() const;
    00132
    00133                                         // Returns the literal whose truth value satisfies this clause. If this clause has a
    00134                                         // consequent, resulting from unit resolution, then the consequent will always be the
    00135                                         // satisfying literal.  Otherwise, the satisfying literal can be any literal that
    00136                                         // makes this clause TRUEVAL."
    00137                                         ISATLiteral const *     get_satisfying_literal_p() const;
    00138
    00139                                         // Returns the number of literals in this clause.
    00140                                         unsigned int            get_numb_of_literals() const;
    00141
    00142                                         //....................................................................................
    00143
    00144                                         // Returns true if the clause is active in theory and false if it is not.
    00145                                         bool                            is_active() const;
    00146
    00147                                         //....................................................................................
    00148
    00149                                         //------------------------------------------------------------------------------------
    00150                                         // Public Operators
    00151                                         //------------------------------------------------------------------------------------
    00152
    00153                                         bool                            operator == (ISATClause const &other) const;
    00154                                         bool                            operator != (ISATClause const &other) const;
    00155                                 //      ISATClause const &      operator =      (ISATClause const &other);
    00156                                         ISATClause const &      operator +=	(ISATClause const &other);
    00157
    00158                                 protected:
    00159                                         //------------------------------------------------------------------------------------
    00160                                         // Protected Function Members
    00161                                         //------------------------------------------------------------------------------------
    00162
    00163                                         void                            set_unit_resolved(bool boolean_value);
    00164
    00165                                         void                            increment_numb_of_unresolved_literals();
    00166                                         void                            decrement_numb_of_unresolved_literals();
    00167
    00168                                         void                            set_satisfying_literal(ISATLiteral const *literal_p);
    00169                                         void                            remove_from_satisfying_literals(ISATLiteral const *literal_p);
    00170
    00171                                         void                            reset_status();
    00172
    00173                                         // Add a new literal into this clause.
    00174                                         bool                            add_literal(ISATLiteral *new_literal_p);
    00175
    00176                                         // Sets the clause to be either active or inactive.
    00177                                         void                            set_active(bool boolean_value);
    00178
    00179                                         //------------------------------------------------------------------------------------
    00180                                         // Protected Object & Data Members
    00181                                         //------------------------------------------------------------------------------------
    00182
    00183                                         // "satisfying_literal_p" is the literal that currently satisfies this clause, i.e.,
    00184                                         // a positive literal whose proposition is TRUEVAL or a negative literal whose
    00185                                         // proposition is FALSEVAL.  If a literal of this clause was resolved based on unit
    00186                                         // clause resolution then it will always be specified under "_satisfying_literal_p".
    00187                                         ISATLiteral const *     satisfying_literal_p;
    00188
    00189                                         // "numb_of_unresolved_literals" indicates number of unresolved literals in this
    00190                                         // clause. This is only present to reduce the time required to determine if the clause
    00191                                         // is satisfied, unsatisfied, or unknown.
    00192                                         unsigned int            numb_of_unresolved_literals;
    00193
    00194                                         // "unit_resolved" indicates whether this clause was unit resolved or not.
    00195                                         bool                            unit_resolved;
    00196
    00197                                         //....................................................................................
    00198
    00199                                         // "in_theory" indicates whether this caluse is in theory.
    00200                                         bool                            active;
    00201
    00202                                 };
    00203                         }
    00204                 }
    00205         }
    00206 }
    00207
    00208 #endif // !defined (ISAT_CLAUSE)
    00209
    00210