2-CNF-SAT问题图形解法的C++实现

struct Literal
{
    Literal() : pSmbl(0) {}
 
    Literal(Symbol* pSymbol, bool isNotSymbol)
        : pSmbl(pSymbol), isNotSmbl(isNotSymbol)
    {}
 
    bool Value() const
    { return isNotSmbl ? !pSmbl->value : pSmbl->value; }
 
    Literal operator!() const
    { return Literal(pSmbl, !isNotSmbl); }
 
 
    Symbol* pSmbl;
    bool isNotSmbl;
 
friend bool FindSCCAndCheckSatisfiability(LtrlGraph& transGraph, std::vector<StrCnnCmpnt>& sccs);
private:
    bool SetSymbolValue(StrCnnCmpnt *pSCC);
};
 
////////////////////////////////////
struct Clause
{
    Clause(Literal const& literal1, Literal const& literal2, size_t numDummyLiterals)
        : numDummyLtrl(numDummyLiterals)
    {
        ltrls&#91;0] = literal1;
        ltrls&#91;1] = literal2;
    }
    Literal ltrls&#91;2];
    size_t numDummyLtrl;
};
 
struct TwoCNF
{
    std::vector<Clause> clauses;
    std::set<Symbol> symbols;
    std::vector<Symbol*> dummySmbls;
}; 

/////////////////////////////////////////
struct Node
{
    Node(Literal const& literal) : state(UNSEARCHED), ltrl(literal), pNewNode(0) {}
    Node(Node const& other) : state(UNSEARCHED), tBgnSrch(other.tBgnSrch),
        tEndSrch(other.tEndSrch), ltrl(other.ltrl), pNewNode(0)
    {}
 
    enum STATE { SEARCHED, SEARCHING, UNSEARCHED } state;
    size_t tBgnSrch, tEndSrch;
    Literal ltrl;
    std::vector<Node*> cnnNodes;
 
friend void TransposeAndSortGraph(LtrlGraph& graph, LtrlGraph& transGraph);
private:
    Node *pNewNode; //Used for transposing the graph
};
 
struct LtrlGraph
{
    std::list<Node> nodes;
}; 

void DepthFirstSearch(LtrlGraph& graph)
{
    InitNodesState(graph);
 
    stack<Node*> searchNodes;
 
    size_t time = 0;
    for (list<Node>::iterator itorNode = graph.nodes.begin();
        itorNode != graph.nodes.end(); ++itorNode)
    {
        Node& node = *itorNode;
        if (node.state != Node::UNSEARCHED)
            continue;
 
        searchNodes.push(&node);
        while (!searchNodes.empty())
        {
            Node& node = *searchNodes.top();
            if (node.state == Node::UNSEARCHED)
            {
                node.state = Node::SEARCHING;
                node.tBgnSrch = ++time;
                for (vector<Node*>::iterator itorCnnNode = node.cnnNodes.begin();
                    itorCnnNode != node.cnnNodes.end(); ++itorCnnNode)
                {
                    Node *pCnnNode = *itorCnnNode;
                    if (pCnnNode->state == Node::UNSEARCHED)
                        searchNodes.push(pCnnNode);
                }
            }
            else if (node.state == Node::SEARCHING)
            {
                node.state = Node::SEARCHED;
                node.tEndSrch = ++time;
                searchNodes.pop();
            }
            else
            {
                //The node has already been searched, just pop it from the stack
                searchNodes.pop();
            }
        }
    }
} 

struct SortingNode
{
    SortingNode(size_t endSearchTime, Node *pOrgNode)
        : tEndSrch(endSearchTime), pNode(pOrgNode)
    {}
 
    size_t tEndSrch;
    Node *pNode;
};
 
inline bool GreaterEndSearchTime(SortingNode const& n1, SortingNode const& n2)
{
    return n1.tEndSrch > n2.tEndSrch;
}
 
void TransposeAndSortGraph(LtrlGraph& graph, LtrlGraph& transGraph)
{
    //Sort nodes by their end search time
    vector<SortingNode> sortingNodes;
    for (list<Node>::iterator itorNode = graph.nodes.begin();
        itorNode != graph.nodes.end(); ++itorNode)
    {
        Node& node = *itorNode;
        sortingNodes.push_back(SortingNode(node.tEndSrch, &node));
    }
    sort(sortingNodes.begin(), sortingNodes.end(), &GreaterEndSearchTime);
 
    //Add new nodes in the transposed graph
    for (vector<SortingNode>::iterator itorSN = sortingNodes.begin();
        itorSN != sortingNodes.end(); ++itorSN)
    {
        transGraph.nodes.push_back(*(itorSN->pNode));
        itorSN->pNode->pNewNode = &transGraph.nodes.back();
    }
 
    //Transpose the graph
    for (list<Node>::iterator itorNode = graph.nodes.begin();
        itorNode != graph.nodes.end(); ++itorNode)
    {
        Node& node = *itorNode;
        for (vector<Node*>::iterator itorCnnNode = node.cnnNodes.begin();
            itorCnnNode != node.cnnNodes.end(); ++itorCnnNode)
        {
            Node* pCnnNode = *itorCnnNode;
            pCnnNode->pNewNode->cnnNodes.push_back(node.pNewNode);
        }
    }
} 

//Strongly Connected Component
struct StrCnnCmpnt
{
    size_t rank;
    std::vector<Literal> literals;
};
  
bool FindSCCAndCheckSatisfiability(LtrlGraph& transGraph, vector<StrCnnCmpnt>& sccs)
{
    stack<Node*> searchNodes;
    size_t strCnnCmptRank = 0;  //Lower number means higher rank
    for (list<Node>::iterator itorNode = transGraph.nodes.begin();
        itorNode != transGraph.nodes.end(); ++itorNode)
    {
        Node& node = *itorNode;
        if (node.state != Node::UNSEARCHED)
            continue;
 
        //Create a strong connected component
        sccs.push_back(StrCnnCmpnt());
        StrCnnCmpnt& scc = sccs.back();
        scc.rank = ++strCnnCmptRank;
 
        searchNodes.push(&node);
        while (!searchNodes.empty())
        {
            Node& node = *searchNodes.top();
            if (node.state == Node::UNSEARCHED)
            {
                node.state = Node::SEARCHING;
                for (vector<Node*>::iterator itorCnnNode = node.cnnNodes.begin();
                    itorCnnNode != node.cnnNodes.end(); ++itorCnnNode)
                {
                    Node *pCnnNode = *itorCnnNode;
                    if (pCnnNode->state == Node::UNSEARCHED)
                        searchNodes.push(pCnnNode);
                }
            }
            else if (node.state == Node::SEARCHING)
            {
                node.state = Node::SEARCHED;
                if (!node.ltrl.SetSymbolValue(&scc))
                //A symbol and its complement is in the same strong connected component,
                //Therefore the symbol value is undefined. No solution is available.
                    return false;
                else
                    scc.literals.push_back(node.ltrl);
                searchNodes.pop();
            }
            else
            {
                searchNodes.pop();
            }
        }
    }
    return true;
} 

bool Literal::SetSymbolValue(StrCnnCmpnt *pSCC)
{
    assert(pSCC != 0 && (pSmbl->cntSCC.pSCC == 0 || pSmbl->cntSCC.pNotSCC == 0));
 
    Symbol::ContainingSCC& cntSCC = pSmbl->cntSCC;
    if (cntSCC.pSCC == 0 && cntSCC.pNotSCC == 0)
    //The first time this symbol is checked
    {
        if (isNotSmbl)
        {
            pSmbl->value = true;
            cntSCC.pNotSCC = pSCC;
        }
        else
        {
            pSmbl->value = false;
            cntSCC.pSCC = pSCC;
        }
        return true;
    }
    else //The second time this symbol is checked
    {
        isNotSmbl ? (cntSCC.pNotSCC = pSCC) : (cntSCC.pSCC = pSCC);
        return cntSCC.IsNotSameSCC();
    }
}