Battleship

print('terms:', cnf.maxterm)
print('clauses:', cnf.clauses)
assert cnf.verify()

interesting = set(f(x,y) for x,y in product(xs, ys))
for solution in cnf.solutions(3, interesting=interesting):
    print()
    marked = {}
    used_ships = [s for s in all_ships if f(*s) in solution]
    for s in used_ships:
        marked.update(exact_ship(*s))
    for y in ys:
        line = ''
        for x in xs:
            if (x,y) in marked:
                line += marked[(x,y)]
            else:
                line += '.'
            line += ' '
        line = line.replace('~', '.')
        print(line)