~jleightcap/picrosssat

27f662c9e130c3277924c3da7fa63a3c0a3137f1 — jleightcap 1 year, 6 months ago 83af33b
Basic working example
5 files changed, 36 insertions(+), 33 deletions(-)

M board.h
M io.cpp
M main.cpp
M sat.cpp
M sat.h
M board.h => board.h +19 -0
@@ 43,6 43,25 @@ class Board {
        auto getColumnVec() { return colVecs; }

        void setBoard(boardState bs, int ii, int jj) { board[ii][jj] = bs; }

        // Convert the board representation into a string.
        std::string boardString() {
            std::string boardString = "";
            for (size_t ii = 0; ii < board.size(); ii++) {
                for (size_t jj = 0; jj < board.size(); jj++) {
                    switch((board)[ii][jj]) {
                        case UNKNOWN:
                            boardString.append(" "); break;
                        case FALSE:
                            boardString.append("x"); break;
                        case TRUE:
                            boardString.append("█"); break;
                    }
                }
                boardString.append("\n");
            }
            return boardString;
        }
};

#endif

M io.cpp => io.cpp +0 -23
@@ 54,29 54,6 @@ parse(std::string raw)



// Convert the board representation into a string.
std::string
boardString(std::vector<std::vector<boardState>> *board)
{
    std::string boardString = "";
    for (size_t ii = 0; ii < board->size(); ii++) {
        for (size_t jj = 0; jj < board->size(); jj++) {
            switch((*board)[ii][jj]) {
                case UNKNOWN:
                    boardString.append(" "); break;
                case FALSE:
                    boardString.append("x"); break;
                case TRUE:
                    boardString.append("█"); break;
            }
        }
        boardString.append("\n");
    }
    return boardString;
}



// Write input string to file.
void
write_file(std::string text, std::string filename)

M main.cpp => main.cpp +3 -2
@@ 6,13 6,13 @@

int main() {
  //auto restrict_row = "[3] [1 3] [2] [2] [2]";
  auto restrict_row = "[1] [1]";
  auto restrict_row = "[1] [3] [1]";
  //std::cout << "Row restriction:\n";
  //std::getline(std::cin, restrict_row);
  auto row_vector = parse(restrict_row);

  //auto restrict_column = "[1 2] [2] [2] [3] [3]";
  auto restrict_column = "[1] [1]";
  auto restrict_column = "[1] [3] [1]";
  //std::cout << "Column restriction:\n";
  //std::getline(std::cin, restrict_column);
  auto column_vector = parse(restrict_column);


@@ 21,6 21,7 @@ int main() {
  SATExpr s(&b1);
  s.cnf();
  s.solve();
  std::clog << b1.boardString();

  return 0;
}

M sat.cpp => sat.cpp +11 -8
@@ 19,10 19,11 @@ SATExpr::~SATExpr()



SATExpr::SATExpr(Board* b)
SATExpr::SATExpr(Board* b):
    dimX(b->getDimX()),
    dimY(b->getDimY()),
    board(b)
{
    dimX = b->getDimX();
    dimY = b->getDimY();
    const auto rowRestricts = *b->getRowVec();
    const auto colRestricts = *b->getColumnVec();



@@ 259,13 260,15 @@ SATExpr::solve()

    auto sat = solver.solve();
    if (sat) {
        std::clog << " SAT \n=====\n";
        std::clog << "\n===SAT===\n";
        for (int ii = 0; ii < dimX; ii++) {
            for (int jj = 0; jj < dimY; jj++)
                std::clog << (solver.modelValue(ii + dimX*jj) == l_True);
            std::clog << std::endl;
            for (int jj = 0; jj < dimY; jj++) {
                // convert solver bool to BoardState
                bool state = solver.modelValue(ii + dimX*jj) == l_True;
                (*board->getBoard())[ii][jj] = (state ? TRUE : FALSE);
            }
        }
    } else {
        std::clog << "UNSAT\n";
        std::clog << "\n===UNSAT===\n";
    }
}

M sat.h => sat.h +3 -0
@@ 10,6 10,9 @@ class SATExpr {
        int dimX;
        int dimY;

        // store pointer to board
        Board* board;

        // Variable mapping uses row-major ordering,
        // board[ii][jj] => Var(ii + jj*dimX)