Proving Equivalences
Time Limit: 4000/2000 MS (Java/Others) Memory Limit: 32768/32768 K (Java/Others)
Total Submission(s): 2738 Accepted Submission(s): 1031
Problem Description
Consider the following exercise, found in a generic linear algebra textbook.
Let A be an n × n matrix. Prove that the following statements are equivalent:
1. A is invertible.
2. Ax = b has exactly one solution for every n × 1 matrix b.
3. Ax = b is consistent for every n × 1 matrix b.
4. Ax = 0 has only the trivial solution x = 0.
The typical way to solve such an exercise is to show a series of implications. For instance, one can proceed by showing that (a) implies (b), that (b) implies (c), that (c) implies (d), and finally that (d) implies (a). These four implications show that the four statements are equivalent.
Another way would be to show that (a) is equivalent to (b) (by proving that (a) implies (b) and that (b) implies (a)), that (b) is equivalent to (c), and that (c) is equivalent to (d). However, this way requires proving six implications, which is clearly a lot more work than just proving four implications!
I have been given some similar tasks, and have already started proving some implications. Now I wonder, how many more implications do I have to prove? Can you help me determine this?
Let A be an n × n matrix. Prove that the following statements are equivalent:
1. A is invertible.
2. Ax = b has exactly one solution for every n × 1 matrix b.
3. Ax = b is consistent for every n × 1 matrix b.
4. Ax = 0 has only the trivial solution x = 0.
The typical way to solve such an exercise is to show a series of implications. For instance, one can proceed by showing that (a) implies (b), that (b) implies (c), that (c) implies (d), and finally that (d) implies (a). These four implications show that the four statements are equivalent.
Another way would be to show that (a) is equivalent to (b) (by proving that (a) implies (b) and that (b) implies (a)), that (b) is equivalent to (c), and that (c) is equivalent to (d). However, this way requires proving six implications, which is clearly a lot more work than just proving four implications!
I have been given some similar tasks, and have already started proving some implications. Now I wonder, how many more implications do I have to prove? Can you help me determine this?
Input
On the first line one positive number: the number of testcases, at most 100. After that per testcase:
* One line containing two integers n (1 ≤ n ≤ 20000) and m (0 ≤ m ≤ 50000): the number of statements and the number of implications that have already been proved.
* m lines with two integers s1 and s2 (1 ≤ s1, s2 ≤ n and s1 ≠ s2) each, indicating that it has been proved that statement s1 implies statement s2.
* One line containing two integers n (1 ≤ n ≤ 20000) and m (0 ≤ m ≤ 50000): the number of statements and the number of implications that have already been proved.
* m lines with two integers s1 and s2 (1 ≤ s1, s2 ≤ n and s1 ≠ s2) each, indicating that it has been proved that statement s1 implies statement s2.
Output
Per testcase:
* One line with the minimum number of additional implications that need to be proved in order to prove that all statements are equivalent.
* One line with the minimum number of additional implications that need to be proved in order to prove that all statements are equivalent.
Sample Input
2
4 0
3 2
1 2
1 3
Sample Output
4
2
题意:
给出 T(<= 100) 组case。后每组 case 首先给出 n(1 ~ 2000) 和 m(0 ~ 5000),代表有 N 个命题 和 M 条关系,每条关系式给出连个数,a 和 b 代表 a -> b。现要求所以的命题全部等价,即 a <-> b,b <-> c…… 输出最小要添加多少条关系来满足要求。
思路:
强连通分量。强连通缩点后,max (入度为 0 的节点数, 出度为 0 的节点数)即为所求。注意当本身已经为强连通时,输出 0 。
AC:
#include <cstdio> #include <algorithm> #include <cstring> #include <vector> #include <stack> using namespace std; const int NMAX = 20005; const int EMAX = 50005 * 2; int n, m; vector<int> v[NMAX]; int scc_cnt, dfs_clock; int pre[NMAX], low[NMAX], cmp[NMAX]; stack<int> s; int out[NMAX], in[NMAX]; void dfs(int u) { pre[u] = low[u] = ++dfs_clock; s.push(u); for (int i = 0; i < v[u].size(); ++i) { if (!pre[ v[u][i] ]) { dfs( v[u][i] ); low[u] = min(low[u], low[ v[u][i] ]); } else if (!cmp[ v[u][i] ]) { low[u] = min(low[u], pre[ v[u][i] ]); } } if (pre[u] == low[u]) { ++scc_cnt; for( ;;){ int x = s.top(); s.pop(); cmp[x] = scc_cnt; if (x == u) break; } } } void scc() { scc_cnt = dfs_clock = 0; memset(pre, 0, sizeof(pre)); memset(cmp, 0, sizeof(cmp)); for (int i = 1; i <= n; ++i) { if (!pre[i]) dfs(i); } } void make_scc() { for (int i = 1; i <= scc_cnt; ++i) { out[i] = in[i] = 0; } for (int i = 1; i <= n; ++i) { for (int j = 0; j < v[i].size(); ++j) { if (cmp[i] != cmp[ v[i][j] ]) { ++in[ cmp[v[i][j]] ]; ++out[ cmp[i] ]; } } } } int main() { int t; scanf("%d", &t); while (t--) { scanf("%d%d", &n, &m); for (int i = 1; i <= n; ++i) v[i].clear(); while (m--) { int f, t; scanf("%d%d", &f, &t); v[f].push_back(t); } scc(); if (scc_cnt == 1) printf("0\n"); else { make_scc(); int o_n = 0, i_n = 0; for (int i = 1; i <= scc_cnt; ++i) { if (!out[i]) ++o_n; if (!in[i]) ++i_n; } printf("%d\n", max(o_n, i_n)); } } }
相关推荐
Interactive+Theorem+Proving+and+Program+Development.
另一个问题是"Proving Equivalences",需要计算添加最少的边使图强连通,答案是出度为0的连通块数量和入度为0的连通块数量中的较大值。在处理这类问题时,可以考虑将出度为0的节点连接起来形成环。 总的来说,图的...
- **扩展性强**:Coq支持用户自定义推理规则和策略,可以根据具体需求定制证明环境。 ### 4. Calculus of Inductive Constructions (构造归纳演算) - **定义**:构造归纳演算(CIC)是一种形式化的逻辑系统,它是...
arma3的一试验场扩展,其功能全面丰富,内容有趣
自动定理证明(Automated Theorem Proving,简称ATP)是计算机科学和数理逻辑领域中的一项重要技术,它涉及到让计算机自动进行数学定理的证明。这一领域涉及的范围很广,包括了逻辑、算法、数据结构、人工智能、形式...
This book, which is based on Pólya's method of problem solving, aids students in their transition from calculus (or precalculus) to higher-level mathematics. The book begins by providing a great deal...
It is shown that any recognition problem solved by a polynomial time-bounded nondeterministic Turing machine can be “reduced” to the problem of determining whether a given propositional formula is a...
精益定理证明使用Sphinx和重组文本构建。如何建造确保已安装精益软件。...如何测试精益代码段 make leantest如何部署 ./deploy.sh leanprover theorem_proving_in_lean如何贡献欢迎提出更正请求。 请遵循我们的commit
ANSI ASCE CI 71-21 Identifying, Quantifying, and Proving Loss of Productivity.pdf
标题《MECHANICAL NON-SOLUTION PROVING OF FAKE DIRAC EQUATION》(伪Dirac方程无解的机器证明)所指的知识点涉及理论物理学领域,特别是量子力学中Dirac方程的真实性和解的存在性问题。Dirac方程是量子力学中描述...
### Coq's Art:交互式定理证明与程序开发 #### 概述 《Coq's Art:交互式定理证明与程序开发》是一本深入介绍Coq系统及其理论基础——归纳构造演算(Calculus of Inductive Constructions)的著作。...
Openfinance是美国证监会批准的第一个STO股权交易所,openfinance用区块链技术解决传统的IPO所面临的局限性。
使学生对自动定理证明中的核心技术有透彻的了解,使他们能够将方法转移到不同的逻辑或应用程序中。
《3D Proving Ground:一个开源的Java3D粒子引擎》 在计算机图形学的世界里,粒子系统是一种广泛用于模拟复杂动态效果的技术,如火、烟雾、水、爆炸等。"3D Proving Ground"项目就是这样一个专注于开发Java3D可视化...
这是关于数学的电子书,高清,最新版本,经典著作,英文版
主要针对ipfs方向的爱好者使用
### SQL查询安全性证明 #### 摘要与背景 本文献主要探讨了SQL查询的安全性问题,特别是如何在运行时避免可能出现的错误。虽然SQL作为一种声明性语言,但在某些情况下仍可能遇到依赖于数据的运行时错误。...