結果
| 問題 |
No.470 Inverse S+T Problem
|
| ユーザー |
 qwewe
|
| 提出日時 | 2025-05-14 12:57:56 |
| 言語 | C++17 (gcc 13.3.0 + boost 1.87.0) |
| 結果 |
AC
|
| 実行時間 | 103 ms / 2,000 ms |
| コード長 | 12,646 bytes |
| コンパイル時間 | 3,116 ms |
| コンパイル使用メモリ | 122,332 KB |
| 実行使用メモリ | 36,748 KB |
| 最終ジャッジ日時 | 2025-05-14 12:59:23 |
| 合計ジャッジ時間 | 3,876 ms |
|
ジャッジサーバーID （参考情報） |
judge5 / judge3 |
（要ログイン）
| ファイルパターン | 結果 |
|---|---|
| sample | AC * 4 |
| other | AC * 27 |
ソースコード
#include <iostream>
#include <vector>
#include <string>
#include <map>
#include <vector>
#include <tuple>
#include <algorithm>
#include <set> // Include set if needed, though current logic doesn't use it directly
using namespace std;
// Structure to represent the 2-SAT problem using Kosaraju's algorithm for SCCs
struct TwoSAT {
int N_orig; // Original number of variables (N)
int n_vars; // Current total number of variables (N + auxiliary)
vector<vector<int>> adj; // Adjacency list for implication graph
vector<vector<int>> rev_adj; // Adjacency list for reversed graph
vector<bool> visited; // Visited flags for DFS traversals
vector<int> component; // Stores SCC component ID for each literal
vector<int> order; // Stores finish order from first DFS
int current_comp; // Counter for SCC IDs
// Constructor initializes with N original variables
TwoSAT(int N) : N_orig(N), n_vars(N) {
adj.resize(2 * N);
rev_adj.resize(2 * N);
}
// Resizes the graph structures if more variables (auxiliary) are added
void resize(int new_n_vars) {
if (new_n_vars > n_vars) {
adj.resize(2 * new_n_vars);
rev_adj.resize(2 * new_n_vars);
n_vars = new_n_vars;
}
}
// Computes the negation of a literal index
// Variable i is represented by literals 2*i (positive) and 2*i+1 (negative)
int neg(int lit) { return lit ^ 1; }
// Adds a directed edge u -> v to the implication graph
void add_edge(int u, int v) {
adj[u].push_back(v);
rev_adj[v].push_back(u);
}
// Adds a clause (u OR v) to the 2-SAT instance.
// This is equivalent to two implications: (NOT u -> v) and (NOT v -> u)
void add_clause(int u, int v) {
// Basic boundary check, important if resize logic has potential issues
if (neg(u) >= adj.size() || v >= adj.size() || neg(v) >= adj.size() || u >= adj.size()) {
cerr << "Error: Literal index out of bounds during clause addition." << endl;
exit(1); // Critical error, exit
}
add_edge(neg(u), v);
add_edge(neg(v), u);
}
// First DFS pass for Kosaraju's algorithm: compute finish times (order)
void dfs1(int u) {
visited[u] = true;
for (int v : adj[u]) {
if (!visited[v]) {
dfs1(v);
}
}
order.push_back(u);
}
// Second DFS pass for Kosaraju's algorithm: find SCCs on the reversed graph
void dfs2(int u) {
visited[u] = true;
component[u] = current_comp;
for (int v : rev_adj[u]) {
if (!visited[v]) {
dfs2(v);
}
}
}
// Solves the 2-SAT problem. Returns true if satisfiable, false otherwise.
// Fills the `assignment` vector with truth values for the original N variables if satisfiable.
bool solve(vector<bool>& assignment) {
int num_nodes = 2 * n_vars; // Total literals = 2 * total variables
visited.assign(num_nodes, false);
order.clear();
order.reserve(num_nodes); // Reserve space for efficiency
// Perform first DFS pass on all nodes to compute finish order
for (int i = 0; i < num_nodes; ++i) {
if (!visited[i]) {
dfs1(i);
}
}
visited.assign(num_nodes, false);
component.assign(num_nodes, -1); // Initialize component IDs to -1
current_comp = 0; // Start component IDs from 0
reverse(order.begin(), order.end()); // Process nodes in reverse finish order
// Perform second DFS pass on reversed graph to identify SCCs
for (int u : order) {
if (!visited[u]) {
dfs2(u);
current_comp++; // Increment component ID for next SCC
}
}
// Check for contradictions: variable `i` and its negation `NOT i` in the same SCC
for (int i = 0; i < N_orig; ++i) {
if (component[2 * i] == component[2 * i + 1]) {
// A conflict exists only if both literals belong to a valid SCC (component ID != -1)
if (component[2 * i] != -1) return false; // Unsatisfiable
}
}
// If no conflicts, find a satisfying assignment for original N variables
assignment.resize(N_orig);
for (int i = 0; i < N_orig; ++i) {
// Assign true to variable `i` if its positive literal `2*i` is in a component with a higher ID
// than its negative literal `2*i+1`. This corresponds to topological order of SCCs.
assignment[i] = (component[2 * i] > component[2 * i + 1]);
}
return true; // Satisfiable
}
};
// Map to store occurrences of each potential string: string -> list of (original_index, option_index, type)
map<string, vector<tuple<int, int, char>>> occurrences;
// Store the two possible pairs (S, T) for each input U_i
vector<pair<string, string>> options[100005];
int main() {
ios_base::sync_with_stdio(false); // Faster I/O
cin.tie(NULL);
int N; // Number of input strings U_i
cin >> N;
// Process each input string U_i
for (int i = 0; i < N; ++i) {
string U;
cin >> U;
options[i].reserve(2); // Optimization: reserve space for 2 pairs
// Option 0: lengths (1, 2)
string s1 = U.substr(0, 1);
string t1 = U.substr(1, 2);
options[i].push_back({s1, t1});
// Record occurrences of s1 and t1 for this option
occurrences[s1].emplace_back(i, 0, 'S');
occurrences[t1].emplace_back(i, 0, 'T');
// Option 1: lengths (2, 1)
string s2 = U.substr(0, 2);
string t2 = U.substr(2, 1);
options[i].push_back({s2, t2});
// Record occurrences of s2 and t2 for this option
occurrences[s2].emplace_back(i, 1, 'S');
occurrences[t2].emplace_back(i, 1, 'T');
}
// Initialize 2-SAT solver with N variables
TwoSAT ts(N);
int current_vars_count = N; // Track total variables including auxiliary ones
// Iterate through all unique strings found and their occurrences
for (auto const& [str, occ_list] : occurrences) {
vector<int> always_indices; // Indices i for which string 'str' appears regardless of option chosen
vector<tuple<int, int, char>> conditional_occurrences; // Occurrences where 'str' appears only for a specific option
map<int, vector<pair<int, char>>> occurrences_by_index; // Group occurrences by original index i
// Group occurrences by index i
for (const auto& occ : occ_list) {
// get<0>(occ) = index i (0..N-1), get<1>(occ) = option k (0 or 1)
occurrences_by_index[get<0>(occ)].push_back({get<1>(occ), get<2>(occ)});
}
// Identify always-X indices and conditional occurrences
for (auto const& [idx, pairs] : occurrences_by_index) {
bool has_opt0 = false, has_opt1 = false;
for(const auto& p : pairs) { // Check if string 'str' occurs for both option 0 and option 1 for index idx
if (p.first == 0) has_opt0 = true;
if (p.first == 1) has_opt1 = true;
}
if (has_opt0 && has_opt1) { // If occurs for both options, index idx is an always-X index
always_indices.push_back(idx);
} else { // Otherwise, all occurrences for this index are conditional
for(const auto& p : pairs) {
conditional_occurrences.emplace_back(idx, p.first, p.second);
}
}
}
// Check for immediate impossibility: If string 'str' must appear for two different indices regardless of choice
if (always_indices.size() >= 2) {
cout << "Impossible" << endl;
return 0;
}
// Handle constraints arising from one always-X index and conditional occurrences
if (always_indices.size() == 1) {
for (const auto& occ : conditional_occurrences) {
int i = get<0>(occ); // Index of the conditional occurrence
int k = get<1>(occ); // Option index (0 or 1) for this conditional occurrence
int var_i = i; // Variable index corresponding to U_i
int lit_to_make_true; // The literal that must be true due to the constraint
// If choosing option k for index i leads to conflict with the always-X index, we must NOT choose option k.
if (k == 0) {
// Must not choose option 0 => L_i must be false => NOT L_i must be true
lit_to_make_true = 2 * var_i + 1;
} else { // k == 1
// Must not choose option 1 => L_i must be true => L_i must be true
lit_to_make_true = 2 * var_i;
}
// Force this literal to be true by adding clause (lit OR lit)
ts.add_clause(lit_to_make_true, lit_to_make_true);
}
}
// Handle constraints among multiple conditional occurrences ("at most one" constraint)
if (always_indices.empty() && conditional_occurrences.size() >= 2) {
int m = conditional_occurrences.size(); // Number of conditional occurrences for string 'str'
int first_aux_var_idx = current_vars_count; // Starting index for auxiliary variables for this group
ts.resize(current_vars_count + m); // Ensure 2-SAT solver has space for m new auxiliary variables
vector<int> literals; // Literals representing the choice leading to the conditional occurrence
literals.reserve(m);
for(const auto& occ : conditional_occurrences) {
int i = get<0>(occ);
int k = get<1>(occ);
int var_i = i;
// Determine the literal corresponding to choosing option k for index i
if (k == 0) { // Choosing option 0 corresponds to L_i being true
literals.push_back(2 * var_i);
} else { // Choosing option 1 corresponds to L_i being false (NOT L_i being true)
literals.push_back(2 * var_i + 1);
}
}
// Implement "at most one" constraint using auxiliary variables s_1, ..., s_m
// s_j represents variable first_aux_var_idx + j - 1
// literal s_j is 2 * (first_aux_var_idx + j - 1)
int s_prev_lit = 2 * first_aux_var_idx; // Positive literal for s_1
// Base case: Clause 1 (NOT Lit_1 OR s_1)
ts.add_clause(ts.neg(literals[0]), s_prev_lit);
// Recursive step for j = 2 to m (indices 1 to m-1 in loop)
for (int j = 1; j < m; ++j) {
// s_{j+1} corresponds to variable first_aux_var_idx + j
int s_curr_lit = 2 * (first_aux_var_idx + j); // Positive literal for s_{j+1}
int Lit_j = literals[j]; // Literal for the j-th conditional occurrence (Lit_{j+1} in formula)
// Add clauses based on the standard encoding for "at most one":
// Clause 2: (NOT s_j OR s_{j+1}) equivalent to (s_j -> s_{j+1})
ts.add_clause(ts.neg(s_prev_lit), s_curr_lit);
// Clause 3: (NOT Lit_{j+1} OR s_{j+1}) equivalent to (Lit_{j+1} -> s_{j+1})
ts.add_clause(ts.neg(Lit_j), s_curr_lit);
// Clause 4: (NOT Lit_{j+1} OR NOT s_j) equivalent to NOT (Lit_{j+1} AND s_j)
ts.add_clause(ts.neg(Lit_j), ts.neg(s_prev_lit));
s_prev_lit = s_curr_lit; // Update s_prev literal for the next iteration
}
current_vars_count += m; // Increment total variable count
}
}
vector<bool> assignment; // Vector to store the resulting truth assignment
// Solve the 2-SAT instance
if (ts.solve(assignment)) {
// If satisfiable, print the chosen pairs (S_i, T_i) based on the assignment
for (int i = 0; i < N; ++i) {
// assignment[i] true => L_i true => choose option 0 (lengths 1, 2)
// assignment[i] false => L_i false => choose option 1 (lengths 2, 1)
int choice = assignment[i] ? 0 : 1;
cout << options[i][choice].first << " " << options[i][choice].second << "\n";
}
} else {
// If unsatisfiable, print "Impossible"
cout << "Impossible" << endl;
}
return 0;
}