3
\$\begingroup\$

I built a solver for Tents puzzles using the CaDiCaL SAT solver. The code works and runs quickly, it takes less than 0.1 seconds for a 60x60 tents puzzle on a 2,6 GHz Dual-Core Intel Core i5 2013 Macbook Pro. Note that the tents website can't handle puzzles greater than 25x25, the 60x60 board was created by a custom script.

My questions are:

  1. Is the code any good? I'm not yet very familiar with C++14 and more modern features, so there might be easy ways to simplify the code.
  2. How can I improve the performance? I thought about using int16_t instead of int to get more tent variables into the cache. int16_t should be enough for boards smaller than 180x180.
  3. How can I improve the code style? I'm torn between using the 80 character limit or not.

main.cpp

#include <fstream>
#include <iostream>
#include <stdexcept>
#include <string>

#include "tents.hpp"

int main(int argc, char ** argv) {
    if (argc < 2) {
        std::cout << "Usage: " << argv[0] << " <tents file>\n";
        return 0;
    }

    std::ifstream file(argv[1]);
    if (file.fail()) {
        std::cout << "Invalid file.\n";
    }

    std::string line;
    std::string board;

    while (std::getline(file, line))
        board += line + '\n';
    
    file.close();

    try {
        Tents * tents = new Tents(board);
        std::cout << *tents << '\n';
        if (tents->solve())
            std::cout << *tents << '\n';
        else
            std::cout << "Could not solve file.\n";
    } catch (const std::invalid_argument & e) {
        std::cout << e.what() << '\n';
    }

}

tents.hpp

#include <chrono>
#include <ostream>
#include <vector>

#define ROWMAX 200
#define COLMAX 200

using sysClock = std::chrono::system_clock;
using durSec = std::chrono::duration<double>;

// States each cell of the tents board can be in.
enum class CellState {
    EMPTY,
    TREE,
    TENT
};

// Each variable denotes a possible tent that can be placed. 'row' and 'col'
// denote the position of the tent on the board, 'number' is the variable number
// used in the SAT solver and 'tree' is the number of the adjacent tree.
struct Variable {
    int row;
    int col;
    int number;
    int tree;

    Variable(int row, int col, int number, int tree) : row(row), col(col),
        number(number), tree(tree) {}
};

class Tents {

private:

    int rows;
    int cols;

    // Number of trees.
    int trees;

    durSec durationBuild;
    durSec durationSolve;

    // Board of size rows * cols. Maximum is ROWMAX * COLMAX.
    std::vector<CellState> board;

    std::vector<int> rowRestrictions;
    std::vector<int> colRestrictions;

    // Variables to build clauses from.
    std::vector<Variable> variables;

    // Variable assignments.
    std::vector<bool> assignments;

    // Clauses for the SAT solver.
    std::vector<int> clauses;

    // Can a tent be placed on the cell denoted by parameters 'row' and 'col'?
    bool tentPlacable(int, int) const;

    // Find all tents that are orthogonally adjacent to the tree denoted by
    // parameters 'row' and 'col'.
    void findTents(int, int, std::vector<std::pair<int, int> > &) const;

    // Check if variables 'v1' and 'v2' are adjacent in any of the following
    // directions: same position, east, south east, south, south west.
    bool adjacent(const Variable &, const Variable &) const;

    // Using the variables 'vars', it builds the clauses for the tree restrictions:
    // every tree must have exactly one adjacent tent.
    void buildClausesTree(const std::vector<std::vector<Variable> > &);

    // Using the variables 'vars', it builds the adjacent tents restrictions:
    // There must be no two adjacent tents.
    void buildClausesAdjacent(const std::vector<std::vector<Variable> > &);

    // Using the variables 'vars', it builds a 'k'-cardinality constraint by
    // building a sequential counter. The sequential counter needs to create new
    // variables starting at variable number 'number'. For more information, see
    // (1) at the bottom of this file.
    void buildSequentialCounter(const std::vector<Variable> &, int, int &);

    // Based on the tents board configuration, it builds clauses in CNF format
    // for the SAT solver.
    void buildClauses();

public:

    // The constructor takes a tents board as string 'str'.
    Tents(const std::string &);

    // Solves the tents puzzle by building clauses and invoking a SAT solver.
    bool solve();

    // Print the tents board.
    friend std::ostream & operator<<(std::ostream & out, const Tents & tents);

};

tents.cpp

#include <chrono>
#include <ostream>
#include <sstream>
#include <stdexcept>
#include <string>
#include <utility>
#include <vector>

#include "cadical.hpp"
#include "tents.hpp"

using sysClock = std::chrono::system_clock;
using durSec = std::chrono::duration<double>;

// Can a tent be placed on the cell denoted by parameters 'row' and 'col'?
bool Tents::tentPlacable(int row, int col) const {
    if (row < 0 || col < 0 || row >= this->rows || col >= this->cols)
        return false;
    
    if (this->rowRestrictions[row] > 0
        && this->colRestrictions[col] > 0
        && this->board[row * this->cols + col] == CellState::EMPTY)
        return true;
    
    return false;
}

// Find all tents that are orthogonally adjacent to the tree denoted by
// parameters 'row' and 'col'.
void Tents::findTents(int row, int col, std::vector<std::pair<int, int> > & tents) const {
    // Check north.
    if (tentPlacable(row - 1, col))
        tents.emplace_back(row - 1, col);
    
    // Check east.
    if (tentPlacable(row, col + 1))
        tents.emplace_back(row, col + 1);

    // Check south.
    if (tentPlacable(row + 1, col))
        tents.emplace_back(row + 1, col);
    
    // Check west.
    if (tentPlacable(row, col - 1))
        tents.emplace_back(row, col - 1);
}

// Check if variables 'v1' and 'v2' are adjacent in any of the following
// directions: same position, east, south east, south, south west.
bool Tents::adjacent(const Variable & v1, const Variable & v2) const {
    // Do both tents belong to the same tree?
    if (v1.tree == v2.tree)
        return false;
    
    // Two tents on the same cell?
    if (v1.row == v2.row && v1.col == v2.col)
        return true;

    // Check east.
    if (v1.row == v2.row && v1.col + 1 == v2.col)
        return true;

    // Check south east.
    if (v1.row + 1 == v2.row && v1.col + 1 == v2.col)
        return true;

    // Check south.
    if (v1.row + 1 == v2.row && v1.col == v2.col)
        return true;

    // Check south west.
    if (v1.row + 1 == v2.row && v1.col - 1 == v2.col)
        return true;

    return false;
}

// Using the variables 'vars', it builds the clauses for the tree restrictions:
// every tree must have exactly one adjacent tent.
void Tents::buildClausesTree(const std::vector<std::vector<Variable> > & vars) {
    for (const auto & tree : vars) {
        // Build a clause of the form a v ... v d.
        for (const auto & var : tree)
            this->clauses.push_back(var.number);
        this->clauses.push_back(0);

        // Build clauses of the form a v ... v d.
        if (tree.size() == 2) {
            // One clause of the form -a v -b.
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[1].number, 0});
        } else if (tree.size() == 3) {
            // Three clauses of the form -a v -b.
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[1].number, 0});
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[2].number, 0});
            this->clauses.insert(this->clauses.end(), {-tree[1].number, -tree[2].number, 0});
        } else if (tree.size() == 4) {
            // Four clauses of the form -a v -b v -c.
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[1].number, -tree[2].number, 0});
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[1].number, -tree[3].number, 0});
            this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[2].number, -tree[3].number, 0});
            this->clauses.insert(this->clauses.end(), {-tree[1].number, -tree[2].number, -tree[3].number, 0});
        }
    }
}

// Using the variables 'vars', it builds the adjacent tents restrictions:
// There must be no two adjacent tents.
void Tents::buildClausesAdjacent(const std::vector<std::vector<Variable> > & vars) {
    std::vector<Variable>::size_type i;
    std::vector<Variable>::size_type j;

    for (int row = 0; row < this->rows - 1; ++row) {
        for (i = 0; i < vars[row].size(); ++i) {
            const auto & v1 = vars[row][i];

            // Are there any adjacent variables in the same row?
            for (j = i + 1; j < vars[row].size(); ++j) {
                const auto & v2 = vars[row][j];
                if (adjacent(v1, v2))
                    this->clauses.insert(this->clauses.end(), {-v1.number, -v2.number, 0});
            }

            // Are there any adjacent variables in the next row?
            for (j = 0; j < vars[row + 1].size(); ++j) {
                const auto & v2 = vars[row + 1][j];
                if (adjacent(v1, v2))
                    this->clauses.insert(this->clauses.end(), {-v1.number, -v2.number, 0});
            }
        }
    }
}

// Using the variables 'vars', it builds a 'k'-cardinality constraint by
// building a sequential counter. The sequential counter needs to create new
// variables starting at variable number 'number'. For more information, see
// (1) at the bottom of this file.
void Tents::buildSequentialCounter(const std::vector<Variable> & vars, int k, int & number) {
    if (k == 0)
        return;

    const int n = vars.size();
    if (n == 1) {
        this->clauses.insert(this->clauses.end(), {vars[0].number, 0});
        return;
    }

    // Initialize the partial sums. Every inner vector is a partial sum of k
    // bits. Every bit has its own variable number.
    std::vector<std::vector<int> > sums(n, std::vector<int>(k, 0));
    for (auto & sum : sums) {
        for (auto & bit : sum)
            bit = number++;
    }

    this->clauses.insert(this->clauses.end(), {-vars[0].number, sums[0][0], 0});

    for (int j = 2; j <= k; ++j)
        this->clauses.insert(this->clauses.end(), {-sums[0][j-1], 0});
    for (int i = 2; i < n; ++i) {
        this->clauses.insert(this->clauses.end(), {-vars[i-1].number, sums[i-1][0], 0,
            -sums[i-2][0], sums[i-1][0], 0});
        
        for (int j = 2; j <= k; ++j) {
            this->clauses.insert(this->clauses.end(), {-vars[i-1].number, -sums[i-2][j-2],
                sums[i-1][j-1], 0, -sums[i-2][j-1], sums[i-1][j-1], 0});
        }
        this->clauses.insert(this->clauses.end(), {-vars[i-1].number, -sums[i-2][k-1], 0});
    }

    this->clauses.insert(this->clauses.end(), {-vars[n-1].number, -sums[n-2][k-1], 0});
}

// Based on the tents board configuration, it builds clauses in CNF format
// for the SAT solver.
void Tents::buildClauses() {

    // Tents that are orthogonally adjacent to a tree.
    std::vector<std::pair<int, int> > tents;
    tents.reserve(4);

    // Reserve space for the variables. Every row has at most # columns * 2 variables,
    // every column at most # rows * 2 and every tree has at most 4.
    // ---------------------
    // | T | 3 | T | 3 | T |
    // | 3 | T | 4 | T | 3 | <- This row has the maximum amount of variables.
    // | T | 3 | T | 3 | T |
    // ---------------------
    //       ^ This column has the maximum amount of variables.
    std::vector<std::vector<Variable> > rowVars(this->rows, std::vector<Variable>());
    for (int row = 0; row < this->rows; ++row)
        rowVars[row].reserve(this->cols * 2);

    std::vector<std::vector<Variable> > colVars(this->cols, std::vector<Variable>());
    for (int col = 0; col < this->cols; ++col)
        colVars[col].reserve(this->rows * 2);

    std::vector<std::vector<Variable> > treeVars(this->trees, std::vector<Variable>());
    for (int tree = 0; tree < this->trees; ++tree)
        treeVars[tree].reserve(4);

    // The board has at most # trees * 4 variables.
    this->variables.reserve(this->trees * 4);

    // Which also means at most # trees * 4 assignments.
    this->assignments.reserve(this->trees * 4);

    // Estimate the number of clauses. 2 ^ 17 clauses should suffice for
    // boards smaller than 70x70.
    this->clauses.reserve(1 << 17);

    // Increasing variable number.
    int number = 1;
    int tree = 0;

    for (int row = 0; row < this->rows; ++row) {
        for (int col = 0; col < this->cols; ++col) {
            if (this->board[row * this->cols + col] == CellState::TREE) {
                // Find all orthogonally adjecent tents.
                findTents(row, col, tents);
                if (tents.size() == 0)
                    continue;
                
                // Construct all variables for each tree.
                for (const auto & tent : tents) {
                    this->variables.emplace_back(tent.first, tent.second, number, tree);
                    rowVars[tent.first].emplace_back(tent.first, tent.second, number, tree);
                    colVars[tent.second].emplace_back(tent.first, tent.second, number, tree);
                    treeVars[tree].emplace_back(tent.first, tent.second, number++, tree);
                }

                tents.clear();
                ++tree;
            }
        }
    }

    // Build the clauses for the SAT solver.
    buildClausesTree(treeVars);
    buildClausesAdjacent(rowVars);
    // Build a sequential counter for each row and column.
    for (int row = 0; row < this->rows; ++row)
        buildSequentialCounter(rowVars[row], this->rowRestrictions[row], number);
    for (int col = 0; col < this->cols; ++col)
        buildSequentialCounter(colVars[col], this->colRestrictions[col], number);
}

// The constructor takes a tents board as string 'str'.
Tents::Tents(const std::string &str) : trees(0) {
    std::stringstream stream(str);
    stream >> std::skipws;

    // Read board size.
    if (!(stream >> this->rows))
        throw std::invalid_argument("Invalid string.");
    if (!(stream >> this->cols))
        throw std::invalid_argument("Invalid string.");
    
    if (this->rows <= 0 || this->cols <= 0)
        throw std::invalid_argument("Invalid board dimensions.");
    if (this->rows > ROWMAX || this->cols > COLMAX)
        throw std::invalid_argument("Invalid board dimensions.");

    // Initialize the board.
    this->board.assign(this->rows * this->cols, CellState::EMPTY);

    this->rowRestrictions.reserve(this->rows);
    this->colRestrictions.reserve(this->cols);

    // Read board.
    char c;
    for (int row = 0; row < this->rows; ++row) {
        // Read row.
        for (int col = 0; col < this->cols; ++col) {
            if (!(stream >> c))
                throw std::invalid_argument("Invalid string.");
            if (c == 'T') {
                this->board[row * this->cols + col] = CellState::TREE;
                ++this->trees;
            }
        }

        // Read row restriction.
        if (!(stream >> this->rowRestrictions[row]))
            throw std::invalid_argument("Invalid string.");
    }

    // Read column restrictions.
    for (int col = 0; col < this->cols; ++col) {
        if (!(stream >> this->colRestrictions[col]))
            throw std::invalid_argument("Invalid string.");
    }
}

// Solves the tents puzzle by building clauses and invoking a SAT solver.
bool Tents::solve() {
    CaDiCaL::Solver * solver = new CaDiCaL::Solver;

    const auto beforeBuild = sysClock::now();
    buildClauses();
    this->durationBuild = sysClock::now() - beforeBuild;

    // Feed clauses to cadical.
    for (auto var : this->clauses)
        solver->add(var);
    
    const auto beforeSolve = sysClock::now();
    const int res = solver->solve();
    this->durationSolve = sysClock::now() - beforeSolve;

    // Is the board unsatisfiable?
    if (res != 10)
        return false;
    
    // It is satisfiable. Set assignments and palce tents.
    std::vector<Variable>::size_type i;
    for (i = 0; i < this->variables.size(); ++i) {
        const bool assignment = (solver->val(this->variables[i].number) > 0);
        this->assignments[i] = assignment;
        if (assignment)
            this->board[this->variables[i].row * this->cols + this->variables[i].col] = CellState::TENT;
    }

    return true;
}

// Print the tents board.
std::ostream & operator<<(std::ostream & out, const Tents & tents) {
    // Print board and row restrictions.
    for (int row = 0; row < tents.rows; ++row) {
        for (int col = 0; col < tents.cols; ++col) {
            const CellState state = tents.board[row * tents.cols + col];
            if (state == CellState::EMPTY)
                out << '.';
            else if (state == CellState::TREE)
                out << 'T';
            else
                out << 'A';
        }
        out << ' ' << tents.rowRestrictions[row] << '\n';
    }

    // Print column restrictions.
    for (int col = 0; col < tents.cols; ++col)
        out << tents.colRestrictions[col] << ' ';

    out << "\nBuilding the clauses took " << tents.durationBuild.count() << "s.\n";
    out << "Solving the clauses took  " << tents.durationSolve.count() << "s.\n"; 
    return out;
}

Tent puzzle of size 15x15

15 15
.........T.T..T 4
T...TT..TT..... 3
......T.....T.. 3
T..T....T..T... 4
....T........T. 2
..TT........... 3
........T.T...T 3
.T.T..T........ 2
......T.......T 4
..T.T.TT..T...T 1
.......T.T.T... 6
T...T.......T.. 1
T........T.T.T. 6
.T..T.T........ 2
............... 1
4 3 3 1 5 1 5 1 4 2 4 3 3 2 4

Tent puzzle of size 20x20

20 20
.T..........T...T..T 4
....TT..T..........T 4
T.T.......TT........ 4
.....T....T..TT..T.T 3
.......T.T......T... 6
.TT.T............... 2
....TT.......T.T.... 2
.T..........T.....T. 8
.T.T.....T.......T.. 1
.....TT.....T..T.T.T 7
T.......TT......T... 1
...............T.... 6
...T.....T..TT..T.T. 2
.TT.T..T............ 7
...........T.....T.. 1
....TT....T........T 7
T....T.....T.TT.T... 1
T.......T.T...T...TT 8
T.TTT.......T....... 2
.......T............ 4
7 3 3 6 3 5 5 3 2 5 2 5 2 5 4 3 6 2 3 6

Tent puzzle of size 25x25

25 25
..............T.T.T.TTT.. 7
...T..T..T.........T..... 4
.T..T...T.....T...T...... 4
.....T..T..T...T......T.. 3
.T..T........T........... 7
T..............TT..T.TTT. 3
.......T.....T.......T... 7
..T.....T.TT.....T....... 3
....T.T......TT...T.T..T. 8
.T.......T.T.......T..... 3
..T..TT...T.....T.T.T...T 9
...T........T...T...TT..T 1
..T..................T... 10
.....T.T.T.TT..T...TT..T. 2
......TT...T.T........... 8
TTT...............T....T. 2
.....T.T....T...T...T.... 9
....T.........T...TT..... 2
..T...TT.T...TT.....T.... 8
.T..................T..T. 3
.T.T......T...T..T..T.T.. 8
T.T..T..T...T.......T.... 3
.....T..........TT..T.... 9
.......T.T.T............T 2
.............T...T....... 0
5 5 5 3 6 4 4 4 7 4 4 7 0 12 0 10 2 10 1 9 3 7 2 7 4

Compile with g++ -std=c++14 -O3 -o tents.out main.cpp tents.cpp -L. -lcadical. You can find the library and the hpp file in the CaDiCaL Github repository.

Run with ./tents.out <tents puzzle txt file>.

\$\endgroup\$

1 Answer 1

1
\$\begingroup\$

Answers to your questions

Is the code any good? I'm not yet very familiar with C++14 and more modern features, so there might be easy ways to simplify the code.

From a first glance, it looks very decent. You are already using lots of modern features, and using good C++ programming practices like range-for, enum classes and so on.

I did notice you use this-> a lot, it is almost never necessary to use that, so remove it where possible. It will also shorten your lines.

How can I improve the performance? I thought about using int16_t instead of int to get more tent variables into the cache. int16_t should be enough for boards smaller than 180x180.

Which cache are you talking about? Forget about the L1d cache, it typically is 32 kB on contemporary CPUs, although maybe there are a few with 64 kB, but that still is probably too little to hold a 180x180 array of int16_ts and all the other data necessary to run the algorithm. The L2 cache is typically much larger. Of course, reducing the bandwidth, even to a cache, might still improve performance. On the other hand the CPU might need to do more work unpacking uint16_ts. So you can try to use int16_t, but you have to measure it to know for sure what version will be faster.

How can I improve the code style? I'm torn between using the 80 character limit or not.

Personally, I would do away with any character limit. If a line is so long you have to split it, it is going to be ugly anyway, and I would rather let my editor split the line visually for me depending on the editor's window size than impose a hardcoded limit that only works well for a specific screen size.

Code style is very much a matter of taste, with the exception that once you pick a certain style, you should apply it consistently. I recommend you pick a code formatter like Artistic Style or ClangFormat, configure it the way you like (I recommend picking one of the built-in standard styles that most closely resembles the one you are already using), and then format your code with the code formatter. Then you don't have to worry too much about the style anymore, and if you want to collaborate with others, they can use the same formatter with the same settings.

Apart from that, your use of this-> has made some lines much longer than necessary, for example:

this->clauses.insert(this->clauses.end(), {-tree[0].number, -tree[1].number, 0});

Can be shortened by 12 characters to:

clauses.insert(clauses.end(), {-tree[0].number, -tree[1].number, 0});

Useless try-catch in main()

You have the following in main():

try {
    ...
} catch (const std::invalid_argument &e) {
    std::cout << e.what() << '\n';
}

This is bad for two reasons: first, if you wouldn't catch the exception, the default behaviour is that e.what() is printed anyway. Second, by catching the error and just letting main() exit normally, the program will now exit with a return code of zero. This is bad if you want to use your tent solving program in a script, as that script can now no longer distinguish between your program having run successfully or unsuccesfuly easily.

In short, only handle exceptions if you can deal with them in a meaningful way. If you can't, that's fine, just don't catch the exception and let the program terminate with an error.

Print error messages to std::cerr

You should print error messages to std::cerr. This allows them to be distinguished from the regular output of your program. This is especially important if ever want to redirect the output of your program to a file. Consider:

./tents-solver input_file > output_file

If you print errors to std::cout, no error message will appear on screen, it will just go to output_file. If you print them to std::cerr`, they will appear on screen.

Exit with a non-zero exit code on errors

If you encountered an error in your program you cannot recover from, make sure you return with a non-zero exit code. So:

if (argc < 2) {
    std::cerr << "Usage: " << argv[0] << " <tents file>\n";
    return 1;
}
...
if (file.fail)) {
    std::cerr << "Invalid file.\n";
    return 1;
}

Check for all possible I/O errors

You only check whether you could open the input file, but you didn't check whether you could read the file correctly. After reading the board, check that there wasn't some error:

while (std::getline(file, line))
    board += line + '\n';

if (file.bad()) {
    std::cerr << "Error reading file.\n";
    return 1;
}

Also, there might be a problem writing the output, especially if the output is redirected to a file, or piped into another program. So you should also check for cout.bad() at the end of main().

Use static constexpr where possible for constants

Instead of using #define, declare constants as static constexpr variables, like so:

static constexpr int ROWMAX = 200;
static constexpr int COLMAX = 200;

Also, since these constants are only used internally in tents.cpp, you should move them into tents.cpp.

Move other types into class Tents

You define several types in tents.hpp outside of class Tents, but since they are only relevant to class Tents itself, you should move their definitions inside that of class Tents to avoid polluting the global namespace. Furthermore, since these types are only used internally, you can make them private. For example:

class Tents {
private:
    using sysClock = std::chrono::system_clock;
    using durSec = std::chrono::duration<double>;

    enum class CellState {
        ...
    }:

    struct Variable {
         ...
    };

    ...
};

Prefer using size_t for sizes and counters

An int can be negative, and might not be large enough to represent all possible sizes of data structures. Prefer using size_t for variables holding sizes and counters, like rows, cols, and trees.

Prefer returning variables where possible

It's perfectly fine in C++ to return "large" objects by value thanks to copy elision. For example, you can make findTents() return the vector of coordinates by value:

std::vector<std::pair<int, int>> Tents::findTents(int, int) const {
    std::vector<std::pair<int, int>> tents;
    tents.reserve(4);
    ...
    return tents;
}

And then use it like so:

for (int row = 0; row < this->rows; ++row) {
    for (int col = 0; col < this->cols; ++col) {
        if (this->board[row * this->cols + col] == CellState::TREE) {
            auto tents = findTents(row, col);
            ...
            // no need for tents.clear()
        }
    }
}

But even better:

Avoid unnecessary temporaries

Instead of building a vector of elements, then doing a single loop through them and discarding the vector, consider changing the flow of the code so you don't need the temporary vector. For example, you could change findTents to apply a function to each of the empty spots it finds:

void Tents::findTents(int, int, std::function<void(int, int)> func) const {
    if (tentPlacable(row - 1, col))
        func(row - 1, col);

    if (tentPlacable(row, col + 1))
        func(row, col + 1);

    ...
}

And use it like so:

for (int row = 0; row < this->rows; ++row) {
    for (int col = 0; col < this->cols; ++col) {
        if (this->board[row * this->cols + col] == CellState::TREE) {
            bool foundSpot = false;
            
            findTents(row, col, [&](int trow, int tcol) {
                foundSpot = true;
                variables.emplace_back(trow, tcol, number, tree);
                rowVars[row].emplace_back(trow, tcol, number, tree);
                colVars[col].emplace_back(trow, tcol, number, tree);
                treeVars[tree].emplace_back(trow, tcol, number++, tree);
            });

            trees += foundSpot;
        }
    }
}

Similarly, you are building a list of clauses in a vector, just to call solver->add() on all of them. This is quite the waste of memory, especially given that you call clauses.reserve(1 << 17). You could just pass a reference to solver to buildClauses(), and have that one in turn pass it on to the other build*() functions.

Have the constructor take a std::istream instead of a std::string

Instead of having the constructor take a reference to a std::string as input, consider having it take a std::istream reference. Apart from having a better symmetry with how you print the result, this avoids having to create a std::stringstream from the string, and even allows directly passing file from main to the constructor:

Tents::Tents(std::istream &stream) : trees(0) {
    ...
}

...

int main(int argc, char **argv) {
   if (argc < 2) {
       ...
   }

   Tents tents(std::ifstream(argv[1]));

   if (tents.solve()) {
       std::cout << tents << '\n';
   } else {
       std::cerr << "Could not solve.\n";
       return 1;
   }
}
\$\endgroup\$
2
  • \$\begingroup\$ Thank you, your review was really helpful. I don't know why I didn't pass the solver directly, it seems obvious now. One more question. What does [&] in buildClauses() do? It seems to allow func access to variables of the local scope. \$\endgroup\$ Dec 20, 2020 at 9:34
  • 1
    \$\begingroup\$ Correct, the things between brackets are the variables the lambda captures, and & is short for "everything by reference". \$\endgroup\$
    – G. Sliepen
    Dec 20, 2020 at 9:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.