Proof Editor Tutorial
As an end user, your objective after opening a puzzle board is to logically prove your solving of the board or prove the board is unsolvable.
- Grid: A coordinate plane where each coordinate consists of a single cell.
-
Cell: An element in a grid (usually in the form of a square).
- A cell is unknown if its content is unknown.
- A cell is adjacent to another cell if they are orthogonally adjacent (orthogonal directions consist of left, right, up, and down).
- A cell adjoins another cell if they are either orthogonally or diagonally adjacent.
- Content: The content or data inside a single cell.
-
Adjacency Path: A path of cells that are adjacent to each other.
- i.e. A sequence of cells where any two successive cells in the sequence are adjacent to each other.
-
Adjacency Region: A set of cells that are all adjacent to each other.
- i.e. For any two cells of the set there is an adjacency path from one to the other.
- Proof Tree: The branching structure in the bottom of the proof editor when you are solving a puzzle.
-
Node: A circle or triangle in the proof tree, connected by a black line.
- Every node holds a board state, which is the board and all moves made up to the given node.
- A node is a leaf if there are no nodes that are directly connected to the right of it
- A transition node is one of the triangular nodes.
After running the Legup.jar file,
click Solve Puzzle. In the file navigation popup window, navigate to the LEGUP puzzles that you have downloaded. If you have cloned the repository, they can be found in C:\Users\your_username\Documents\GitHub\LEGUP\puzzles files. If you downloaded them for they class, they are in your computer's default download location.
LEGUP has multiple puzzles. Each puzzle has its own set of rules, but they all share common elements to make defining or interpreting a new puzzle fairly straightforward. Select a puzzle and press Open to begin solving it. Note that depending on the puzzle, as well as the specific instance of the grid for that puzzle (each exact file opened), certain functionalities may be in development and thus not fully complete.
For this example, we use a Light Up puzzle. Light Up Rules: https://github.com/Bram-Hub/Legup/wiki/Light%20up-Rules
To formally prove that you have solved a puzzle, you must prove each step you make. In the Rules section of the window, there are three types of rules: Direct rules, Case rules, and Contradiction rules.
- Direct rules are applied to a given move or set of moves to prove the next move logically follows. For example, it is required for no light bulbs to be around a black cell with '0' on it, which you apply the Direct rule "Finish With Empty".
- Case rules are applied when you can't apply a direct rule to make a move. These allow you to say, "What if this tile was a ___?" or "What if a direct rule was fulfilled for this tile?" and continue from there. All case rules allow you to create multiple branches of the puzzle, which are required to find every possible finished game board.
- Contradiction rules can be used at any time to prove that a given state of the board has an invalid group of tiles. If this is the case, no matter what other tiles you add, the board state selected will never have a valid solution. For example, if you reach a state where a Light Up cell with a '1' on it does not have any light bulbs around it, then you can apply the Contradiction rule "Too Few Bulbs" to invalidate the branch containing that board state. If all possible branches are invalid, then you have proved that the puzzle is impossible.
Select one of these categories in the Rules section to find all of a given type of rule or search for a specific rule in the Search Rules tab. If you hover over one of them with your cursor, there is a tiny popup of the rule description.
Tutorial on how to progress your proof tree:
First, you want to ensure you have selected the board state you wish to progress from. To do so, click on the node in the Proof Tree you want to select. Initially, there will only be one, representing the starting board state. When the node turns blue, it means you have selected it.
As you solve the puzzle, you can select any other node. The state of the board in the top-right section of the program will change as you click on different nodes to reflect the board state at that point in solving the puzzle.
NOTE: You may select multiple by holding Ctrl while clicking. This is necessary for merging nodes or deleting nodes from multiple branches at once.
Follow the tutorial of whatever puzzle you are solving to edit the board. In Light Up, you left-click on an unknown cell to cycle through the possible tile states of empty, light bulb, or unknown. In the Proof Tree, your changes will be made to a transition node that is connected to the node on the left. The changes made in the transition node are highlighted in green, and the node itself will be gray. Those moves have yet to be proven; now, you need to apply a direct rule to prove the move is valid.
NOTE: If you have selected a circular node, you will not be able to edit it; you can only edit transition nodes. The exception is for a leaf node, which will create a transition node for you, and your move will be represented in that node's board.
Go to the Rules section of the window and find the rule that must be applied to prove your move is valid. Typically, you have some rule in mind as you make a move; you just need to find the corresponding rule.
Left-click on the one.
If you apply the rule on a move that doesn't logically follow, the transition node will turn red, symbolizing a failure to apply the rule to your selected moves. To edit the rule used on the transition, you will need to reselect the transition node, then click on the rule you want to switch to. You can also directly edit the board in the transition node to see what nodes would or wouldn't follow from a given rule.
Make sure that you have selected a leaf node, then navigate to the Case Rules in the Rules tab. From there, select a case rule. The board will change, as you need to choose a cell to apply the case rule to. Those cells will be highlighted in blue. Click on one of them.
The proof tree will now display one node pointing to multiple nodes (if you selected a Case rule and cell that creates multiple cases). From there, you need to select one of the trees to continue editing from.
If at any time you see that the board state invalidates one of the fundamental rules of the puzzle, you should be able to prove that the board is invalid.
Make sure that you have selected the leaf node of the branch that contains the invalid board state. It is fine if this is the only branch in the tree.
Navigate to the Contradictions Rules in the rules tab and click on the corresponding rule the board states breaks. If the contradiction rule applies, all nodes in the branch will turn red and the lead node will point to an 'X'. If the rule is invalid, only the transition node will turn red; the leaf node will still point to an 'X', but that does not mean that the branch is invalid.
Important notes:
- Hovering over an arrow in the proof tree with your cursor shows - next to your cursor - the image corresponding to the rule you justified that move with. It also outlines in red the cells in the board which were changed that step.
- Hovering over a circle reveals the instance of the board that it represents, in the board window.
- You cannot backtrack and edit nodes directly; you need to select the transition nodes. Once you make those moves, they will be displayed on all future boards.
On the left of the proof tree, there are four extra features: Add, Remove, Merge, and Clean. The Clean option has not been implemented yet.
You can manually add a new node to the tree, but you will not have proven anything or made any new moves. You will still need to go back and apply rules to every move. We recommend letting the proof editor create the tree for you.
To remove a circle (board instance) or a step (arrow), have it selected by left clicking on it, and then press the - button in the proof tree section of the window. If you select a non-leaf node, it will delete all nodes after it, so be careful!
If this leave you with a transition node as a leaf, you can re-add the circular node using the Add tree element function.
What if I have multiple identical leaf nodes in my Proof Tree? You can merge them by selecting them both by clicking while holding Ctrl, and then pressing the merge button to the left of the Proof Tree, which looks like this:
to merge them to one node.
Once you have completed your proof tree, click 'Check' at the top, and it will display a message indicating if you did.
Currently, the only correct solution involves resolving all leaf branches to completion. In the future, there may be a goal state, such as proving if a certain cell is empty.