c++boostimplementation2-satisfiability

Has anyone seen a 2-Sat implementation


I have been looking for a while, but I just can't seem to find any implementation of the 2-Sat algorithm.

I am working in c++ with the boost library (which has a strongly connected component module) and need some guidance to either create an efficient 2-Sat program or find an existing library for me to utilise through c++.


Solution

  • I suppose you know how to model a 2-Sat problem to solve it with SCC. The way I handle vars and its negation isn't very elegant, but allows a short implementation: Given n variables numbered from 0 to n-1, in the clauses -i means the negation of variable i, and in the graph i+n means the same (am I clear ?)

    #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;
    }