# PROBLEM 1 
from z3 import *
def read_dimacs(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()

    # Parse the preamble line
    preamble = lines[0].strip().split()
    assert preamble[0] == 'p' and preamble[1] == 'cnf'
    num_vars = int(preamble[2])
    num_clauses = int(preamble[3])

    clauses = []
    for line in lines[1:]:
        if line.startswith('c'):
            continue  # Skip comment lines
        clause = list(map(int, line.strip().split()))
        assert clause[-1] == 0  # Each clause should end with 0
        clauses.append(clause[:-1])  # Exclude the trailing 0

    assert len(clauses) == num_clauses
    return num_vars, clauses
def count_satisfying_assignments(num_vars, clauses):
    # Create Z3 variables
    vars = [Bool(f'x{i+1}') for i in range(num_vars)]
    solver = Solver()
    # Add clauses to the solver
    for clause in clauses:
        z3_clause = []
        for literal in clause:
            if literal > 0:
                z3_clause.append(vars[literal - 1])
            else:
                z3_clause.append(Not(vars[-literal - 1]))
        solver.add(Or(z3_clause))
    count = 0
    while solver.check() == sat:
        count += 1
        model = solver.model()
        # Create a blocking clause to prevent the same model from being found again
        blocking_clause = []
        for var in vars:
            if is_true(model[var]):
                blocking_clause.append(Not(var))
            else:
                blocking_clause.append(var)
        solver.add(Or(blocking_clause))
    return count
if __name__ == "__main__":
    num_vars, clauses = read_dimacs("input.dimacs")
    result = count_satisfying_assignments(num_vars, clauses)
    print(result)


# PROBLEM 2
from z3 import *
def count_light_on_configurations(n):
    # Create Z3 variables
    switches = [Bool(f'switch_{i}') for i in range(n)]
    solver = Solver()
    # Constraint 1: An odd number of switches are on
    parity = False
    for v in switches:
        parity = Xor(parity, v)
    solver.add(parity)
    # Constraint 2: No two adjacent switches are both on
    for i in range(n - 1):
        solver.add(Or(Not(switches[i]), Not(switches[i + 1])))
    # Constraint 3: The first or the last switch is on
    solver.add(Or(switches[0], switches[-1]))
    count = 0
    while solver.check() == sat:
        count += 1
        model = solver.model()
        # Create a blocking clause to prevent the same model from being found again
        blocking_clause = []
        for switch in switches:
            if is_true(model[switch]):
                blocking_clause.append(Not(switch))
            else:
                blocking_clause.append(switch)
        solver.add(Or(blocking_clause))
    return count
if __name__ == "__main__":
    n = int(input().strip())
    result = count_light_on_configurations(n)
    print(result)

#PROBLEM 3
from z3 import *

def read_input(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()
    n = int(lines[0].strip())
    constraints = []
    for line in lines[1:]:
        if line.strip():
            parts = list(map(int, line.strip().split()))
            constraints.append(parts)
    return n, constraints

def count_valid_assignments(n, constraints):
    X = [[Bool(f"x_{i}_{j}") for j in range(n)] for i in range(n)]
    solver = Solver()

    # 각 사람은 정확히 한 자리에 앉는다
    for i in range(n):
        row = [X[i][j] for j in range(n)]
        solver.add(AtMost(*row, 1))
        solver.add(AtLeast(*row, 1))

    # 각 자리는 정확히 한 사람이 앉는다
    for j in range(n):
        col = [X[i][j] for i in range(n)]
        solver.add(AtMost(*col, 1))
        solver.add(AtLeast(*col, 1))

    # 제약 조건 추가
    for constraint in constraints:
        if constraint[0] == 1:
            i, j = constraint[1] - 1, constraint[2] - 1
            solver.add(Not(X[i][j]))
        elif constraint[0] == 2:
            i, j = constraint[1] - 1, constraint[2] - 1
            solver.add(X[i][j])
        elif constraint[0] == 3:
            i, j = constraint[1] - 1, constraint[2] - 1
            for k in range(n - 1):
                solver.add(Or(Not(X[i][k]), Not(X[j][k + 1])))
                solver.add(Or(Not(X[j][k]), Not(X[i][k + 1])))

    # 해의 개수 세기
    count = 0
    while solver.check() == sat:
        count += 1
        model = solver.model()
        blocking_clause = []
        for i in range(n):
            for j in range(n):
                if is_true(model[X[i][j]]):
                    blocking_clause.append(Not(X[i][j]))
                else:
                    blocking_clause.append(X[i][j])
        solver.add(Or(blocking_clause))

    return count

if __name__ == "__main__":
    n, constraints = read_input("input.txt")
    result = count_valid_assignments(n, constraints)
    print(result)


#PROBLEM 4
from z3 import *
def read_input(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()
    n = int(lines[0].strip())
    skill_levels = list(map(int, lines[1].strip().split()))
    k = int(lines[2].strip())
    return n, skill_levels, k
def count_match_schedules(n, skill_levels, k):
    num_players = 2 * n
    # X_ij <-> player i is matched with player j
    X = [[Bool(f'x_{i}{j}') for j in range(num_players)] for i in range(num_players)]
    solver = Solver()
    # Each player is matched with exactly one other player
    for i in range(num_players):
        row = [X[i][j] for j in range(num_players) if i != j]
        solver.add(Or(row))              
        # Each match is between two players
        for j in range(num_players):
            if i != j:
                solver.add(X[i][j] == X[j][i])
            else:
                solver.add(Not(X[i][j]))
            for k in range(j + 1, num_players):
                if i != k and j != k:
                    solver.add(Or(Not(X[i][j]), Not(X[i][k])))
    # Skill level constraint
    for i in range(num_players):
        for j in range(i + 1, num_players):
            if abs(skill_levels[i] - skill_levels[j]) > k:
                solver.add(Not(X[i][j]))
    print (solver)
    count = 0
    while solver.check() == sat:
        count += 1
        model = solver.model()
        # Create a blocking clause to prevent the same model from being found again
        blocking_clause = []
        for i in range(num_players):
            for j in range(num_players):
                if is_true(model[X[i][j]]):
                    blocking_clause.append(Not(X[i][j]))
                else:
                    blocking_clause.append(X[i][j])
        solver.add(Or(blocking_clause))
    return count
if __name__ == "__main__":
    n, skill_levels, k = read_input("input.txt")
    result = count_match_schedules(n, skill_levels, k)
    print(result)


#PROBLEM 5
from z3 import *
def read_input(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()
    n, m = map(int, lines[0].strip().split())
    edges = []
    for line in lines[1:m+1]:
        u, v = map(int, line.strip().split())
        edges.append((u, v))
    constraints = []
    for line in lines[m+1:]:
        parts = list(map(int, line.strip().split()))
        constraints.append(parts)
    return n, edges, constraints
def find_shortest_path(n, edges, constraints):
    start = 0
    end = n - 1
    X = [[Bool(f'x_{i}{j}') for j in range(n)] for i in range(n)] # X_ij <-> edge from i to j is in the path
    pred = {}
    succ = {}
    for i in range(n):
        pred[i] = []
        succ[i] = []
    for u, v in edges:
        succ[u].append(v)
        pred[v].append(u)

    solver = Optimize()
    # if incoming edge to a node is in the path, an outgoing edge from the node must be in the path
    for u in range(n):
        preds = pred[u]
        succs = succ[u]
        pred_taken = Or([X[p][u] for p in preds]) if len(preds) > 0 else True
        succ_taken = Or([X[u][s] for s in succs]) if len(succs) > 0 else True
        succ_only_one_taken = True 
        for s in succs:
            others = [X[u][s2] for s2 in succs if s2 != s]
            succ_only_one_taken = And(succ_only_one_taken, Or(Not(X[u][s]), Not(Or(others))))
        solver.add(Implies(pred_taken, And(succ_taken, succ_only_one_taken)))
    for u in range(n):
        for v in range(n):
            if (u, v) in edges:
                solver.add_soft(X[u][v], -1)
    # add constraints
    for constraint in constraints:
        if constraint[0] == 1:
            # node that must be included
            node = constraint[1]
            incoming = pred.get(node, [])
            solver.add(Or([X[p][node] for p in incoming]))
        elif constraint[0] == 2:
            # node that must be excluded
            node = constraint[1]
            incoming = pred.get(node, [])
            outgoing = succ.get(node, [])
            solver.add(And([Not(X[p][node]) for p in incoming] + [Not(X[node][s]) for s in outgoing]))
        elif constraint[0] == 3:
            # if node1 is visited, node2 must be visited
            node1, node2 = constraint[1], constraint[2]
            incoming1 = pred.get(node1, [])
            incoming2 = pred.get(node2, [])
            if len(incoming1) == 0: 
                solver.add(Or([X[p][node2] for p in incoming2]))
            else:
                solver.add(Implies(Or([X[p][node1] for p in incoming1]), Or([X[p][node2] for p in incoming2])))
        elif constraint[0] == 4:
            # if node1 is visited, node2 cannot be visited
            node1, node2 = constraint[1], constraint[2]
            incoming1 = pred.get(node1, [])
            incoming2 = pred.get(node2, [])
            if len(incoming1) == 0: 
                solver.add(And([Not(X[p][node2]) for p in incoming2]))
            else:
                solver.add(Implies(Or([X[p][node1] for p in incoming1]), And([Not(X[p][node2]) for p in incoming2])))
    # starting and ending nodes
    solver.add(Or([X[start][s] for s in succ.get(start, [])]))
    solver.add(Or([X[p][end] for p in pred.get(end, [])]))
    # find the shortest path
    if solver.check() == sat:
        model = solver.model()
        path = []
        current = start
        while current != end:
            path.append(current)
            next_node = None
            for v in range(n):
                if (current, v) in edges and is_true(model[X[current][v]]):
                    next_node = v
                    break
            if next_node is None:
                return "No path"
            current = next_node
        path.append(end)
        return path
    else:
        return "No path"
if __name__ == "__main__":
    n, edges, constraints = read_input("input.txt")
    result = find_shortest_path(n, edges, constraints)
    print(result)


#PROBLEM 6
from z3 import *
def read_input(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()
    n, m = map(int, lines[0].strip().split())
    edges = []
    for line in lines[1:m+1]:
        u, v = map(int, line.strip().split())
        edges.append((u, v))
    k = int(lines[m+1].strip())
    taken_courses = list(map(int, lines[m+2].strip().split()))
    return n, edges, taken_courses
def count_course_combinations(n, edges, taken_courses):
    min_courses = 1
    taken_set = set(taken_courses)
    # Create Z3 variables
    X = [Bool(f'course_{i}') for i in range(n)]
    solver = Optimize()
    # Courses already taken 
    for course in taken_courses:
        solver.add(X[course])
    # Prerequisite constraints
    prereq = {i: [] for i in range(n)}
    for u, v in edges:
        prereq[v].append(u)
    for course in range(n):
        if course not in taken_set:
            for pre in prereq[course]:
                solver.add(Implies(X[course], X[pre]))
    for i in range(n):
        solver.add_soft(X[i], 1)
    count = 0
    while solver.check() == sat:
        take = 0
        model = solver.model()
        print(model)
        # Create a blocking clause to prevent the same model from being found again
        blocking_clause = []
        for i in range(n):
            if is_true(model[X[i]]):
                blocking_clause.append(Not(X[i]))
                take += 1
            else:
                blocking_clause.append(X[i])
        if take - len(taken_courses) < min_courses:
            break
        count += 1
        solver.add(Or(blocking_clause))
    return count
if __name__ == "__main__":
    n, edges, taken_courses = read_input("input.txt")
    result = count_course_combinations(n, edges, taken_courses)
    print(result)

	
#PROBLEM 7
from z3 import *
def read_input(file_path):
    with open(file_path, 'r') as f:
        lines = f.readlines()
    n = int(lines[0].strip())
    edges = []
    for line in lines[1:]:
        u, v = map(int, line.strip().split())
        edges.append((u, v))
    return n, edges
def min_colors(n, edges):
    nodes = [i for i in range(n)]
    k = n 
    while k >= 1: 
        # Step 1: Create Boolean variables
        color_vars = {
            node: [Bool(f"{node}_{c}") for c in range(k)]
            for node in nodes
        }
        solver = Solver()

        # Step 2: Each node gets exactly one color (1-hot)
        for node in nodes:
            # At least one color
            solver.add(Or(color_vars[node]))

        # At most one color
        for c1 in range(k):
            for c2 in range(c1 + 1, k):
                solver.add(Not(And(color_vars[node][c1], color_vars[node][c2])))

        # Step 3: Adjacent nodes must have different colors
        for node, neighbor in edges:
            for c in range(k):
                solver.add(Or(Not(color_vars[node][c]), Not(color_vars[neighbor][c])))

        # Step 4: Check satisfiability
        if solver.check() == sat:
            k = k - 1
        else: 
            return k + 1
    return k

if __name__ == "__main__":
    n, edges = read_input("input.txt")
    result = min_colors(n, edges)
    print(result)