You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
<p>Code extracted from <ahref="https://github.com/deontic-logic/proof-tool" title="GitHub repository">deontic-logic/proof-tool</a> (still private; <ahref="https://deontic-logic.github.io/readme.html">readme</a>). Can be used to generate improved versions of <ahref="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> of the <ahref="https://us.metamath.org/mmsolitaire/mms.html" title="us.metamath.org/mmsolitaire/mms.html">mmsolitaire</a> project.<br>Exemplary generated results are available at <ahref="https://github.com/xamidi/mmsolitaire" title="GitHub repository">xamidi/mmsolitaire</a>.<br>Eligible for high-performance computing. If you have access to a powerful computer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.<br>The following table exemplary shows progress that has already been made.</p>
217
+
<p>Code initially extracted from <ahref="https://github.com/deontic-logic/proof-tool" title="GitHub repository">deontic-logic/proof-tool</a> (still private; <ahref="https://deontic-logic.github.io/readme.html">readme</a>). Can be used to generate improved versions of <ahref="https://us.metamath.org/mmsolitaire/pmproofs.txt" title="us.metamath.org/mmsolitaire/pmproofs.txt">pmproofs.txt</a> of the <ahref="https://us.metamath.org/mmsolitaire/mms.html" title="us.metamath.org/mmsolitaire/mms.html">mmsolitaire</a> project.<br>Exemplary generated results are available at <ahref="https://github.com/xamidi/mmsolitaire" title="GitHub repository">xamidi/mmsolitaire</a>.<br>Eligible for high-performance computing. If you have access to a powerful computer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.<br>The following table exemplary shows progress that has already been made.</p>
<p>For MPI-based filtering, each spawned process is multithreaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.<br>The following exemplary <ahref="https://slurm.schedmd.com/documentation.html">Slurm</a> batch script has been used via <ahref="https://slurm.schedmd.com/sbatch.html">sbatch</a> in order to reduce <code>dProofs31‑unfiltered31+.txt</code> to <code>dProofs31.txt</code>.</p>
318
+
<pre><code>#!/bin/zsh
319
+
#SBATCH --job-name=pmGen-20
320
+
#SBATCH --output=output_%J.txt
321
+
#SBATCH --partition=c18m
322
+
#SBATCH --account=rwth1392
323
+
#SBATCH --time=3-00:00:00
324
+
#SBATCH --mem-per-cpu=3900M
325
+
#SBATCH --cpus-per-task=48
326
+
#SBATCH --mail-user=<email>
327
+
#SBATCH --mail-type=END,FAIL,TIME_LIMIT
328
+
## Number of nodes to use ; Also update #processes (via srun)!
329
+
#SBATCH --nodes=6
330
+
srun -n 6 ./pmGenerator -m 31
331
+
</code></pre><p>A subsequent query with <ahref="https://slurm.schedmd.com/squeue.html">squeue</a> would then reveal the following information:</p>
Copy file name to clipboardExpand all lines: README.md
+30-1Lines changed: 30 additions & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -2,7 +2,7 @@
2
2
3
3
# @xamidi/pmGenerator
4
4
5
-
Code extracted from [deontic-logic/proof-tool](https://github.com/deontic-logic/proof-tool"GitHub repository") (still private; [readme](https://deontic-logic.github.io/readme.html)). Can be used to generate improved versions of [pmproofs.txt](https://us.metamath.org/mmsolitaire/pmproofs.txt"us.metamath.org/mmsolitaire/pmproofs.txt") of the [mmsolitaire](https://us.metamath.org/mmsolitaire/mms.html"us.metamath.org/mmsolitaire/mms.html") project.
5
+
Code initially extracted from [deontic-logic/proof-tool](https://github.com/deontic-logic/proof-tool"GitHub repository") (still private; [readme](https://deontic-logic.github.io/readme.html)). Can be used to generate improved versions of [pmproofs.txt](https://us.metamath.org/mmsolitaire/pmproofs.txt"us.metamath.org/mmsolitaire/pmproofs.txt") of the [mmsolitaire](https://us.metamath.org/mmsolitaire/mms.html"us.metamath.org/mmsolitaire/mms.html") project.
6
6
Exemplary generated results are available at [xamidi/mmsolitaire](https://github.com/xamidi/mmsolitaire"GitHub repository").
7
7
Eligible for high-performance computing. If you have access to a powerful computer, please consider to use this tool to further contribute to our knowledge regarding minimal proofs.
8
8
The following table exemplary shows progress that has already been made.
@@ -11,8 +11,11 @@ The following table exemplary shows progress that has already been made.
For MPI-based filtering, each spawned process is multithreaded and attempts to use as many threads as the hardware specifies as concurrent. Therefore, it is ideal to spawn the same amount of processes and nodes.
64
+
The following exemplary [Slurm](https://slurm.schedmd.com/documentation.html) batch script has been used via [sbatch](https://slurm.schedmd.com/sbatch.html) in order to reduce `dProofs31‑unfiltered31+.txt` to `dProofs31.txt`.
65
+
66
+
#!/bin/zsh
67
+
#SBATCH --job-name=pmGen-20
68
+
#SBATCH --output=output_%J.txt
69
+
#SBATCH --partition=c18m
70
+
#SBATCH --account=rwth1392
71
+
#SBATCH --time=3-00:00:00
72
+
#SBATCH --mem-per-cpu=3900M
73
+
#SBATCH --cpus-per-task=48
74
+
#SBATCH --mail-user=<email>
75
+
#SBATCH --mail-type=END,FAIL,TIME_LIMIT
76
+
## Number of nodes to use ; Also update #processes (via srun)!
77
+
#SBATCH --nodes=6
78
+
srun -n 6 ./pmGenerator -m 31
79
+
80
+
A subsequent query with [squeue](https://slurm.schedmd.com/squeue.html) would then reveal the following information:
Copy file name to clipboardExpand all lines: helper/FctHelper.cpp
+7Lines changed: 7 additions & 0 deletions
Original file line number
Diff line number
Diff line change
@@ -26,6 +26,13 @@ bool cmpStringGrow::operator()(const string& a, const string& b) const {
26
26
return a < b;
27
27
}
28
28
29
+
string FctHelper::mpi_nodeName() {
30
+
int len;
31
+
ManagedArray<char> arr(MPI_MAX_PROCESSOR_NAME);
32
+
MPI_Get_processor_name(arr.data, &len);
33
+
return arr.data;
34
+
}
35
+
29
36
// Templates for using values, static arrays and dynamic arrays on MPI_Send and MPI_Recv ("block until received", with extra mode "receive only if sent")
30
37
template<typename T> voidmpi_send(int rank, int count, MPI_Datatype type, const T* val, int dest, int tag, bool debug, auto printer) {
0 commit comments