//
//  StConn - Version 1.1 - October 19, 2023
//
// Author: Sam Buss
//
// Generate CNF instances of the StConn tautologies.
//
// See S. Buss, "Polynomial-Size Frege and Resolution Proofs 
//    of st-Connectivity and Hex Tautologies", 
//    Theoretical Computer Science 357, 1 - 3 (2006) 35 - 52.
// The output encodes the STCONN^c CNF formula of that paper.
// 
// Command line syntax:
// 
//    % StConn <d> <n>
//
// Parameters: 
//     d - width of the grid graph.
//     n - lengths of the grid graph.
// Variables 
//     r_e  - Edge e is red. 
//     b_e  - Edge e is blue.
//     Total of (n-1)(d-1) edges.
//
// Code is supplied as-is, without warranties of
//   suitablility or correctness. It may be used
//   freely. It is appreciated if use is acknowledged.
//   If the code is modified, it is suggested to change
//   the file names to avoid confusing among versions.
//

#define _CRT_SECURE_NO_WARNINGS
#include <stdio.h>
#include <assert.h>
#include <vector>

// Function prototypes
void StConnCnf();
void BuildStConnCnf();
void PrintStConnCnf();
int VarIndex(int color, int i, int j, int direction);
int VarForced(int color, int i, int j, int direction);
void VarCanonical(int i, int j, int direction, int& ileft, int& jdown, int& iright, int& jup);
void AddLiteral(int color, int i, int j, int direction, bool polarity);
void FinalizeClause();
void PrintHelpMsg();

const int colorRed = 0;
const int colorBlue = 1;

// **************************
// Global data for StConn
// **************************

int d;      // Width of the grid graph
int n;      // Length of the grid graph
int numVariables;
int numClauses;

std::vector<int> CnfClauseData;
int clauseStatus = 0;           // Running number of literals in the current clause
bool clauseHasTrueLit = false;  // If true, this clause can be dropped.

int main( int argc, char* argv[] ) {
#if 1
    if (argc != 3) {
        PrintHelpMsg();
        return 0;
    }
    sscanf(argv[1], "%d", &d);  // Width d
    sscanf(argv[2], "%d", &n);  // Length n
    if (!(d > 1 && n > 2)) {
        PrintHelpMsg();
        return 0;
    }
#else
    d = 3;
    n = 4;
#endif
    StConnCnf();
    return 1;
}

void PrintHelpMsg() {
    fprintf(stderr, "StConn: Generate StConn Grid Graph tautologies.\n\n");
    fprintf(stderr, "Usage: StConn <width> <length>\n\n");
    fprintf(stderr, "where <width> and <length> are the width and length (in vertices) of the grid.\n");
}

void StConnCnf() {
    BuildStConnCnf();
    PrintStConnCnf();
}

void BuildStConnCnf() {
    assert(d >= 2 && n >= 3);
    numVariables = 2 * (2 * d * n - d - n - 4);
    numClauses = 0;
    CnfClauseData.clear();

    // Output all clauses that concern edges that share a (single) common endpoint
    for (int i = 0; i < n; i++) {
        for (int j = 0; j < d; j++) {
            // Consider all edges, red or blue, that touch vertex (i,j).
            for (int c = 0; c < 2; c++) {
                // Consider all incident edges of color c
                // Output the clauses that state zero or two of them are present.
                // First, four clauses stating that at most two edges present
                // Second, four clauses stating that not exactly one edge of four is present
                for (int dir = 0; dir < 4; dir++) {
                    for (int dir2 = 0; dir2 < 4; dir2++) {
                        if (dir2 != dir) {
                            AddLiteral(c, i, j, dir2, false);
                        }
                    }
                    FinalizeClause();   // At most two of the four edges are present
                    for (int dir2 = 0; dir2 < 4; dir2++) {
                        AddLiteral(c, i, j, dir2, dir!=dir2);
                    }
                    FinalizeClause();   // Not exactly one of the four edges is present.
                }
            }
        }
    }
    // Add clauses saying that blue and red version of edge are not both present
    // And clauses that blue abd red edges sharing exactly one common vertex are not present
    for (int i = 0; i < n; i++) {
        for (int j = 0; j < d; j++) {
            for (int dir = 0; dir < 2; dir++) {
                // The red and blue edges in direction dir cannot both be present.
                // (These clauses could be omitted w.l.o.g.)
                AddLiteral(0, i, j, dir, false);
                AddLiteral(1, i, j, dir, false);
                FinalizeClause();
            }
            // Next: two opposite color edges that intersect in exactly (i,j) are not present.
            for (int dir = 0; dir < 4; dir++) {
                for (int dir2 = 0; dir2 < 4; dir2++) {
                    if (dir != dir2) {
                        AddLiteral(0, i, j, dir, false);
                        AddLiteral(1, i, j, dir2, false);
                        FinalizeClause();
                    }
                }
            }
        }
    }
}

void PrintStConnCnf() {
    fprintf(stdout, "c\nc StConn grid graph tautology. Width  d=%d; Length n=%d.\nc\n", n, d);
    fprintf(stdout, "p cnf %d %d\n", numVariables, numClauses);
    for (std::vector<int>::iterator it = CnfClauseData.begin(); it < CnfClauseData.end(); it++) {
        if (*it != 0) {
            fprintf(stdout, "%d ", *it);
        }
        else {
            fprintf(stdout, "0\n");
        }
    }
}

void AddLiteral(int color, int i, int j, int direction, bool polarity) {
    // Check if literal forced.  If so, either abort clause or skip literal
    // Add literal's signed index - push to vector<int>
    // Increment count of literals in clause
    int forced = VarForced(color, i, j, direction);
    if (forced) {
        if ((forced == 1) == polarity) {
            clauseHasTrueLit = true;    // Clause will be discarded
        }
        return;
    }
    int varIndex = VarIndex(color, i, j, direction);
    CnfClauseData.push_back(polarity ? varIndex : -varIndex);  // Add the literal to the clause
    clauseStatus++;         // Increment number of literals in current clause
}

void FinalizeClause() {
    // If clause is aborted (i.e., forced true), remove it from the CnfClauseData
    // Otherwise, add a "0" to terminate the clause. 
    // Increment number of clauses
    if (clauseHasTrueLit) {
        for (int i = 0; i < clauseStatus; i++) {
            CnfClauseData.pop_back();
        }
        clauseHasTrueLit = false;
    }
    else {
        CnfClauseData.push_back(0);
        numClauses++;
    }
    clauseStatus = 0;
}


// ***********************************
// VarIndex - Calculate the index of a variable
//   color - 0 for red, 1 for blue
//   i,j - one endpoint of the edge
//   direction - 0, 1, 2, 3 for up, right, down, left
// Return
//   An index of the edge. rangles from 1 to 2*(d-1)(n-1)-8
// ***********************************
int VarIndex(int color, int i, int j, int direction) {
    int iright, ileft, jdown, jup;
    VarCanonical(i, j, direction, ileft, jdown, iright, jup);
    direction = direction & 0x01;   // Make direction up (0) or left (1).
    assert(!VarForced(color, ileft, jdown, direction));

    int displacement = 0;
    if (color == colorRed) {
        displacement = 2*d*n - d - n - 4;   // Number of indices needed for blue edges
        int temp = jdown;
        jdown = d - 1 - jup;                  // Flip upside down (red/blue vertical anti-symmetry)
        jup = d - 1 - temp;
    }
    int idx;
    if (direction == 1) {
        // Horizontal edge
        idx = jdown * (n - 1) + ileft;
    }
    else {
        // Vertical edge
        idx = jdown * n + ileft + (d * n - d - 2);
    }
    return idx + displacement;
}


// ***********************************
// VarForced - Calculate whether a variable is forced.
//   color - 0 for red, 1 for blue
//   i,j - one endpoint of the edge
//   direction - 0, 1, 2, 3 for up, right, down, left
// Return
//   0 - variable is not forced
//   1 - variable is forced true
//  -1 - variable is forced false.
// Variables which are forced do *not* get included in
// the CNF.  (Not even in unit clauses.) They are just discarded.
// ***********************************
int VarForced(int color, int i, int j, int direction) {
    int iright, ileft, jdown, jup;
    VarCanonical(i, j, direction, ileft, jdown, iright, jup);
    direction = direction & 0x01;   // Make direction up (0) or left (1).
    if (color == colorBlue) {
        if ((ileft == 0 && jdown == 0) || (iright == n - 1 && jup == d - 1)) {
            return -1;      // Blue edge forced false (Intersects start/end of red path)
        }
        if (((ileft == -1 && jdown == d - 1) || (ileft == n - 1 && jdown == 0)) && direction == 1) {
            return 1;       // Blue edge forced true (past the start/end of blue path)
        }
    }
    else {   // Color is red 
        if ((ileft == 0 && jup == d - 1) || (iright == n - 1 && jdown == 0)) {
            return -1;      // Red edge forced false (Intersects start/end of blue path)
        }
        if (((ileft == -1 && jdown == 0) || (ileft == n - 1 && jdown == d - 1)) && direction == 1) {
            return 1;       // Red edge forced true (past the start/end of red path)
        }
    }
    if (ileft == -1 || iright == n || jdown == -1 || jup == d ) {
        return -1;       // Edge outside grid is forced false
    }
    return 0;        // Interior edge not forced true or false.
}

//}
//
//// *********************************************
//// Return edge in canonical representation.
////    From left to right, from below to above
////    iright <= ileft and jdown <= jup will hold upon return.
//// *********************************************
void VarCanonical( int i, int j, int direction, int& ileft, int& jdown, int& iright, int& jup ) {
    switch (direction) {
    case 0:  // Edge direction is upward (postive j direction)
        ileft = i;
        iright = i;
        jdown = j;
        jup = j + 1;
        break;
    case 1:   // Edge direction is rightward (positive i direction)
        ileft = i;
        iright = i + 1;
        jdown = j;
        jup = j;
        break;
    case 2:  // Edge direction is downward (negative j direction)
        ileft = i;
        iright = i;
        jdown = j - 1;
        jup = j;
        break;
    case 3:   // Edge direction is leftward (negative i direction)
        ileft = i - 1;
        iright = i;
        jdown = j;
        jup = j;
        break;
    }
}