Кто-нибудь видел реализацию 2-Sat

Question

Я искал некоторое время, но я просто не могу найти какую-либо реализацию алгоритма 2-Sat.

Я работаю в C++ с библиотекой boost (которая имеет сильно связанный компонентный модуль), и мне нужно некоторое руководство, чтобы создать эффективную 2-Sat программу или найти существующую библиотеку, которую я мог бы использовать через C++.

Answer 1

Я полагаю, вы знаете, как смоделировать задачу 2-Sat, чтобы решить ее с помощью SCC. То, как я обрабатываю vars и его отрицание, не очень элегантно, но допускает короткую реализацию: учитывая n переменных, пронумерованных от 0 до n-1, в пунктах -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;
}