from random import random, shuffle
import re
from functools import reduce
from itertools import product


class State:
    def __init__(self):
        self.empty = False
        self.vars = [None]
        self.clauses = []
        self.trail = []
        self.dlevel = 0
        self.tlevel = 0


class Variable:
    def __init__(self):
        self.set = False
        self.sign = False
        self.mark = False
        self.unit = False
        self.unit_sign = False
        self.dlevel = 0
        self.reason = None
        self.watches = [[], []]

    def set_unit(self, sign):
        self.unit = True
        self.unit_sign = sign


#  Literal helper defs.


def literal_get_idx(literal):
    return abs(literal)


def literal_get_sign(literal):
    return literal < 0


def literal_get_var(state, literal):
    idx = literal_get_idx(literal)
    return state.vars[idx]


def literal_is_false(state, literal):
    v = literal_get_var(state, literal)
    return v.set and v.sign != literal_get_sign(literal)


def literal_get_mark(state, literal):
    v = literal_get_var(state, literal)
    return v.mark


def literal_add_watch(state, literal, clause):
    v = literal_get_var(state, literal)
    watch = v.watches[int(literal_get_sign(literal))]
    watch.append(clause)


def literal_set(state, literal, reason):
    v = literal_get_var(state, literal)
    v.sign = literal_get_sign(literal)
    v.set = True
    v.dlevel = state.dlevel
    v.reason = reason
    state.trail.append(literal)


def sat_add_clause(state, clause):
    n = len(clause)
    if n == 0:
        state.empty = True
        return None
    elif n == 1:
        v = literal_get_var(state, clause[0])
        sign = literal_get_sign(clause[0])
        if v.unit:
            if sign != v.unit_sign:
                state.empty = True
            return None

        v.set_unit(sign)
        return None
    else:
        literal_add_watch(state, clause[0], clause)
        literal_add_watch(state, clause[1], clause)


# Select a literal.  Chooses a literal at random (provided not already set).


def sat_select_literal(state):
    M = 1
    N = len(state.vars) - 1
    i = int(M + (N - M + 1) * random())
    i0 = i

    while state.vars[i].set:
        i += 1
        if i >= len(state.vars):
            i = 1
        if i == i0:
            return 0

    literal = -i if random() < 0.5 else i
    return literal


# Solver main loop.


def sat_solve(size, clauses):
    # Create the state:
    state = State()
    for i in range(size):
        state.vars.append(Variable())
    for i in range(len(clauses)):
        sat_add_clause(state, clauses[i])

    # UNSAT if empty clause has been asserted:
    if state.empty:
        return False, []

    # Find and propagate unit clauses:
    for i in range(1, len(state.vars)):
        v = state.vars[i]
        if v.unit:
            literal = -i if v.unit_sign else i
            if not sat_unit_propagate(state, literal, None):
                return False, []

    # Main loop:
    state.dlevel = 1
    num_sol = 0
    sols = []
    while 1:

        literal = sat_select_literal(state)
        if literal == 0:
            # // All variables are now set; and no conflicts; therefore SAT
            # print("solution :", [not x.sign for x in state.vars[1:]])
            # return True
            return (True, [not x.sign for x in state.vars[1:]])

        if not sat_unit_propagate(state, literal, None):
            #   UNSAT
            return (False, [])
            return (False, None)

        state.dlevel += 1
    print("only one solution")
    return True, sols if num_sol == 1 else False, []


# Unit propagation.


def sat_unit_propagate(state, literal, reason):
    restart = True
    while restart:
        curr = len(state.trail)
        _next = curr + 1

        literal_set(state, literal, reason)

        restart = False
        while curr < _next:
            literal = state.trail[curr]
            curr += 1
            literal = -literal
            v = literal_get_var(state, literal)
            watch = v.watches[int(literal_get_sign(literal))]

            i = 0
            while i < len(watch):
                _continue = False

                clause = watch[i]
                watch_idx = int(clause[0] == literal)
                watch_lit = clause[watch_idx]
                watch_sign = literal_get_sign(watch_lit)
                w = literal_get_var(state, watch_lit)
                if w.set and w.sign == watch_sign:
                    # 'clause' is true -- no work to do.
                    _continue = True
                if not _continue:
                    # Search for a non-false literal in 'clause'.
                    j = 2
                    while j < len(clause) and literal_is_false(
                            state, clause[j]):
                        j += 1

                    _continue1 = False
                    if j >= len(clause):
                        # // All other literals a false; use the other watch:
                        if not w.set:
                            # Implied set:
                            if watch_idx != 0:
                                clause[0] = watch_lit
                                clause[1] = literal

                            literal_set(state, watch_lit, clause)
                            _next += 1
                            _continue1 = True
                        if not _continue1:
                            #   All literals in 'clause' are false; conflict!
                            reason = sat_backtrack(state, clause)
                            if reason == None:
                                return False
                            literal = reason[0]
                            restart = True
                            break
                    if not _continue1:
                        # // Watch the other literal:
                        new_lit = clause[j]
                        clause[int(not watch_idx)] = new_lit
                        clause[j] = literal
                        literal_add_watch(state, new_lit, clause)
                        if i == len(watch) - 1:
                            watch.pop()
                        else:
                            watch[i] = watch.pop()
                            i -= 1
                i += 1
            if restart:
                break

    return True


# Backtracking and no-good learning.


def sat_backtrack(state, reason):
    conflicts = []

    # Level 0 failure; no work to do.
    if state.dlevel == 0:
        return None

    # Mark literals in reason:
    count = 0
    for i in range(len(reason)):
        v = literal_get_var(state, reason[i])
        if v.dlevel == 0:
            continue
        v.mark = True
        if v.dlevel < state.dlevel:
            conflicts.append(reason[i])
        else:
            count += 1

    # Find the UIP and collect conflicts:
    tlevel = len(state.trail) - 1
    while 1:
        if tlevel < 0:
            return None

        literal = state.trail[tlevel]
        tlevel -= 1
        v = literal_get_var(state, literal)
        v.set = False
        if not v.mark:
            continue
        v.mark = False
        count -= 1
        if count <= 0:
            break
        for i in range(1, len(v.reason)):
            literal = v.reason[i]
            w = literal_get_var(state, literal)
            if w.mark or w.dlevel == 0:
                continue
            if w.dlevel < state.dlevel:
                conflicts.append(literal)
            else:
                count += 1
            w.mark = True

    # Simplify the conflicts; create the no-good.
    nogood = [-literal]
    blevel = 0
    for i in range(len(conflicts)):
        literal = conflicts[i]
        v = literal_get_var(state, literal)
        if v.reason != None:
            k = 1
            while k < len(v.reason) and literal_get_mark(state, v.reason[k]):
                k += 1
            if k >= len(v.reason):
                continue

        nogood.append(literal)
        if blevel < v.dlevel:
            blevel = v.dlevel
            nogood[-1] = nogood[1]
            nogood[1] = literal

    # // Unwind the trail:
    while (tlevel >= 0):
        literal = state.trail[tlevel]
        v = literal_get_var(state, literal)
        if v.dlevel <= blevel:
            break
        v.set = False
        tlevel -= 1
    _len = len(state.trail)
    if tlevel + 1 <= _len:
        state.trail = state.trail[:tlevel + 1]
    else:
        state.trail.extend([None for _ in range(tlevel + 1 - _len)])

    # // Clear the marks:
    for i in range(len(conflicts)):
        v = literal_get_var(state, conflicts[i])
        v.mark = False

    # // Add the no-good clause:
    sat_add_clause(state, nogood)
    state.dlevel = blevel
    if state.empty:
        return None

    return nogood
    
def find_out_mr_wrong(cnvs):    
    m = len(cnvs)
    names = set(conv.split(':')[0] for conv in cnvs)
    hsh = {name: i for i, name in enumerate(names)}
    # number of persons
    n = len(hsh)
    dct = {n: [] for n in names}
    for cnv in cnvs:
        name, statement = cnv.split(":")
        dct[name].append(statement)
    initial_cdts = []
    initial_cdts.extend([[k * n + i + 1 for k in range(n)] for i in range(n)])
    initial_cdts.extend([[i * n + k + 1 for k in range(n)] for i in range(n)])

    initial_cdts.append([n * n + k + 1 for k in range(n)])
    for k in range(n):
        for l in range(k + 1, n):
            initial_cdts.append([-(n * n + k + 1), -(n * n + l + 1)])
    for i in range(n):
        for k in range(n):
            for l in range(k + 1, n):
                initial_cdts.append([-(k * n + i + 1), -(l * n + i + 1)])
    for i in range(n):
        for k in range(n):
            for l in range(k + 1, n):
                initial_cdts.append([-(i * n + k + 1), -(i * n + l + 1)])

    def make_cdt(name, info):
        name_idx = hsh[name] 
        rxp0 = r"I'm in (\w+) position"
        rxp1 = r"The man behind me is (\w+)."
        rxp2 = r"The man in front of me is (\w+)."
        rxp3 = r"There (?:are|is) (\w+) people in front of me."
        rxp4 = r"There (?:are|is) (\w+) people behind me."
        ms = [re.match(rxp, info) for rxp in (rxp0, rxp1, rxp2, rxp3, rxp4)]
        idx = next((i for i in range(5) if bool(ms[i])), None)
        s = ms[idx].groups()[0]

        match idx:
            case 0:
                num_str = re.search(r'(\d+)', s).groups()[0]
                k = int(num_str) - 1               
                cdt1 = [[name_idx * n + k + 1]]
                cdt2 = [[-(name_idx * n + k + 1)]]                
            case 1:
                other_idx = hsh[s]
                cdt1 = [[-(name_idx * n + i + 1), (other_idx * n + i + 2)] for i in range(n - 1)] + [[-(name_idx * n + n)]]               
                cdt2 = [[name_idx * n + n, -(name_idx * n + i + 1), -(other_idx * n + i + 2)] for i in range(n - 1)] 
            case 2:
                other_idx = hsh[s]
                cdt1 = [[-(name_idx * n + i + 1), (other_idx * n + i)] for i in range(1, n)] + [[-(name_idx * n + 1)]]
                cdt2 = [[name_idx * n + 1, -(name_idx * n + i + 1), -(other_idx * n + i)] for i in range(1, n)] 
            case 3:
                num_str = re.search(r'(\d+)', s).groups()[0]
                k = int(num_str)
                cdt1 = [[name_idx * n + k + 1]]
                cdt2 = [[-(name_idx * n + k + 1)]]
            case 4:
                num_str = re.search(r'(\d+)', s).groups()[0]
                k = n - int(num_str) - 1
                cdt1 = [[name_idx * n + k + 1]]
                cdt2 = [[-(name_idx * n + k + 1)]]

        return [cdt1, cdt2]
        
    def get_cdts():
        cdts_hsh = {n: [[], []] for n in names}
        names_arr = ["" for _ in range(n)]
        
        for name, infos in dct.items():
            for info in infos:
                cdt0, cdt1 = make_cdt(name, info)
                # print("name:", name)
                # print("info:", info)
                # print("cdt:", cdt, sep='\n')
                cdts_hsh[name][0].extend(cdt0)
                cdts_hsh[name][1].extend(cdt1)
        cur_cdts = [r[:] for r in initial_cdts]
        for name, cdts in cdts_hsh.items():
            cdt0, cdt1 = cdts
            idx = hsh[name]
            names_arr[idx] = name
            cur_cdts.extend([n * n + idx + 1] + cdt for cdt in cdt0)
            cur_cdts.extend([-(n * n + idx + 1)]  + cdt for cdt in cdt1)
        return names_arr, cur_cdts
        
    names_arr, cur_cdts = get_cdts()
    b, ans = sat_solve(n * (n + 1), cur_cdts)
    if not b:
        return None
    for i in range(n):
        if ans[n * n + i]:
            liar = names_arr[i]
            break
    idx = hsh[liar]
    cur_cdts.append([-(n * n + idx + 1)])
    b1, ans1 = sat_solve(n * (n + 1), cur_cdts)
    if not b1:
        return liar
    return None


samples = [
    #  conversation                                   Mr. Wrong
    
    (["John:I'm in 1st position.",
      "Peter:I'm in 2nd position.",
      "Tom:I'm in 1st position.",
      'Peter:The man behind me is Tom.'],              'Tom'),

    (["John:I'm in 1st position.",
      "Peter:I'm in 2nd position.",
      "Tom:I'm in 1st position.",
      'Peter:The man in front of me is Tom.'],         'John'),

    (["John:I'm in 1st position.",
      'Peter:There is 1 people in front of me.',
      'Tom:There are 2 people behind me.',
      'Peter:The man behind me is Tom.'],              'Tom'),

    (['John:The man behind me is Peter.',
      'Peter:There is 1 people in front of me.',
      'Tom:There are 2 people behind me.',
      'Peter:The man behind me is Tom.'],               None),

    (['Dowfls:There is 0 people behind me.',
      "Dowfls:I'm in 4th position.",
      "Ljiyxbmr:I'm in 2nd position.",
      'Ljiyxbmr:There is 1 people in front of me.',
      'Cvvugb:There are 2 people in front of me.',
      'Cvvugb:There is 1 people behind me.',
      'Tzjlvruhk:The man behind me is Dowfls.',
      'Tzjlvruhk:There are 2 people in front of me.'],  None),
    
    (["Tom:The man behind me is Bob.",
      "Bob:The man in front of me is Tom.",
      "Bob:The man behind me is Gary.",
      "Gary:The man in front of me is Bob.",
      "Fred:I'm in 1st position."],  "Fred"),
    
    (['Ivivue:The man in front of me is Eeznx.',
     'Wxnaz:The man behind me is Eeznx.',
     'Eeznx:The man in front of me is Wxnaz.',
     'Picgcavr:The man behind me is Eeznx.']
     ,'Picgcavr'),
    
    (["Wrong:The man behind me is Wrong."], "Wrong")
]

for convs, ans in samples:
    sol = find_out_mr_wrong(convs)
    print(sol, ans)