Binairo
Fill the grid with black and white circles: never three equal circles in a row or column, every line half black, half white, and no two rows — or columns — alike. Click a cell to cycle black → white → clear.
The solver never learns the human trick catalog. Instead it enumerates — once per size — the dictionary of all binary words that are legal as one line: balanced (half of each color) and triple-free. Each row and each column ranges over that dictionary; propagation keeps, per line, the candidate words matching its decided cells and projects: a cell on which every surviving word agrees is decided. The classic techniques are shadows of that single projection — a sandwich 1 _ 1 forces the 0 because every candidate says so, a pair flanks itself for the same reason, and a color at quota flips the rest of its line. The no-duplicate rule becomes alldifferent over the dictionary: a word already spent by a finished parallel line is removed from every sibling's candidates — which is exactly the human "don't copy that finished row" move. Run to a fixpoint this is as strong as enumerating each whole line; when it stalls, a search branches on the line with the fewest candidates left and proves every bundled board has a single solution. Boards are authored answer-first — a full grid built row-by-row out of the dictionary, givens greedily deleted while uniqueness survives — so every remaining given is load-bearing.