2-Sat 구현을 본 사람이 누구입니까

Question

잠시 동안 찾고 있었지만 2-Sat 알고리즘의 구현을 찾을 수없는 것 같습니다.

내가 (A strongly connected component module있다) 부스트 라이브러리와 C++에서 작업 나 C++를 사용하는 기존 라이브러리에 몇 가지 지침이 필요하거나 효율적인 2 토 프로그램을 만들거나 찾을 수 있어요.

Answer 1

SCC로 문제를 해결하기 위해 2-Sat 문제를 모델링하는 방법을 알고 있다고 가정합니다. 나는 vars와 그것의 부정을 다루는 방법이 매우 우아하지는 않지만 짧은 구현을 허용한다 : 0에서 n-1까지의 n 개의 변수가 주어진다면, 절에서 -i는 변수 i의 부정을 의미하고 그래프 i + n은 같은 의미입니다 (명확합니까?)

#include <boost/config.hpp> 
#include <iostream> 
#include <vector> 
#include <boost/graph/strong_components.hpp> 
#include <boost/graph/adjacency_list.hpp> 
#include <boost/foreach.hpp> 

typedef std::pair<int, int> clause; 

//Properties of our graph. By default oriented graph 
typedef boost::adjacency_list<> Graph; 


const int nb_vars = 5; 

int var_to_node(int var) 
{ 
    if(var < 0) 
     return (-var + nb_vars); 
    else 
     return var; 
} 

int main(int argc, char ** argv) 
{ 
    std::vector<clause> clauses; 
    clauses.push_back(clause(1,2)); 
    clauses.push_back(clause(2,-4)); 
    clauses.push_back(clause(1,4)); 
    clauses.push_back(clause(1,3)); 
    clauses.push_back(clause(-2,4)); 

    //Creates a graph with twice as many nodes as variables 
    Graph g(nb_vars * 2); 

    //Let's add all the edges 
    BOOST_FOREACH(clause c, clauses) 
    { 
     int v1 = c.first; 
     int v2 = c.second; 
     boost::add_edge(
       var_to_node(-v1), 
       var_to_node(v2), 
       g); 

     boost::add_edge(
       var_to_node(-v2), 
       var_to_node(v1), 
       g); 
    } 

    // Every node will belong to a strongly connected component 
    std::vector<int> component(num_vertices(g)); 
    std::cout << strong_components(g, &component[0]) << std::endl; 

    // Let's check if there is variable having it's negation 
    // in the same SCC 
    bool satisfied = true; 
    for(int i=0; i<nb_vars; i++) 
    { 
     if(component[i] == component[i+nb_vars]) 
      satisfied = false; 
    } 
    if(satisfied) 
     std::cout << "Satisfied!" << std::endl; 
    else 
     std::cout << "Not satisfied!" << std::endl; 
}