chuffed / chuffed

The Chuffed CP solver
MIT License
93 stars 42 forks source link

Assertion failure in engine when solving certain problems #31

Closed Qix- closed 1 year ago

Qix- commented 6 years ago

I'm evaluating chuffed and implementing a rudimentary (and most likely very poorly performing) Sudoku solver.

Throw this into the examples folder and compile it like any other example:

#include <cstdio>
#include <cassert>
#include <chuffed/core/engine.h>
#include <chuffed/core/propagator.h>
#include <chuffed/branching/branching.h>
#include <chuffed/vars/modelling.h>
#include <iostream>
#include <vector>

// hardest puzzles taken from https://github.com/dimitri/sudoku/blob/master/hardest.txt
static const char * const hardest[] = {
    "85...24..72......9..4.........1.7..23.5...9...4...........8..7..17..........36.4.",
    "..53.....8......2..7..1.5..4....53...1..7...6..32...8..6.5....9..4....3......97..",
    "12..4......5.69.1...9...5.........7.7...52.9..3......2.9.6...5.4..9..8.1..3...9.4",
    "...57..3.1......2.7...234......8...4..7..4...49....6.5.42...3.....7..9....18.....",
    "7..1523........92....3.....1....47.8.......6............9...5.6.4.9.7...8....6.1.",
    "1....7.9..3..2...8..96..5....53..9...1..8...26....4...3......1..4......7..7...3..",
    "1...34.8....8..5....4.6..21.18......3..1.2..6......81.52..7.9....6..9....9.64...2",
    "...92......68.3...19..7...623..4.1....1...7....8.3..297...8..91...5.72......64...",
    ".6.5.4.3.1...9...8.........9...5...6.4.6.2.7.7...4...5.........4...8...1.5.2.3.4.",
    "7.....4...2..7..8...3..8.799..5..3...6..2..9...1.97..6...3..9...3..4..6...9..1.35",
    "....7..2.8.......6.1.2.5...9.54....8.........3....85.1...3.2.8.4.......9.7..6....",
    nullptr
};

static void renderBoard(std::ostream &os, const char *board) {
    for (int y = 0; y < 9; y++) {
        if (y == 0) {
            os << "┌─────┬─────┬─────┐" << std::endl;
        } else if (y % 3 == 0) {
            os << "├─────┼─────┼─────┤" << std::endl;
        }

        for (int x = 0; x < 9; x++) {
            if (x % 3 == 0) {
                os << "│";
            } else {
                os << " ";
            }

            char c = board[y * 9 + x];
            if (c == '.') c = ' ';
            os << c;
        }

        os << "│" << std::endl;
    }

    os << "└─────┴─────┴─────┘" << std::endl;
}

class Sudoku : public Problem {
public:
    // Core variables

    std::vector<vec<IntVar*>> rows;
    std::vector<vec<IntVar*>> cols;
    std::vector<vec<IntVar*>> tiles;

    Sudoku(const char * const board) : rows(9), cols(9), tiles(9) {
        renderBoard(std::cout, board);

        for (int i = 0; i < 9; i++) {
            createVars(rows[i], 9, 1, 9);
            all_different(rows[i]);
            branch(rows[i], VAR_INORDER, VAL_MIN);
        }

        for (int c = 0; c < 9; c++) {
            cols[c].growTo(9);
            for (int r = 0; r < 9; r++) {
                cols[c][r] = rows[r][c];
            }
            all_different(cols[c]);
        }

        for (int t = 0; t < 9; t++) {
            tiles[t].growTo(9);
            int tx = t % 3;
            int ty = t / 3;
            for (int cell = 0; cell < 9; cell++) {
                int cx = cell % 3;
                int cy = cell / 3;
                int row = tx * 3 + cx;
                int col = ty * 3 + cy;
                tiles[t][cell] = rows[row][col];
            }
            all_different(tiles[t]);
        }

        for (int y = 0; y < 9; y++) {
            for (int x = 0; x < 9; x++) {
                char c = board[y * 9 + x];
                if (c != '.') {
                    rows[y][x]->setVal(c - '0');
                }
            }
        }
    }

    void print(std::ostream& os) {
        char str[81];
        for (int i = 0; i < 81; i++) {
            str[i] = rows[i / 9][i % 9]->getVal() + '0';
        }

        renderBoard(os, str);
    }
};

int main() {
    const char * const *cur = hardest;
    while (*cur) {
        engine.solve(new Sudoku((cur++)[0]));
    }
    return 0;
}

It correctly solves the first two:

┌─────┬─────┬─────┐
│8 5  │    2│4    │
│7 2  │     │    9│
│    4│     │     │
├─────┼─────┼─────┤
│     │1   7│    2│
│3   5│     │9    │
│  4  │     │     │
├─────┼─────┼─────┤
│     │  8  │  7  │
│  1 7│     │     │
│     │  3 6│  4  │
└─────┴─────┴─────┘
┌─────┬─────┬─────┐
│8 5 9│6 1 2│4 3 7│
│7 2 3│8 5 4│1 6 9│
│1 6 4│3 7 9│5 2 8│
├─────┼─────┼─────┤
│9 8 6│1 4 7│3 5 2│
│3 7 5│2 6 8│9 1 4│
│2 4 1│5 9 3│7 8 6│
├─────┼─────┼─────┤
│4 3 2│9 8 1│6 7 5│
│6 1 7│4 2 5│8 9 3│
│5 9 8│7 3 6│2 4 1│
└─────┴─────┴─────┘

----------
┌─────┬─────┬─────┐
│    5│3    │     │
│8    │     │  2  │
│  7  │  1  │5    │
├─────┼─────┼─────┤
│4    │    5│3    │
│  1  │  7  │    6│
│    3│2    │  8  │
├─────┼─────┼─────┤
│  6  │5    │    9│
│    4│     │  3  │
│     │    9│7    │
└─────┴─────┴─────┘
┌─────┬─────┬─────┐
│1 4 5│3 2 7│6 9 8│
│8 3 9│6 5 4│1 2 7│
│6 7 2│9 1 8│5 4 3│
├─────┼─────┼─────┤
│4 9 6│1 8 5│3 7 2│
│2 1 8│4 7 3│9 5 6│
│7 5 3│2 9 6│4 8 1│
├─────┼─────┼─────┤
│3 6 7│5 4 2│8 1 9│
│9 8 4│7 6 1│2 3 5│
│5 2 1│8 3 9│7 6 4│
└─────┴─────┴─────┘

----------

but chokes on the third one:

../chuffed/core/engine.cpp:419: Not yet supported
[1]    47394 abort      ./sudoku

What exactly isn't supported? Looks like not declaring output variables but I'm not entirely sure what those are in terms of chuffed.

Dekker1 commented 6 years ago

The problem seems to be that your problem class doesn't declare the variables that will be used as output. Adding output_vars(rows[i]); in the for-loop that creates your variables seems to fix the problem. The output variables are guaranteed to be set to the correct values whenever the search finds a solution. (Other variables might disappear if a better representation, like a boolean formula is available)

Qix- commented 6 years ago

Ahhhh okay. That makes sense. Is this documented anywhere?

Dekker1 commented 6 years ago

To be perfectly honest, chuffed is really not meant to be used as a library: various parts of the engine are kept in the global space and there is no documentation other than some comment in the code. We mainly maintain the FlatZinc interface.

If you are using chuffed as a library you will probably run into various issues that are not easy to resolve, and there is only limited support that we can provide.

Qix- commented 6 years ago

That's disappointing mainly because it's one of the only complete FDCS implementations that is efficient and has any sort of sensible API outside of scripting languages. :/

Know of any others?

schutta commented 6 years ago

Jip's statement is a little bit too strong. We have a ToDo list for Chuffed, which also includes to make Chuffed usable as a library. However, we do not have the manpower to work on it at the moment and in the near future. But we are more than happy if you want to contribute to Chuffed by making Chuffed usable as a library.