~jleightcap/picrosssat

f19961e78322913a27e19b80c05e9c556907ccbf — jleightcap 1 year, 6 months ago 27f662c master
Update README, stdin and I/O input
4 files changed, 96 insertions(+), 30 deletions(-)

M README.md
M main.cpp
M sat.cpp
M sat.h
M README.md => README.md +33 -3
@@ 1,7 1,7 @@
# PicrossSAT
Solve picross (nonogram) puzzles using MiniSat.

## Requirements
## Dependencies
MiniSat with CMake integration, for example master-keyring's fork of `minisat`:
```
git clone https://github.com/master-keying/minisat/


@@ 14,7 14,37 @@ Verified for `g++ 10.1.0` and `clang 10.0.0`:
```
mkdir build && cd build
cmake .. && make picrosssat
./picrosssat [file]
```

For testing, `make test && ./test`
## Usage
```
./picrosssat [ROW] [COL]
```

For example,
```
$ ./picrosssat "[1] [3] [1]" "[1] [3] [1]"
===SAT===
x█x
███
x█x
```

Or for file input,

```
./picrosssat [FILE]
```

First line of file is row restriction, second is column restriction:

```
$ cat test.dat
[1] [3] [1]
[1] [3] [1]
$ ./picrosssat test.dat
===SAT===
x█x
███
x█x
```

M main.cpp => main.cpp +40 -20
@@ 1,27 1,47 @@
#include <iostream>
#include <fstream>

#include "io.h"
#include "board.h"
#include "sat.h"

int main() {
  //auto restrict_row = "[3] [1 3] [2] [2] [2]";
  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] [3] [1]";
  //std::cout << "Column restriction:\n";
  //std::getline(std::cin, restrict_column);
  auto column_vector = parse(restrict_column);

  Board b1(&row_vector, &column_vector);
  SATExpr s(&b1);
  s.cnf();
  s.solve();
  std::clog << b1.boardString();

  return 0;
int main(int argc, char* argv[]) {
    std::string restrictRow;
    std::string restrictCol;

    // file input
    if (argc == 2) {
        std::ifstream input(argv[1]);
        if (input.is_open()) {
            std::getline(input, restrictRow);
            std::getline(input, restrictCol);
        }
        else {
            std::cerr << "Could not open file: " << argv[1] << std::endl;
            return -1;
        }
        input.close();
    }

    // stdin input
    else if (argc == 3) {
        restrictRow = argv[1];
        restrictCol = argv[2];
    }

    else {
        std::cerr << "Usage: ./picrosssat [FILE]; ./picrosssat [ROW] [COL]\n";
        return -1;
    }

    auto rowVec = parse(restrictRow);
    auto colVec = parse(restrictCol);

    Board b1(&rowVec, &colVec);
    SATExpr s(&b1);
    s.cnf();
    s.solve();
    std::clog << b1.boardString();

    return 0;
}

M sat.cpp => sat.cpp +20 -7
@@ 87,7 87,13 @@ SATExpr::SATExpr(Board* b):
        dnfVec.growTo(dnfVec.size() + 1);
        permuteDNF.moveTo(dnfVec.last());
    }
}



void
SATExpr::printDNF()
{
    std::clog << "\n===DNF===\n";
    for (int ii = 0; ii < dnfVec.size(); ii++) {
        for (int jj = 0; jj < dnfVec[ii].size(); jj++) {


@@ 100,6 106,19 @@ SATExpr::SATExpr(Board* b):
}


void
SATExpr::printCNF()
{

    std::clog << "\n===CNF===\n";
    for (auto& nn : cnfVec) {
        for (auto& mm : nn)
            std::clog << mm.x << " ";
        std::clog << std::endl;
    }
}



vector<vector<int>>
restrictParse(std::vector<int> v, int dim)


@@ 234,12 253,6 @@ SATExpr::cnf()
        }
    }

    std::clog << "\n===CNF===\n";
    for (auto& nn : cnfVec) {
        for (auto& mm : nn)
            std::clog << mm.x << " ";
        std::clog << std::endl;
    }
}




@@ 260,7 273,7 @@ SATExpr::solve()

    auto sat = solver.solve();
    if (sat) {
        std::clog << "\n===SAT===\n";
        std::clog << "===SAT===\n";
        for (int ii = 0; ii < dimX; ii++) {
            for (int jj = 0; jj < dimY; jj++) {
                // convert solver bool to BoardState

M sat.h => sat.h +3 -0
@@ 40,6 40,9 @@ class SATExpr {

        auto getDNF() { return &dnfVec; }
        auto getCNF() { return &cnfVec; }

        void printDNF();
        void printCNF();
};