Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incorrect constraint used in explanation when multiple are possible #29

Open
469512345 opened this issue Mar 18, 2024 · 1 comment
Open

Comments

@469512345
Copy link

469512345 commented Mar 18, 2024

Whenever there are multiple constraints which could be used within a single explanation in a deduction, demystify will always default to a given constraint.

For example, a Naked Pairs puzzle from Sudoku Wiki
SudokuWiki-NakedPairs-1

We get the following deduction included in the output:

{
        "decision": "Setting grid[1,4] is not 1 because:",
        "reason": [
          "cells (1,2) and (1,3) cannot both be 6 as they are in the same box",
          "cells (1,2) and (1,4) cannot both be 1 as they are in the same row",
          "cells (1,3) and (1,4) cannot both be 1 as they are in the same row"
        ]
}

(Note the sudoku eprime file indexes (col,row) instead of (row,col) so I have changed the "column" constraint to "row" in this output to better align with the above image).

This deduction is very much correct, but the explanation is wrong. It is true that cells (1,2) and (1,3) are in the same box, but this doesn't contribute to the deduction. Consider if it were cells (2,2) and (1,3) - they would still be in the same box, but the naked pair deduction would no longer hold for (1,4). It is therefore not the box constraint that makes this deduction correct, but the row constraint between (1,2) and (1,3).

From my observations, demystify will always choose the box constraint whenever possible, even if a row or column constraint is the correct explanation. I have only explored demystify within the context of Sudoku, but I would assume this issue occurs for other puzzles too. The box constraint is the last constraint defined in the eprime file which could be why this constraint is always chosen.

With this issue, it is not possible to accurately categorise the deductions made by demystify, as two identical deductions may look different.

@ChrisJefferson
Copy link
Collaborator

I'm not sure I would call this "wrong", if we need to know that (1,2) and (1,3) are different, then saying they are different because they are in the same box, or different because they are in the same row, are exactly the same I think?

I agree it might feel more "natural" to say it is because they are in the same row. The Essence' model actually has both constraints, and in this case demystify notices it has been given two logically identical constraints between (1,2) and (1,3), and throws away one of the two. We could change the 'box' constraint so when things are in the same row, or same column, we don't both putting the 'box' version of the constraint on (as it's implied).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants