from pathlib import Path
from typing import List


def update_file(filename: Path, solution: List[int]):
    """Updates a CNF file by adding a solution to the enclosed problem to the
    header. This allows CryptoMiniSAT to find additional (distinct) solutions
    to the problem.
    """

    def update_header(additional_clause_count: int, header: str) -> str:
        segments = header.strip().split()
        new_clause_count = int(segments[3]) + additional_clause_count
        return ' '.join(segments[:3] + [str(new_clause_count)])

    def add_clause_to_header(clause: str) -> str:
        return update_header(1, clause)

    lines = filename.read_text().strip().splitlines()
    updated_header = add_clause_to_header(lines[0])
    negated_solution = [-1 * var for var in solution]
    negated_solution_str = ' '.join(str(var) for var in negated_solution + [0])
    updated_lines = [updated_header] + lines[1:] + [negated_solution_str]
    updated_contents = '\n'.join(updated_lines)
    filename.write_text(updated_contents)