Too Many Constraints (Codeforces 1697F)
Tags: Others, 2-sat

You are asked to build an array $$$a$$$, consisting of $$$n$$$ integers, each element should be from $$$1$$$ to $$$k$$$.The array should be non-decreasing ($$$a_i \le a_{i+1}$$$ for all $$$i$$$ from $$$1$$$ to $$$n-1$$$). You are also given additional constraints on it. Each constraint is of one of three following types:   $$$1~i~x$$$: $$$a_i$$$ should not be equal to $$$x$$$;  $$$2~i~j~x$$$: $$$a_i + a_j$$$ should be less than or equal to $$$x$$$;  $$$3~i~j~x$$$: $$$a_i + a_j$$$ should be greater than or equal to $$$x$$$. Build any non-decreasing array that satisfies all constraints or report that no such array exists.

Input: The first line contains a single integer $$$t$$$ ($$$1 \le t \le 10^4$$$) — the number of testcases.The first line of each testcase contains three integers $$$n, m$$$ and $$$k$$$ ($$$2 \le n \le 2 \cdot 10^4$$$; $$$0 \le m \le 2 \cdot 10^4$$$; $$$2 \le k \le 10$$$).The $$$i$$$-th of the next $$$m$$$ lines contains a description of a constraint. Each constraint is of one of three following types:   $$$1~i~x$$$ ($$$1 \le i \le n$$$; $$$1 \le x \le k$$$): $$$a_i$$$ should not be equal to $$$x$$$;  $$$2~i~j~x$$$ ($$$1 \le i < j \le n$$$; $$$2 \le x \le 2 \cdot k$$$): $$$a_i + a_j$$$ should be less than or equal to $$$x$$$;  $$$3~i~j~x$$$ ($$$1 \le i < j \le n$$$; $$$2 \le x \le 2 \cdot k$$$): $$$a_i + a_j$$$ should be greater than or equal to $$$x$$$. The sum of $$$n$$$ over all testcases doesn't exceed $$$2 \cdot 10^4$$$. The sum of $$$m$$$ over all testcases doesn't exceed $$$2 \cdot 10^4$$$.

Output: For each testcase, determine if there exists a non-decreasing array that satisfies all conditions. If there is no such array, then print -1. Otherwise, print any valid array — $$$n$$$ integers from $$$1$$$ to $$$k$$$.


Sample Inputs:
4
4 0 4
2 2 3
3 1 2 3
1 2 2
3 3 2
1 1 1
2 2 3 2
3 2 3 2
5 5 5
3 2 5 7
2 4 5 10
3 4 5 6
3 3 4 7
2 1 5 7

Sample Outputs:
1 2 3 4
1 3
-1
1 2 2 5 5

Solution (Python):
import sys
readline = sys.stdin.readline

def SCC(N, edges):
    start = [0] * (N + 1)
    elist = [0] * len(edges)
    for e in edges:
        start[e[0] + 1] += 1
    for i in range(1, N + 1):
        start[i] += start[i - 1]
    counter = start[:]
    for e in edges:
        elist[counter[e[0]]] = e[1]
        counter[e[0]] += 1
    N = N
    now_ord = group_num = 0
    visited = []
    low = [0] * N
    order = [-1] * N
    ids = [0] * N
    parent = [-1] * N
    stack = []
    for i in range(N):
        if order[i] == -1:
            stack.append(i)
            stack.append(i)
            while stack:
                v = stack.pop()
                if order[v] == -1:
                    low[v] = order[v] = now_ord
                    now_ord += 1
                    visited.append(v)
                    for i in range(start[v], start[v + 1]):
                        to = elist[i]
                        if order[to] == -1:
                            stack.append(to)
                            stack.append(to)
                            parent[to] = v
                        else:
                            low[v] = min(low[v], order[to])
                else:
                    if low[v] == order[v]:
                        while True:
                            u = visited.pop()
                            order[u] = N
                            ids[u] = group_num
                            if u == v:
                                break
                        group_num += 1
                    if parent[v] != -1:
                        low[parent[v]] = min(low[parent[v]], low[v])
    for (i, x) in enumerate(ids):
        ids[i] = group_num - 1 - x
    groups = [[] for _ in range(group_num)]
    for (i, x) in enumerate(ids):
        groups[x].append(i)
    return groups

class TwoSAT:

    def __init__(self, N=None):
        self.N = N
        self.edges = []

    def Add_Clause(self, i, f, j, g):
        if self.N != None:
            assert 0 <= i < self.N
            assert 0 <= j < self.N
        self.edges.append((2 * i + (0 if f else 1), 2 * j + (1 if g else 0)))
        self.edges.append((2 * j + (0 if g else 1), 2 * i + (1 if f else 0)))

    def Satisfiable(self):
        N = self.N if self.N != None else max((max(i, j) for (i, j) in self.edges)) // 2 + 1
        scc = SCC(N * 2, self.edges)
        idx = [None] * N * 2
        for (i, lst) in enumerate(scc):
            for x in lst:
                idx[x] = i
        retu = [None] * N
        for i in range(N):
            if idx[2 * i] == idx[2 * i + 1]:
                return None
            retu[i] = idx[2 * i] < idx[2 * i + 1]
        return retu
T = int(readline())
for t in range(T):
    (N, M, K) = map(int, readline().split())
    TSAT = TwoSAT(N * (K + 2))
    for n in range(N):
        for k in range(K + 1):
            TSAT.Add_Clause(n * (K + 2) + k, 1, n * (K + 2) + k + 1, 0)
        TSAT.Add_Clause(n * (K + 2), 1, n * (K + 2), 1)
        TSAT.Add_Clause(n * (K + 2) + 1, 1, n * (K + 2) + 1, 1)
        TSAT.Add_Clause(n * (K + 2) + K + 1, 0, n * (K + 2) + K + 1, 0)
    for n in range(N - 1):
        for k in range(K + 2):
            TSAT.Add_Clause(n * (K + 2) + k, 0, (n + 1) * (K + 2) + k, 1)
    for m in range(M):
        query = tuple(map(int, readline().split()))
        if query[0] == 1:
            (_, i, x) = query
            i -= 1
            TSAT.Add_Clause(i * (K + 2) + x, 0, i * (K + 2) + x + 1, 1)
        elif query[0] == 2:
            (_, i, j, x) = query
            i -= 1
            j -= 1
            for k in range(K + 2):
                if 0 <= x + 1 - k <= K + 1:
                    TSAT.Add_Clause(i * (K + 2) + k, 0, j * (K + 2) + x + 1 - k, 0)
        else:
            (_, i, j, x) = query
            i -= 1
            j -= 1
            for k in range(K + 2):
                if 0 <= x + 1 - k <= K + 1:
                    TSAT.Add_Clause(i * (K + 2) + k, 1, j * (K + 2) + x + 1 - k, 1)
    lst = TSAT.Satisfiable()
    if lst == None:
        print(-1)
    else:
        ans_lst = [sum(lst[n * (K + 2):(n + 1) * (K + 2)]) - 1 for n in range(N)]
        print(*ans_lst)

Solution (Python):
import sys, os, io
input = io.BytesIO(os.read(0, os.fstat(0).st_size)).readline

def f(u, v):
    return u * (k + 2) + v + 1

def add_edge(u, v, tu, tv):
    e.append(u if not tu else u + n)
    e.append(v + n if not tv else v)
    e.append(v if not tv else v + n)
    e.append(u + n if not tu else u)
    return

def make_graph(n, e):
    m = len(e) >> 1
    (s1, s2) = ([0] * (n + 3), [0] * (n + 3))
    for i in range(0, 2 * m, 2):
        s1[e[i] + 2] += 1
        s2[e[i + 1] + 2] += 1
    for i in range(3, n + 3):
        s1[i] += s1[i - 1]
        s2[i] += s2[i - 1]
    (G, R) = ([0] * m, [0] * m)
    for i in range(2 * m):
        j = e[i] + 1
        if not i & 1:
            G[s1[j]] = e[i ^ 1]
            s1[j] += 1
        else:
            R[s2[j]] = e[i ^ 1]
            s2[j] += 1
    return (G, s1, R, s2)

def scc(n, G, s1, R, s2):
    now = list(s1)
    st = []
    u = [0] * (n + 1)
    c = 1
    for i in range(1, n + 1):
        if u[i]:
            continue
        (st, u[i]) = ([i], -1)
        while st:
            j = st[-1]
            while now[j] < s1[j + 1] and u[G[now[j]]]:
                now[j] += 1
            if now[j] == s1[j + 1]:
                u[st.pop()] = c
                c += 1
            else:
                st.append(G[now[j]])
                u[st[-1]] = -1
    v = [0] * n
    for i in range(1, n + 1):
        v[u[i] - 1] = i
    (c, z) = ([0] * (n + 1), 1)
    for i in v[::-1]:
        if c[i]:
            continue
        (q, c[i]) = ([i], z)
        for j in q:
            for w in range(s2[j], s2[j + 1]):
                k = R[w]
                if not c[k]:
                    q.append(k)
                    c[k] = z
        z += 1
    return c

def two_sat():
    (G, s1, R, s2) = make_graph(2 * n, e)
    c = scc(2 * n, G, s1, R, s2)
    (ok, z) = (1, [0] * (n + 1))
    for i in range(1, n + 1):
        if c[i] == c[i + n]:
            ok = 0
        elif c[i] < c[i + n]:
            z[i] = 1
    return (ok, z)
t = int(input())
ans = []
for t0 in range(t):
    (n, m, k) = map(int, input().split())
    n0 = n
    n = n * (k + 2)
    e = []
    for i in range(n0 - 1):
        for j in range(k + 2):
            add_edge(f(i, j), f(i + 1, j), 0, 1)
    for i in range(n0):
        for j in range(k + 1):
            add_edge(f(i, j), f(i, j + 1), 1, 0)
    for i in range(n0):
        add_edge(f(i, 1), f(i, 1), 1, 1)
        add_edge(f(i, k + 1), f(i, k + 1), 0, 0)
    for _ in range(m):
        q = list(map(int, input().split()))
        if q[0] == 1:
            (i, x) = (q[1], q[2])
            add_edge(f(i - 1, x), f(i - 1, x + 1), 0, 1)
            continue
        (q, i, j, x) = q
        for u in range(k + 2):
            for v in range(k + 2):
                if u + v == x + 1:
                    add_edge(f(i - 1, u), f(j - 1, v), q & 1, q & 1)
                    break
    (ok, z) = two_sat()
    if ok:
        (ans0, j) = ([0] * n0, 1)
        for i in range(n0):
            while not z[f(i, j)]:
                j += 1
            ans0[i] = j - 1
    else:
        ans0 = [-1]
    ans.append(' '.join(map(str, ans0)))
sys.stdout.write('\n'.join(ans))

Solution (Python):
import sys
readline = sys.stdin.readline

def SCC(N, edges):
    start = [0] * (N + 1)
    elist = [0] * len(edges)
    for e in edges:
        start[e[0] + 1] += 1
    for i in range(1, N + 1):
        start[i] += start[i - 1]
    counter = start[:]
    for e in edges:
        elist[counter[e[0]]] = e[1]
        counter[e[0]] += 1
    N = N
    now_ord = group_num = 0
    visited = []
    low = [0] * N
    order = [-1] * N
    ids = [0] * N
    parent = [-1] * N
    stack = []
    for i in range(N):
        if order[i] == -1:
            stack.append(i)
            stack.append(i)
            while stack:
                v = stack.pop()
                if order[v] == -1:
                    low[v] = order[v] = now_ord
                    now_ord += 1
                    visited.append(v)
                    for i in range(start[v], start[v + 1]):
                        to = elist[i]
                        if order[to] == -1:
                            stack.append(to)
                            stack.append(to)
                            parent[to] = v
                        else:
                            low[v] = min(low[v], order[to])
                else:
                    if low[v] == order[v]:
                        while True:
                            u = visited.pop()
                            order[u] = N
                            ids[u] = group_num
                            if u == v:
                                break
                        group_num += 1
                    if parent[v] != -1:
                        low[parent[v]] = min(low[parent[v]], low[v])
    for (i, x) in enumerate(ids):
        ids[i] = group_num - 1 - x
    groups = [[] for _ in range(group_num)]
    for (i, x) in enumerate(ids):
        groups[x].append(i)
    return groups

class TwoSAT:

    def __init__(self, N=None):
        self.N = N
        self.edges = []

    def Add_Clause(self, i, f, j, g):
        if self.N != None:
            assert 0 <= i < self.N
            assert 0 <= j < self.N
        self.edges.append((2 * i + (0 if f else 1), 2 * j + (1 if g else 0)))
        self.edges.append((2 * j + (0 if g else 1), 2 * i + (1 if f else 0)))

    def Satisfiable(self):
        N = self.N if self.N != None else max((max(i, j) for (i, j) in self.edges)) // 2 + 1
        scc = SCC(N * 2, self.edges)
        idx = [None] * N * 2
        for (i, lst) in enumerate(scc):
            for x in lst:
                idx[x] = i
        retu = [None] * N
        for i in range(N):
            if idx[2 * i] == idx[2 * i + 1]:
                return None
            retu[i] = idx[2 * i] < idx[2 * i + 1]
        return retu
T = int(readline())
for t in range(T):
    (N, M, K) = map(int, readline().split())
    TSAT = TwoSAT(N * (K + 2))
    for n in range(N):
        for k in range(K + 1):
            TSAT.Add_Clause(n * (K + 2) + k, 1, n * (K + 2) + k + 1, 0)
        TSAT.Add_Clause(n * (K + 2), 1, n * (K + 2), 1)
        TSAT.Add_Clause(n * (K + 2) + 1, 1, n * (K + 2) + 1, 1)
        TSAT.Add_Clause(n * (K + 2) + K + 1, 0, n * (K + 2) + K + 1, 0)
    for n in range(N - 1):
        for k in range(K + 2):
            TSAT.Add_Clause(n * (K + 2) + k, 0, (n + 1) * (K + 2) + k, 1)
    for m in range(M):
        query = tuple(map(int, readline().split()))
        if query[0] == 1:
            (_, i, x) = query
            i -= 1
            TSAT.Add_Clause(i * (K + 2) + x, 0, i * (K + 2) + x + 1, 1)
        elif query[0] == 2:
            (_, i, j, x) = query
            i -= 1
            j -= 1
            for k in range(K + 2):
                if 0 <= x + 1 - k <= K + 1:
                    TSAT.Add_Clause(i * (K + 2) + k, 0, j * (K + 2) + x + 1 - k, 0)
        else:
            (_, i, j, x) = query
            i -= 1
            j -= 1
            for k in range(K + 2):
                if 0 <= x + 1 - k <= K + 1:
                    TSAT.Add_Clause(i * (K + 2) + k, 1, j * (K + 2) + x + 1 - k, 1)
    lst = TSAT.Satisfiable()
    if lst == None:
        print(-1)
    else:
        ans_lst = [sum(lst[n * (K + 2):(n + 1) * (K + 2)]) - 1 for n in range(N)]
        print(*ans_lst)