<SYSTEM_TASK:>
Solve the following problem using Python, implementing the functions described below, one line at a time
<END_TASK>
<USER_TASK:>
Description:
 def expr2dimacssat(ex):
 """Convert an expression into an equivalent DIMACS SAT string."""

    if not ex.simple:
        raise ValueError("expected ex to be simplified")

    litmap, nvars = ex.encode_inputs()

    formula = _expr2sat(ex, litmap)
    if 'xor' in formula:
        if '=' in formula:
            fmt = 'satex'
        else:
            fmt = 'satx'
    elif '=' in formula:
        fmt = 'sate'
    else:
        fmt = 'sat'

    return "p {} {}\n{}".format(fmt, nvars, formula)