Constraint and Consequence
 
   
  Craig Holman   Research   Jabberwocky   Quotations   Contact
 
  Home > Jabberwocky           Previous      Next
 
 
 

Jabberwocky for June 10, 2008
 
 

The Reduce To Elegance Algorithm

          First in thread      Previous in thread      Next in thread

After not touching my source code for boolean satisfiability testing and reduction for several years, I recently spent several weekends tinkering with it and getting it running again.

I'll write up the algorithm properly later, but I want to get it out in some form this week, and that form is some of my current C++ source code for the application.

In order to get this source code, I removed a great deal of debugging and tracing code. I've made a good-faith effort to do so with care, but I'm not sure I didn't remove something important. I'll continue to review the code and correct any errors or omissions that I discover.

I'm still reviewing and revising the code for reduction to elegance and will post revisions as appropriate.

I'd been planning on posting a proof that the elegance reductions are a complete set of reductions before posting this, but I'm still typing it and am only about halfway through. You'll understand when you see it.

The following constraint tree was often used when exploring transformations and may be useful as a reference constraint tree.

 

 

Notes on the source code

A constraint tree is made of of alternating layers of And nodes and Or nodes. The root of a constraint tree is an And node.

The Reduce to Elegance algorithm follows this alternating-layer structure in that it has two mutually-recursive methods to handle nodes at each type of layer.

The AndReduceToElegance method is applied to And nodes and the OrReduceToElegance method is applied to Or nodes.

A CConstraintSet is a class that encompasses two CSets - one a set of positive constraints, and the other a set of negative constraints.

A dominant set of a node is the union of the guard sets in the nodes that are in the handle of the broom centered at the node, of the nodes that dominated the node.

A side set of a node is the union of the guard sets of the siblings of the node that only contain one constraint.

The InconsistentHandle method tests for an inconsistent handle in the broom centered at the node it is passed and returns the action that should be taken (i.e. keep or delete).

The AndCut method tests for an opportunity to remove an unnecessary And node and performs the surgery if warranted.

The OrCut method tests for an opportunity to remove an unnecessary Or node and performs the surgery if warranted.

The other elegance transformations are tested for and applied in AndReduceToElegance and OrReduceToElegance direct without being packaged as separate methods.

The AdoptGreatGrandchildren method takes three parameters, poNode, poDoomedChild, and poDoomedGrandchild, replaces the reference to the doomed child in poNode's list of children with references to poDoomedGrandchild's children, and then deletes poDoomedChild and poDoomedGrandchild. This method is used by both AndCut and OrCut.

The ReleaseTree method removes the subtree rooted at the node it is passed, including the node it is passed.

The ZeroConstraints method returns true iff the node it is passed has zero children.

The OneConstraint method returns true iff the node it is passed has one child.

Several of the CSet methods such as Intersect and Union operate on the first two parameters and set the third parameter to the result.

_poRoot points to the root node of the constraint tree.

Partial C++ source code for reducing a constraint tree to Elegant Normal Form

The following is also available as a file.

  
EPCResult
CBooleanExpression::
ReduceToElegance()
{
   CConstraintSet   csetDominant;
   CConstraintSet   csetSide;

   switch ( AndReduceToElegance ( _poRoot, csetDominant, csetSide ) )
   {
      case  keDelete :

            ReleaseTree( _poRoot );

            _poRoot = NULL;

            ReportEvent( keLogicalClass, keContradiction );
            break;

      case  keDisconnect :

            ReleaseTree( _poRoot );

            _poRoot = NULL;

            ReportEvent( keLogicalClass, keTautology );
            break;

      case  keKeep :

            if ( _poRoot->_vpoChildren.size() == 0  &&  
                 _poRoot->_csetConstraints.Cardinality() == 0 )
            {
               ReportEvent( keLogicalClass, keTautology );
            }
            else
            {
               ReportEvent( keLogicalClass, keUndetermined ); 
            }
            break;
   }

   return keSuccess;
}

EReductionSignal
CBooleanExpression::
AndReduceToElegance( IN     CNode *            poCurrentNode,
                     INOUT  CConstraintSet &   rcsetDominant,
                     INOUT  CConstraintSet &   rcsetSide )
{
   CConstraintSet   csetHandle;
   CConstraintSet   csetPrevious;
   CConstraintSet   csetResult;

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Subtract redundant constraints
   //
   ///////////////////////////////////////////////////////////////////////////

   csetResult = poCurrentNode->_csetConstraints;

   poCurrentNode->_csetConstraints -= rcsetDominant;

   csetResult -= poCurrentNode->_csetConstraints;

   if ( csetResult.Cardinality() > 0 )
   {
      if ( poCurrentNode->_csetConstraints.Cardinality() == 0 )
      {
         if ( poCurrentNode->_vpoChildren.size == 0 )
         {
            return keDisconnect;
         }
      }
   }

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Remove opposing command constraints
   //
   /////////////////////////////////////////////////////////////////////////// 

   csetResult = poCurrentNode->_csetConstraints;

   poCurrentNode->_csetConstraints._setPositive -= rcsetSide._setNegative;

   poCurrentNode->_csetConstraints._setNegative -= rcsetSide._setPositive;

   csetResult -= poCurrentNode->_csetConstraints;

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Detect zero-contraint subsumption by the current node
   //
   ///////////////////////////////////////////////////////////////////////////

   if ( poCurrentNode->_vpoChildren.size() == 0  &&  ZeroConstraints( poCurrentNode ) )
   {
      return keDisconnect;
   }

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Detect one-constraint subsumption of selections containing the
   //  current node
   //
   ///////////////////////////////////////////////////////////////////////////

   SetIntersection( poCurrentNode->_csetConstraints, rcsetSide, csetResult );

   if ( csetResult.Cardinality() > 0 )
   {
      _bDeleteDueToInconsistentHandle = false;

      return keDelete;
   }

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Major cycle of reduction
   //
   ///////////////////////////////////////////////////////////////////////////

   do
   {
      ///////////////////////////////////////////////////////////////////////
      //
      //  Remember the current value of the current node's guard set
      //
      ///////////////////////////////////////////////////////////////////////

      csetPrevious = poCurrentNode->_csetConstraints;

      ///////////////////////////////////////////////////////////////////////
      //
      //  Detect an inconsistent handle set
      //
      ///////////////////////////////////////////////////////////////////////

      if ( InconsistentHandle( poCurrentNode, rcsetDominant, csetHandle ) == keDelete )
      {
         return keDelete;
      }

      ///////////////////////////////////////////////////////////////////////
      //
      //  Reduce each child's subtree
      //
      ///////////////////////////////////////////////////////////////////////

      int  iInitialNumChildren = poCurrentNode->_vpoChildren.size();

      for ( std::vector<CNode *>::iterator  
      
                ppoChild = poCurrentNode->_vpoChildren.begin();
                ppoChild != poCurrentNode->_vpoChildren.end();
          )
      {
         switch ( OrReduceToElegance( *ppoChild, csetHandle, rcsetSide ) )
         {
            case  keDelete :

                  {
                     for ( std::vector<CNode *>::iterator  
                     
                        ppoChild2 = poCurrentNode->_vpoChildren.begin();
                        ppoChild2 != poCurrentNode->_vpoChildren.end();
                        ++ppoChild2 )
                     {
                        ReleaseTree( *ppoChild2 );
                     }

                     poCurrentNode->_vpoChildren.clear();

                     return keDelete;
                  }

            case  keDisconnect :

                  ReleaseTree( *ppoChild );

                  ppoChild = poCurrentNode->_vpoChildren.erase( ppoChild );

                  if ( poCurrentNode->_vpoChildren.size() == 0 )
                  {
                     if ( poCurrentNode->_csetConstraints.Cardinality() == 0 )
                     {
                        return keDisconnect;
                     }
                     else if ( poCurrentNode->_csetConstraints.Cardinality() == 1 )
                     {
                        return keKeepNewTerminalUnit;
                     }
                  }
                  break;

            case  keKeep :

                  switch ( AndCut( *ppoChild ) )
                  {
                     case  keDisconnect :

                           ReleaseTree( *ppoChild );

                           ppoChild = poCurrentNode->_vpoChildren.erase( ppoChild );

                           if ( poCurrentNode->_vpoChildren.size() == 0 )
                           {
                              if ( poCurrentNode->_csetConstraints.Cardinality() == 0 )
                              {
                                 return keDisconnect;
                              }
                              else if ( poCurrentNode->_csetConstraints.Cardinality() == 1 )
                              {
                                 return keKeepNewTerminalUnit;
                              }
                           }
                           break;


                     case  keKeep :

                           ++ppoChild;
                           break;                         

                     case  keKeepNewTerminalUnit :

                           break;
                  }

                  break;

            case  kePromoteConstraints :

                  poCurrentNode->_csetConstraints.UnionWith( _csetPromotableConstraints );

                  csetHandle.UnionWith( csetResult );

                  CConstraintSet   csetDoomed;

                  for ( std::vector<CNode *>::iterator  
                  
                           ppoChild2 = (*ppoChild)->_vpoChildren.begin();
                           ppoChild2 != (*ppoChild)->_vpoChildren.end();
                           ++ppoChild2 )
                  {
                     SetIntersection( (*ppoChild2)->_csetConstraints, 
                                      _csetPromotableConstraints, csetDoomed );

                     (*ppoChild2)->_csetConstraints -= _csetPromotableConstraints;
                  }

                  AndCut( *ppoChild );

                  ppoChild = poCurrentNode->_vpoChildren.begin();
                  break;

            case  kePromoteConstraintsAndDisconnect :

                  poCurrentNode->_csetConstraints.UnionWith( _csetPromotableConstraints );

                  csetHandle.UnionWith( csetResult );

                  AndCut( *ppoChild );

                  ppoChild = poCurrentNode->_vpoChildren.begin();

                  ReleaseTree( *ppoChild );

                  ppoChild = poCurrentNode->_vpoChildren.erase( ppoChild );

                  if ( poCurrentNode->_vpoChildren.size() == 0 )
                  {
                     if ( poCurrentNode->_csetConstraints.Cardinality() == 0 )
                     {
                        return keDisconnect;
                     }
                     else if ( poCurrentNode->_csetConstraints.Cardinality() == 1 )
                     {
                        return keKeepNewTerminalUnit;
                     }
                  }
                  break;
         }
      }

      OrCut( poCurrentNode );
   }
   while ( poCurrentNode->_csetConstraints != csetPrevious );

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Detect zero-constraint subsumption by the current node
   //
   ///////////////////////////////////////////////////////////////////////////

   if ( poCurrentNode->_vpoChildren.size() == 0  &&  
        ZeroConstraints( poCurrentNode ) )
   {
      return keDisconnect;
   }

   return keKeep;
}

EReductionSignal
CBooleanExpression::
OrReduceToElegance( IN     CNode *            poCurrentNode,
                    INOUT  CConstraintSet &   rcsetDominant,
                    INOUT  CConstraintSet &   rcsetSide )
{
   CConstraintSet   csetLocalSide;
   CConstraintSet   csetResult;

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Reduce each child's subtree
   //
   ///////////////////////////////////////////////////////////////////////////

   for ( std::vector<CNode *>::iterator  
   
            ppoChild = poCurrentNode->_vpoChildren.begin();
            ppoChild != poCurrentNode->_vpoChildren.end();
       )
   {
      ///////////////////////////////////////////////////////////////////////
      //
      //  Construct the local side sets for the current child
      //
      ///////////////////////////////////////////////////////////////////////

      csetLocalSide = rcsetSide;

      for ( std::vector<CNode *>::iterator  
      
               ppoChild2 = poCurrentNode->_vpoChildren.begin();
               ppoChild2 != poCurrentNode->_vpoChildren.end();
               ++ppoChild2 )
      {
         if ( ppoChild2 != ppoChild  &&  (*ppoChild2)->_vpoChildren.size() == 0  &&  
              OneConstraint( *ppoChild2 ) )
         {
            csetLocalSide.UnionWith( (*ppoChild2)->_csetConstraints );
         }
      }

      if ( ! csetLocalSide.IsConsistent() )
      {
         return keDisconnect;
      }

      ///////////////////////////////////////////////////////////////////////
      //
      //  Reduce the child's subtree
      //
      ///////////////////////////////////////////////////////////////////////

      switch ( AndReduceToElegance ( *ppoChild, rcsetDominant, csetLocalSide ) )
      {
         case  keDelete :

               if ( poCurrentNode->_vpoChildren.size() > 1 )
               {
                  ReleaseTree( *ppoChild );

                  ppoChild = poCurrentNode->_vpoChildren.erase( ppoChild );
               }
               else
               {
                  return keDelete;
               }
               break;

         case  keDisconnect :

               return  keDisconnect;

         case  keKeep :

               ++ppoChild;
               break;

         case  keKeepNewTerminalUnit :

               ppoChild = poCurrentNode->_vpoChildren.begin();
               break;
      }
   }

   ///////////////////////////////////////////////////////////////////////////
   //
   //  Detect promotability of constraints
   //
   ///////////////////////////////////////////////////////////////////////////

   _csetPromotableConstraints.SetAllElements();

   for ( ppoChild = poCurrentNode->_vpoChildren.begin();
         ppoChild != poCurrentNode->_vpoChildren.end();
         ++ppoChild )
   {
      _csetPromotableConstraints.IntersectWith( (*ppoChild)->_csetConstraints );
   }

   if ( _csetPromotableConstraints.Cardinality() > 0 )
   {
      for ( ppoChild = poCurrentNode->_vpoChildren.begin();
            ppoChild != poCurrentNode->_vpoChildren.end();
            ++ppoChild )
      {
         if ( (*ppoChild)->_csetConstraints == _csetPromotableConstraints )
         {
            return kePromoteConstraintsAndDisconnect;
         }
      }

      return kePromoteConstraints;
   }
   else
   {
      return keKeep;
   }
}

void
CBooleanExpression::
AdoptGreatGrandchildren( IN   CNode *   poNode,
                         IN   CNode *   poDoomedChild,
                         IN   CNode *   poDoomedGrandchild )
{
   std::vector<CNode *>   vpoOriginalChildren;

   vpoOriginalChildren.insert( vpoOriginalChildren.end(), 
                               poNode->_vpoChildren.begin(), 
                               poNode->_vpoChildren.end() );

   poNode->_vpoChildren.clear();

   poNode->_vpoChildren.reserve( vpoOriginalChildren.size() - 1 + 
                                  poDoomedGrandchild->_vpoChildren.size() );

   for ( std::vector<CNode *>::iterator  
   
            ppoChild = vpoOriginalChildren.begin();
            ppoChild != vpoOriginalChildren.end();
            ++ppoChild )
   {
      if ( *ppoChild == poDoomedChild )
      {
         for ( std::vector<CNode *>::iterator  
         
            ppoGreatGrandchild = poDoomedGrandchild->_vpoChildren.begin();
            ppoGreatGrandchild != poDoomedGrandchild->_vpoChildren.end();
            ++ppoGreatGrandchild )
         {
            poNode->_vpoChildren.push_back( *ppoGreatGrandchild );
         }
      }
      else
      {
         poNode->_vpoChildren.push_back( *ppoChild );
      }
   }

   poDoomedGrandchild->_vpoChildren.clear();
}


EReductionSignal
CBooleanExpression::
AndCut( IN  CNode *     poCurrentNode )
{
   CNode *            poPreviousChild  =  NULL;
   EReductionSignal   result           =  keKeep;
   CNode *            poTempNode       =  NULL;

   for ( std::vector<CNode *>::iterator  
   
            ppoChild = poCurrentNode->_vpoChildren.begin();
            ppoChild != poCurrentNode->_vpoChildren.end();
       )
   {
      if ( ZeroConstraints( *ppoChild )  &&  
           (*ppoChild)->_vpoChildren.size() == 1 )
      {
         CNode *   poDoomedChild  =  *ppoChild;

         ppoChild = poCurrentNode->_vpoChildren.erase( ppoChild );

         CNode *   poDoomedGrandchild = poDoomedChild->_vpoChildren[0];

         for ( std::vector<CNode *>::iterator  
         
            ppoGreatGrandchild = poDoomedGrandchild->_vpoChildren.begin();
            result != keDisconnect  &&  
               ppoGreatGrandchild != poDoomedGrandchild->_vpoChildren.end();
            ++ppoGreatGrandchild )
         {
            if ( (*ppoGreatGrandchild)->_vpoChildren.size() == 0 )
            {
               switch ( (*ppoGreatGrandchild)->_csetConstraints.Cardinality() )
               {
                  case 0 :  result = keDisconnect;
                            break;

                  case 1 :  result = keKeepNewTerminalUnit;
                            break;
               }
            }
         }

         AdoptGreatGrandchildren( poCurrentNode, poDoomedChild, poDoomedGrandchild );

         delete poDoomedGrandchild;
         poDoomedGrandchild = NULL;

         delete poDoomedChild;
         poDoomedChild = NULL;

         ppoChild = poCurrentNode->_vpoChildren.begin();
      }
      else
      {
         ++ppoChild;
      }
   }

   return result;
}

EReductionSignal
CBooleanExpression::
InconsistentHandle( IN     CNode *            kpoCurrentNode,
                    INOUT  CConstraintSet &   rcsetDominant,
                    INOUT  CConstraintSet &   rcsetHandle )
{
   SetUnion( kpoCurrentNode->_csetConstraints, rcsetDominant, rcsetHandle );

   bool  bConsistentHandle  =  rcsetHandle.IsConsistent();

   if ( ! bConsistentHandle )
   {
      _bDeleteDueToInconsistentHandle = true;
   }

   return bConsistentHandle ? keKeep : keDelete;
}

void
CBooleanExpression::
OrCut( IN  CNode *     poCurrentNode )
{
   for ( std::vector<CNode *>::iterator  
   
            ppoChild = poCurrentNode->_vpoChildren.begin();
            ppoChild != poCurrentNode->_vpoChildren.end();
       )
   {
      if ( (*ppoChild)->_vpoChildren.size() == 1 )
      {
         CNode *   poDoomedChild  =  *ppoChild;

         CNode *   poDoomedGrandchild  =  poDoomedChild->_vpoChildren[0];

         AdoptGreatGrandchildren( poCurrentNode, poDoomedChild, poDoomedGrandchild );

         poCurrentNode->_csetConstraints.UnionWith( poDoomedGrandchild->_csetConstraints );

         delete poDoomedGrandchild;
         poDoomedGrandchild = NULL;

         delete poDoomedChild;
         poDoomedChild = NULL;

         ppoChild = poCurrentNode->_vpoChildren.begin();
      }
      else
      {
         ++ppoChild;
      }
   }
}

long
CBooleanExpression::
ReleaseTree( IN  CNode *    poCurrentNode )
{
   long   liNumLiteralsReleased  =  0;

   for ( std::vector<CNode *>::iterator  
   
            ppoChild = poCurrentNode->_vpoChildren.begin();
            ppoChild != poCurrentNode->_vpoChildren.end();
            ++ppoChild )
   {
      liNumLiteralsReleased += ReleaseTree( *ppoChild );
   }

   poCurrentNode->_vpoChildren.clear();

   if ( poCurrentNode->_entType == keAnd )
   {
      liNumLiteralsReleased += poCurrentNode->_csetConstraints.Cardinality();
   }

   delete poCurrentNode;

   return liNumLiteralsReleased;
}
 

          First in thread      Previous in thread      Next in thread

 
 
 
  Home > Jabberwocky           Previous      Next
 
  Craig Holman   Research   Jabberwocky   Quotations   Contact  
 
 
 
  Patterncraft™ and Constraint and Consequence™
are trademarks of Craig Stewart Holman

Copyright © 2008 Craig Stewart Holman

Copyright and Legal Notices

All Rights Reserved.

 
   
 
  Patterncraft logo