Troubleshooting Hamiltonian path to SAT

  c++

I’m not sure if this question should be asked here but it is my last resort, also first time on Stackoverflow. I have very little experience coding and I’m currently doing an Algorithm specialization in Coursera. The exercise is, given a graph, reducing a Hamiltonian path problem to a SAT problem, which then they evaluate using a minisat solver (http://minisat.se/). The code below (about 95% me, they provide a starter file) passes a few of their tests but eventually fails (Note: this code actually runs minisat, the one I submitted prints to the terminal). They don’t provide the input for the test case that failed or the expected answer, it just says Wrong Answer.

I have tested with a few graphs and it works. I’ve also tried stress testing my solution against a non-SAT implementation found online ( https://cppsecrets.com/users/22319897989712197103975756505164103109971051084699111109/Hamiltonian-Path.php), but so far they always agree. I could add the code for that if needed.

Are there any fringe test cases that I should consider? What am I missing? I know this is not a general programming question but I’m going bananas and I can’t move forward unless I pass the exercise.

Thanks


#include <ios>
#include <iostream>
#include <fstream>
#include <vector>
#include <string>

/*
    Converts a graph G with n vertices and m edges into a series of booleans to evaluate whether a Hamiltonian
    path exists. It then uses minisat solver (http://minisat.se/) to evaluate the clauses and return either SAT
    if there is a path or UNSAT if no path exists.

    This is part of a coursera assigment with the description below. The only difference is that instead of printing 
    the clauses to the terminal, I'm actually running minisat.

    Input Format. The first line contains two integers 𝑛 and π‘š β€” the number of rooms and the number of corridors 
    connecting the rooms respectively. Each of the next π‘š lines contains two integers 𝑒 and 𝑣 describing the corridor 
    going from room 𝑒 to room 𝑣. The corridors are two-way, that is, you can go both from 𝑒 to 𝑣 and from 𝑣 to 𝑒. No 
    two corridors have a common part, that is, every corridor only allows you to go from one room to one other room. 
    Of course, no corridor connects a room to itself. Note that a corridor from 𝑒 to 𝑣 can be listed several times, and 
    there can be listed both a corridor from 𝑒 to 𝑣 and a corridor from 𝑣 to 𝑒.

    Constraints. 1 ≀ 𝑛 ≀ 30;0 ≀ π‘š ≀ 𝑛(π‘›βˆ’1);1 ≀ 𝑒,𝑣 ≀ 𝑛.

    Output Format. You need to output a boolean formula in the CNF form in a specific format. If it is possible to go 
    through all the rooms and visit each one exactly once to clean it, the formula must be satisfiable. Otherwise, the 
    formula must be unsatisfiable. The sum of the numbers of variables used in each clause of the formula must not exceed 
    120 000.

*/

using namespace std;

typedef vector<vector<int>> Matrix;

string FILE_IN = "apartment_cnf.txt";
string FILE_OUT = "apartment_out.txt";

struct ConvertHampathToSat {
    int numVertices;
    int numEdges;
    int repeatedEdges;
    Matrix adj_matrix;

    ConvertHampathToSat(int n, int m) : numVertices(n), numEdges(m) { 
        repeatedEdges = 0;
        adj_matrix.resize(n, vector<int>(n));
    }

    int numeric_Sum(const int n) {
    /*
        Helper function returns the sum of numbers from 0 to n-1.
    */
        int sum = 0;
        for (int i = 0; i < n; i++) {
            sum += i;
        }
        return sum;
    }

    void add_NotEdges(ofstream &cnf, const int f, const vector<int> &t, int &count) {
    /* 
        Adds the clauses for pair of vertices without an edge between them.
        For each pair, it adds one clause for when the from vertex is at the start of path, one clause
        for when it is at the end of path, and two clauses for each position in the middle of path.
    */

        if (t.empty()) { return; }

        /* Converting from vertex number to variable */
        int from = (f - 1) * numVertices + 1;
        vector<int> not_edges;
        for (int to : t) {
            not_edges.push_back((to - 1) * numVertices + 1);
        }
        
        for (int path_pos = 0; path_pos < numVertices; path_pos++) {
            for (int to : not_edges) {
                if (path_pos == 0) {
                    /* from vertex is at start of path */
                    cnf << -(from + path_pos) << ' ' << -(to + path_pos + 1) << ' ' << 0 << endl;
                } else if (path_pos == numVertices - 1) {
                    /* from vertex is at end of path */
                    cnf << -(from + path_pos) << ' ' << -(to + path_pos - 1) << ' ' << 0 << endl;
                } else {
                    /* from vertex is in middle of path */
                    cnf << -(from + path_pos) << ' ' << -(to + path_pos + 1) << ' ' << 0 << endl;
                    cnf << -(from + path_pos) << ' ' << -(to + path_pos - 1) << ' ' << 0 << endl;
                    count++;
                }
                count++;
            }
        }

    }

    void write_ToFile() {
    /* 
        Calculates number of variables and clauses, then writes it out in the format: p cnf variables clauses
        Writes all the clauses in the format required by minisat: 1 -2 -4 0 (1 OR -2 OR -4). All clauses use OR.
        Example: for a graph with 3 edges, variables 1, 2, and 3 represent vertex 1 in path position 1, 2, and 3.
        Variables 1, 4, and 7 represent position 1 occupied by vertex 1, 2, and 3.
    */

        /* Count was added to keep track of the number of clauses when I needed to figure out an equation */
        int count = 0;

        int numberVariables = numVertices * numVertices;
        /* Calculation of total number of clauses 
            First term = Each vertex is in path + each path position has a vertex
            Second term = Each vertex appears only once in path + each path has only one vertex
            Third term =  All possible non edges. */
        int maxEdges = numeric_Sum(numVertices);
        int actual_Edges = numEdges - repeatedEdges;
        int clauses = (2 * numVertices)                                         // First term
                    + (2 * numVertices * numeric_Sum(numVertices))              // Second term
                    + 2 * (numVertices - 1) * (maxEdges - actual_Edges);        // Third term
        

        /* Creating the file */
        ofstream cnf{FILE_IN};

        /* Print out number of variables and number of clauses */
        cnf << "p cnf " << numberVariables << ' ' << clauses << endl;

        /* Special case that there's only one vertex */
        if (numVertices == 1) {
            cnf << 1 << ' ' << 0 << endl;
            cnf << -1 << ' ' << 0 << endl;
            return;
        }

        /* Each vertex must have a position in the path */
        for (int vertex = 1; vertex <= numberVariables;  vertex += numVertices) {
            for (int path_pos = 0; path_pos < numVertices; path_pos++) {
                cnf << vertex + path_pos << ' ';
            }
            cnf << 0 << endl;
            count++;
        }

        /* Each vertex must appear just once in the path */
        for (int vertex = 1; vertex <= numberVariables;  vertex += numVertices) {
            for (int vertex_path = vertex; vertex_path < numVertices + vertex; vertex_path++) {
                for (int path_pos = 1; path_pos < vertex + numVertices - vertex_path; path_pos++) {
                    cnf << -(vertex_path) << ' ' << -(vertex_path + path_pos) << ' ' << 0 << endl;
                    count++;
                }
            }
        }

        /* Each position must have a vertex */
        for (int path_pos = 0; path_pos < numVertices; path_pos++) {
            for (int vertex = 1; vertex <= numberVariables;  vertex += numVertices) {
                cnf << vertex + path_pos << ' ';
            }
            cnf << 0 << endl;
            count++;
        }

        /* Each position can have only one vertex */
        for (int path_pos = 1; path_pos <= numVertices; path_pos++) {
            for (int vertex_path = path_pos; vertex_path < numberVariables; vertex_path += numVertices) {
                for (int vertex = numVertices; vertex <= numberVariables - vertex_path;  vertex += numVertices) {
                    cnf << -(vertex_path) << ' ' << -(vertex_path + vertex) << ' ' << 0 << endl;
                    count++;
                }
            }
        }

        /* Contiguos vertices in the path must have an edge */
        Matrix edges_PlusAdded = adj_matrix;                    // Could do without this new matrix
        for (int from = 1; from <= numVertices; from++) {
            vector<int> not_edges;
            for (int to = 1; to <= numVertices; to++) {
                if (from != to && !edges_PlusAdded[from - 1][to - 1]) {
                    not_edges.push_back(to);
                    // To avoid duplicating clauses
                    edges_PlusAdded[from - 1][to - 1] = 1;
                    edges_PlusAdded[to - 1][from - 1] = 1;
                }
            }
            add_NotEdges(cnf, from, not_edges, count);
        }
    }

    string read_File() {
    /* 
        Reads the first line from minisat output file FILE_OUT
    */

        /* Opening the file */
        ifstream ist{FILE_OUT};

        /* Only care about the first line, which contains SAT or UNSAT */
        string result;
        ist >> result;

        return result;
    }
    
    string printEquisatisfiableSatFormula() {
    /* 
        Writes the input to a .txt file, runs minisat then outputs the answer 
    */

        /* Creating and writing the input to the file */
        write_ToFile();

        /* Calling minisat (http://minisat.se/) on the terminal */
        string s = "minisat " + FILE_IN + " " + FILE_OUT;
        const char *command = s.c_str();
        system(command);

        /* Reading the answer from minisat output file */ 
        return read_File();
    }


};

int main() {
    ios::sync_with_stdio(false);

    /* n = number of vertices, m = number of edges*/
    int n, m;
    cin >> n >> m;

    ConvertHampathToSat converter(n, m);
    vector<int> vertices(n);

    for (int i = 0; i < m; i++) {

        int from, to;
        cin >> from >> to;
        /* Input can have repeated edges, which need to be substracted for the 
            calculation of number of clauses */
        if (converter.adj_matrix[from - 1][to - 1]) {
            converter.repeatedEdges++;
        }
        /*  Adding edges to adjacency list */
        converter.adj_matrix[from - 1][to - 1] = 1;
        converter.adj_matrix[to - 1][from - 1] = 1;
    }

    string answer = converter.printEquisatisfiableSatFormula();

    cout << answer << endl;

    return 0;
}



Source: Windows Questions C++

LEAVE A COMMENT