For example, to figure out when a piece should stay in place undisturbed, we have the following fairly complicated rule, where single_jump_capture is itself substantial and dependent on the current state of the board:
(<= (next (cell ?x ?y ?p)) (does ?player (move ?piece ?x1 ?y1 ?x2 ?y2)) (true (cell ?x ?y ?p)) (not (single_jump_capture ?player ?x1 ?y1 ?x ?y ?x2 ?y2)) (different_cells ?x ?y ?x1 ?y1) (different_cells ?x ?y ?x2 ?y2))
Checkers was a simple enough case for me to try rewriting it in a fairly short time (unlike chess). I had already considered rewriting it to deal with the messiness of how it implements triple jumps. Dealing with sentences with upwards of eight variables can be difficult for a rules engine to deal with, and the old rules don't allow for more than three jumps in a row. The new approach deals with chained jumps over multiple turns: if a player makes a jump and can make additional jumps with the same piece, they retain control and can make those jumps.
I used the rules from the World Checkers Draughts Federation to decide how to handle edge cases. For example, if a pawn is kinged during a capture, it can't continue a capture chain, even if it's available. The ending conditions for the game have also changed: the game now only ends in a draw after 20 turns with no pawn moves or captures (loosely resembling the real rules). When it is a draw, there is no advantage for the player with more pieces; victories must be complete.
Here's a link to the new set of game rules. To avoid confusion with the old rulesheets and keep a more international perspective, I've called this version of the game English draughts.
Here are the performance results. The first rules engine is the out-of-the-box ProverStateMachine from GGP-Base. The second is a modified, heavily optimized version of the ProverStateMachine. The third is the propnet-based rules engine that Alloy uses. Each was run for 60 seconds on random depth charges through the games in question. The unit is average number of state changes per second:
Note that the prover-based and propnet-based rules engines here chain their logic in different directions, so it's not obvious that an improvement for one would be an improvement for the other. In this case, there are substantial improvements for both kinds, roughly between 2.5x and 5x.
(The generated propnet is also smaller and takes less time to build than the propnets for the other two games, even though I neglected to add base and input rules.)
What techniques and principles led to performance improvements? Without A/B testing of one feature at a time, I don't have an evidence-based answer. However, any of the following may have helped:
- Track only which spaces have pieces in them, not which spaces are blank
- Don't have rules involving a large number of variables at once (thanks to eliminating the double and triple jumps)
- Stop using a turn-dependent "single_jump_capture" relation all over the place; use constants and minimize state checking
- Generally, keep the way the prover works in mind when writing rules, to make sure it short-circuits quickly and only goes down a minimal number of paths
- Don't keep track of the number of pieces on the board (thanks to the new rules for ending the game)