The simplest requirement is that each ship appear only once out of the dozens of places it could be. The cells list holds the terms that are related to a single ship. The tree_one() function takes a list of terms and then constructs a binary tree out of them such that at most one of the terms will be true. The root value of this tree will be one if any of the leaves are active, and it will be zero if none of them are. Or (as in this case) if the root is set to one then one of the leaves must also be true. The function
cnf.write_one() creates a clause from the terms it is given - here by writing a clause of a single term, that single term must be true. Additionally a summary of how many legal positions there are for each ship will be displayed. Frequently one of the ships will be extremely constrained; normally puzzles are designed this way to give a human solver a place to start.