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

# /Users/fpy/titan-1-5-MBARI/Mers/Models/Base/Utils/MutualExclusionAndExhaustion.cpp

    00001 //=============================================================================
    00002 //MutualExclusionAndExhaustion.h: interface for the
    00003 //MutualExclusionAndExhaustion class.
    00004 //
    00005 // Copyright (c) 2003           Model-based Embedded and Robotic Systems Group
    00006 // All Rights Reserved          Massachusetts Institute of Technology
    00007 //
    00008 // This software is provided as is. Model-based Embedded and Robotic Systems
    00009 // (MERS) group does not assume any responsibility.
    00010 //
    00011 // Author:                      Paul Elliott
    00012 // Organization:        Model-based Embedded and Robotic Systems Group
    00013 //                                      Massachusetts Institute of Technology
    00014 //
    00015 // Basic class for adding and removing mutual exclusion and exhaustion
    00016 // clauses from a theory.  This class operates on a BaseModelClause.
    00017 //
    00018 // Mutual exclusion clauses, for a variable v with domain (d1, d2,
    00019 // .. dn) are of the form (!(v = d1) or !(v = d2)) and (!(v = d1) or
    00020 // !(v = d3)) and .. (!(v = d1) or !(v = dn)) and .. (!(v = d2) or !(v
    00021 // = d3)) and ... (!(v = dn-1) or !(v = dn)).  So n^2 / 2 terms for a
    00022 // domain of size n.  This constraint states that there cannot be more
    00023 // than one assignment to v.
    00024 //
    00025 // An Exhaustion clause is of the form ((v = d1) or (v = d2) or (v =
    00026 // d3) or .. (v = dn)).  This constraint says that there must be at
    00027 // least one assignment to v.
    00028 //
    00029 // Combined, these state that there must be exactly one assignment to
    00030 // each variable v.
    00031 //
    00032 // Traditional SAT engines require these clauses because they only
    00033 // work with literals, such as (v = d3), and this can either be true
    00034 // or false.
    00035 //
    00036 // However, some of the SAT engines know that the variable v has the
    00037 // domain d, and so knows that (v = d3) really means "v is assigned
    00038 // d3", so the mutual exclusion and exhaustion clauses are redundant,
    00039 // if not harmfull.
    00040 //
    00041 //=============================================================================
    00042
    00043 #include "MutualExclusionAndExhaustion.h"
    00044
    00046
    00047 MutualExclusionAndExhaustion::MutualExclusionAndExhaustion()
    00048 {
    00049 }
    00050
    00052
    00053 MutualExclusionAndExhaustion::MutualExclusionAndExhaustion
    00054         (MutualExclusionAndExhaustion const &other)
    00055 {
    00056         (void) other;
    00057 }
    00058
    00060
    00061 MutualExclusionAndExhaustion::~MutualExclusionAndExhaustion()
    00062 {
    00063 }
    00064
    00066
    00067 int MutualExclusionAndExhaustion::removeMEE(BaseModelSentence &theory)
    00068 {
    00069         // Find clauses of the form (!(Vn = Dx) or !(Vn = Dy))
    00070
    00071         // Find clauses of the form ((Vn = D0) or (Vn = D1) or (Vn = D2) or ...)
    00072
    00073 }
    00074
    00076
    00077 int MutualExclusionAndExhaustion::addMEE(BaseModelSentence &theory)
    00078 {
    00079         // Copy over a variable set and then call addMEE(var set, theory)
    00080 }
    00081
    00083
    00084 int
    00085 MutualExclusionAndExhaustion::addMEE(BaseModelVariableArray const &variables,
    00086         BaseModelSentence &theory)
    00087 {
    00088         // Add clauses of the form (!(Vn = Dx) or !(Vn = Dy))
    00089
    00090         // Add clauses of the form ((Vn = D0) or (Vn = D1) or (Vn = D2) or ...)
    00091 }
    00092
    00094