SAT.cpp

#include "SAT.hpp"

/// Constructs an random K-SAT instance
SAT::SAT(int N, int M, int k, std::mt19937 &rng)
            : clauses(M),
              N(N),
              M(M),
              k(k)
{
    std::uniform_int_distribution<int> uniform(1, N);
    std::uniform_real_distribution<double> uniform_real(0, 1);

    for(int m=0; m<M; ++m)
    {
        Clause c(k);
        for(int i=0; i<k; ++i)
        {
            int v;
          
            // variables should not occur twice
            do
            {
                v = uniform(rng);
            } while(c.contains(v));
          
            // negated with 50% chance
            if(uniform_real(rng) > 0.5)
                v *= -1;
          
            c.variables[i] = v;
        }
        clauses[m] = c;
    }
}

/// prints the representation of the K-SAT instance
void SAT::print()
{
    for(int j=0; j<M; ++j)
    {
        std::cout << "(";
        for(int i=0; i<k; ++i)
        {
            auto &clause = clauses[j];
            auto var = std::abs(clause.variables[i]);
            if(clause.variables[i] < 0)
                std::cout << "!";
            std::cout << "x_" << var;
            if(i != k-1)
                std::cout << " ∧ ";
        }
        if(j != M-1)
            std::cout << ") v ";
        else
            std::cout << ")";
    }
    std::cout << std::endl;
}

/// prints the representation of the K-SAT instance in DIMACS format
std::string SAT::dimacs()
{
    std::stringstream ss;

    ss << "c My Problem\n";
    ss << "p cnf " << N << " " << M << "\n";
    for(auto c : clauses)
    {
        for(auto v : c.variables)
            ss << v << " ";
        ss << "0\n";
    }

    return ss.str();
}

SAT.hpp

#include <vector>
#include <random>

class Clause
{
    public:
        Clause() {};
        Clause(int k)
            : variables(k, 0),
              k(k)
        {
        };

        std::vector<int> variables;
        int k;

        // this should be pretty fast since k is fairly small
        bool contains(int v)
        {
            for(auto t : variables)
                if(std::abs(v) == std::abs(t))
                    return true;
            return false;
        };
};

class SAT
{
    public:
        SAT(int N, int M, int k, std::mt19937 &rng);

        std::vector<Clause> clauses;
        int N;
        int M;
        int k;

        void print();
        std::string dimacs();
};