#include <vector>
#include <utility>

typedef std::pair<unsigned int, unsigned int> RelationElement;
typedef std::vector<RelationElement> Relation;

typedef std::vector<int> Clause;
typedef std::vector<Clause> Cnf;

// All following functions are to solve the following task.
// Given a binary relation R over Z_n, decide if there are 8 relations 
// R1, R2, R3, R4, R5, R6, R7, R8 such that R is their union and
// all there relations satisfy:
// \forall x \forall y \forall z (Ri(x,y) & Ri(x,z) -> Ri(y,z))
// Your task is to implement the following three functions.


// 1. This function uses any trivial algorithm.
bool decomposeRelationTrivial(const Relation&, unsigned int n);

// 2. This function creates a simple reformulation of the problem as CNF-SAT.
// Keep things simple.
Cnf decomposeRelationToCNFNonBinary(const Relation&, unsigned int n);

// 3. This function creates a reformulation of the problem as CNF-SAT.
// Make this as fast as possible. To evaluate the speed of your solution,
// I will use minisat. Inputs generated by the procedure defined bellow 
// - n varies
// - p will be chosen depending on n so that the procedure generates rougly 
//   equal ratios of SAT and UNSAT instances given various random seeds.
// - seed varies :)
Cnf decomposeRelationToCNFBest(const Relation&, unsigned int n);

// Test inputs (generated by the procedure below):
// Seed: 1 - SATISFIABLE
// Seed: 2 - SATISFIABLE
// Seed: 3 - UNSATISFIABLE
// Seed: 4 - UNSATISFIABLE
// Seed: 5 - UNSATISFIABLE
// Seed: 6 - SATISFIABLE
// Seed: 7 - UNSATISFIABLE
// Seed: 8 - UNSATISFIABLE
// Seed: 9 - UNSATISFIABLE
// Seed:10 - UNSATISFIABLE

// Generating procedure (requires #include <random>):
/*
    const unsigned int n=25;    
    const unsigned int p=2000; // probability p/10000
    
    std::mt19937 gen(seed); //set seed
    std::uniform_int_distribution<> distrib(0, 9999);

    Relation r;
    for(int i=0; i<n; i++) {
        for(int j=0; j<n; j++) {
            if (i==j || distrib(gen)<p) {
                r.emplace_back(i, j);
            }
        }
    }
*/