Skip to content

Commit 5c86297

Browse files
conp-solutionsconp-solutions
authored
Merge pull request #73 from conp-solutions/eda-ai
Eda ai
2 parents 7a46b16 + 899dc7c commit 5c86297

File tree

7 files changed

+339
-0
lines changed

7 files changed

+339
-0
lines changed

‎tools/eda-ai/README‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
MergeSat (EDA-AI version), Norbert Manthey, Johannes Fichte, 2021
2+
3+
This package contains tools to solve CNF formulas with MergeSat.
4+
5+
## Quick Start
6+
7+
The following steps allow to solve a CNF INPUT_FILE:
8+
9+
```
10+
./build.sh # run once
11+
./binary/run_config*.sh "$INPUT_FILE" # run selected configuration on CNF
12+
```
13+
14+
## MergeSat in the EDA AI package
15+
16+
This package contains several configurations of the MergeSat solver. Each
17+
configuration package wlil select a single one. Hence, the instructions in this
18+
README file are generic, especially the step to solve the CNF.

‎tools/eda-ai/build.sh‎

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#!/bin/bash
2+
#
3+
4+
SELECTED_CONFIGURATION=1 # could be 1, 2 or 3
5+
6+
# locate the script to be able to call related scripts
7+
SCRIPT=$(readlink -e "$0")
8+
SCRIPTDIR=$(dirname "$SCRIPT")
9+
10+
# fail on error
11+
set -e
12+
13+
mkdir -p "$SCRIPTDIR"/binary
14+
OUTPUT_DIR=$(readlink -e "$SCRIPTDIR"/binary)
15+
16+
rsync -avz "$SCRIPTDIR"/code/mergesat/ "$OUTPUT_DIR"/mergesat-src/
17+
18+
pushd "$SCRIPTDIR"/binary/mergesat-src
19+
make r BUILD_TYPE=simp VERB= -j $(nproc)
20+
cp build/release/bin/mergesat "$OUTPUT_DIR"/
21+
cd "$OUTPUT_DIR"
22+
rm -rf mergesat-src
23+
popd
24+
25+
cp "$SCRIPTDIR"/code/mergesat/tools/eda-ai/run_config"$SELECTED_CONFIGURATION".sh "$OUTPUT_DIR"/
26+
27+
ls binary

‎tools/eda-ai/license.txt‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
MergeSat -- Copyright (c) 2021, Norbert Manthey
2+
3+
This file lists the license for the MergeSat package for EDA AI
4+
5+
### MergeSat License ###
6+
7+
Permission is hereby granted, free of charge, to any person obtaining a
8+
copy of this software and associated documentation files (the
9+
"Software"), to deal in the Software without restriction, including
10+
without limitation the rights to use, copy, modify, merge, publish,
11+
distribute, sublicense, and/or sell copies of the Software, and to
12+
permit persons to whom the Software is furnished to do so, subject to
13+
the following conditions:
14+
15+
The above copyright notice and this permission notice shall be included
16+
in all copies or substantial portions of the Software.
17+
18+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
19+
OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
20+
MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
21+
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
22+
LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
23+
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
24+
WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

‎tools/eda-ai/run_config1.sh‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
#!/bin/bash
2+
#
3+
# Tuned EDA AI Configuration:
4+
5+
6+
# locate the script to be able to call related scripts
7+
SCRIPT=$(readlink -e "$0")
8+
SCRIPTDIR=$(dirname "$SCRIPT")
9+
10+
# fail on error
11+
set -e
12+
13+
INPUT_FILE="$1"
14+
15+
if [ ! -r "$INPUT_FILE" ]; then
16+
echo "Cannot read input file $INPUT_FILE, abort"
17+
exit 1
18+
fi
19+
20+
exec "$SCRIPTDIR"/mergesat \
21+
-VSIDS-init-lim=10000\
22+
-VSIDS-lim=30000000\
23+
-no-almost-pure\
24+
-ccmin-mode=2\
25+
-ccnr-change-time=2000\
26+
-ccnr-change-time-inc=1\
27+
-ccnr-change-time-inc-inc=0.2\
28+
-ccnr-conflict-ratio=0.4\
29+
-no-ccnr-initial\
30+
-ccnr-ls-mems=50000000\
31+
-no-ccnr-mediation\
32+
-ccnr-percent-ratio=0.8987846297972459\
33+
-ccnr-restart-gap=300\
34+
-ccnr-switch-heuristic=500\
35+
-ccnr-up-time-ratio=0.2\
36+
-chrono=100\
37+
-cl-lim=20\
38+
-cla-decay=0.9990000000000001\
39+
-confl-to-chrono=4000\
40+
-core-size-lim=480195073\
41+
-core-size-lim-inc=0.1\
42+
-elim\
43+
-gc-frac=0.20000000000000023\
44+
-grow=0\
45+
-inprocess-delay=2.0\
46+
-inprocess-init-delay=-1\
47+
-inprocess-learnt-level=2\
48+
-inprocess-penalty=2\
49+
-lbd-avg-compare-limit=0.8000000000000004\
50+
-lcm\
51+
-lcm-core\
52+
-lcm-delay=1000\
53+
-lcm-delay-inc=1000\
54+
-lcm-dup-buffer=16\
55+
-lcm-reverse\
56+
-max-act-bump=100\
57+
-max-lbd-calc=100\
58+
-max-simp-cls=2147483647\
59+
-max-simp-steps=40000000000\
60+
-min-step-size=0.06000000000000003\
61+
-phase-saving=1\
62+
-pre\
63+
-pref-assumpts\
64+
-rfirst=100\
65+
-rinc=2.0\
66+
-rnd-freq=0.0\
67+
-rnd-init=0\
68+
-rnd-seed=9.16482529999E7\
69+
-rtype=2\
70+
-simp-gc-frac=0.49999999999999994\
71+
-sls-clause-lim=507381039\
72+
-sls-var-lim=-1\
73+
-step-size=0.40000000000000013\
74+
-step-size-dec=1.0E-4\
75+
-sub-lim=268761228\
76+
-use-backup-trail\
77+
-use-ccnr\
78+
-use-rephasing\
79+
-var-decay=0.8000000000000004\
80+
-var-decay-conflicts=5000\
81+
-vsids-c=12000000\
82+
-vsids-p=3000000000 \
83+
"$INPUT_FILE"

‎tools/eda-ai/run_config2.sh‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
#!/bin/bash
2+
#
3+
# Tuned EDA AI Configuration:
4+
5+
6+
# locate the script to be able to call related scripts
7+
SCRIPT=$(readlink -e "$0")
8+
SCRIPTDIR=$(dirname "$SCRIPT")
9+
10+
# fail on error
11+
set -e
12+
13+
INPUT_FILE="$1"
14+
15+
if [ ! -r "$INPUT_FILE" ]; then
16+
echo "Cannot read input file $INPUT_FILE, abort"
17+
exit 1
18+
fi
19+
20+
exec "$SCRIPTDIR"/mergesat \
21+
-VSIDS-init-lim=10000\
22+
-VSIDS-lim=30000000\
23+
-no-almost-pure\
24+
-ccmin-mode=2\
25+
-ccnr-change-time=2000\
26+
-ccnr-change-time-inc=1\
27+
-ccnr-change-time-inc-inc=0.2\
28+
-ccnr-conflict-ratio=0.4\
29+
-no-ccnr-initial\
30+
-ccnr-ls-mems=50000000\
31+
-no-ccnr-mediation\
32+
-ccnr-percent-ratio=0.9\
33+
-ccnr-restart-gap=300\
34+
-ccnr-switch-heuristic=500\
35+
-ccnr-up-time-ratio=0.2\
36+
-chrono=100\
37+
-cl-lim=20\
38+
-cla-decay=0.9990000000000001\
39+
-confl-to-chrono=4000\
40+
-core-size-lim=50000\
41+
-core-size-lim-inc=0.1\
42+
-elim\
43+
-gc-frac=0.20000000000000023\
44+
-grow=0\
45+
-inprocess-delay=2.0\
46+
-inprocess-init-delay=-1\
47+
-inprocess-learnt-level=2\
48+
-inprocess-penalty=2\
49+
-lbd-avg-compare-limit=0.8000000000000004\
50+
-lcm\
51+
-lcm-core\
52+
-lcm-delay=1000\
53+
-lcm-delay-inc=1000\
54+
-lcm-dup-buffer=16\
55+
-lcm-reverse\
56+
-max-act-bump=100\
57+
-max-lbd-calc=100\
58+
-max-simp-cls=2147483647\
59+
-max-simp-steps=40000000000\
60+
-min-step-size=0.06000000000000003\
61+
-phase-saving=2\
62+
-pre\
63+
-pref-assumpts\
64+
-rfirst=100\
65+
-rinc=2.0\
66+
-rnd-freq=0.0\
67+
-rnd-init=0\
68+
-rnd-seed=9.16482529999E7\
69+
-rtype=2\
70+
-simp-gc-frac=0.49999999999999994\
71+
-sls-clause-lim=-1\
72+
-sls-var-lim=-1\
73+
-step-size=0.40000000000000013\
74+
-step-size-dec=1.0E-4\
75+
-sub-lim=1000\
76+
-use-backup-trail\
77+
-use-ccnr\
78+
-use-rephasing\
79+
-var-decay=0.8000000000000004\
80+
-var-decay-conflicts=5000\
81+
-vsids-c=12000000\
82+
-vsids-p=3000000000 \
83+
"$INPUT_FILE"

‎tools/eda-ai/run_config3.sh‎

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
#!/bin/bash
2+
#
3+
# Tuned EDA AI Configuration:
4+
5+
6+
# locate the script to be able to call related scripts
7+
SCRIPT=$(readlink -e "$0")
8+
SCRIPTDIR=$(dirname "$SCRIPT")
9+
10+
# fail on error
11+
set -e
12+
13+
INPUT_FILE="$1"
14+
15+
if [ ! -r "$INPUT_FILE" ]; then
16+
echo "Cannot read input file $INPUT_FILE, abort"
17+
exit 1
18+
fi
19+
20+
exec "$SCRIPTDIR"/mergesat \
21+
-VSIDS-init-lim=1302817790\
22+
-VSIDS-lim=30000000\
23+
-no-almost-pure\
24+
-ccmin-mode=2\
25+
-ccnr-change-time=2000\
26+
-ccnr-change-time-inc=1\
27+
-ccnr-change-time-inc-inc=0.2\
28+
-ccnr-conflict-ratio=0.4\
29+
-no-ccnr-initial\
30+
-ccnr-ls-mems=50000000\
31+
-no-ccnr-mediation\
32+
-ccnr-percent-ratio=0.9\
33+
-ccnr-restart-gap=300\
34+
-ccnr-switch-heuristic=500\
35+
-ccnr-up-time-ratio=0.2\
36+
-chrono=100\
37+
-cl-lim=20\
38+
-cla-decay=0.9990000000000001\
39+
-confl-to-chrono=4000\
40+
-core-size-lim=50000\
41+
-core-size-lim-inc=0.1\
42+
-elim\
43+
-gc-frac=1.7917893266839732E-4\
44+
-grow=0\
45+
-inprocess-delay=2.0\
46+
-inprocess-init-delay=-1\
47+
-inprocess-learnt-level=2\
48+
-inprocess-penalty=2\
49+
-lbd-avg-compare-limit=0.8000000000000004\
50+
-lcm\
51+
-lcm-core\
52+
-lcm-delay=1000\
53+
-lcm-delay-inc=1000\
54+
-lcm-dup-buffer=16\
55+
-lcm-reverse\
56+
-max-act-bump=100\
57+
-max-lbd-calc=100\
58+
-max-simp-cls=2147483647\
59+
-max-simp-steps=40000000000\
60+
-min-step-size=0.06000000000000003\
61+
-phase-saving=2\
62+
-pre\
63+
-pref-assumpts\
64+
-rfirst=100\
65+
-rinc=2.0\
66+
-rnd-freq=0.0\
67+
-rnd-init=0\
68+
-rnd-seed=9.16482529999E7\
69+
-rtype=2\
70+
-simp-gc-frac=0.0021144031760272014\
71+
-sls-clause-lim=-1\
72+
-sls-var-lim=-1\
73+
-step-size=0.40000000000000013\
74+
-step-size-dec=1.0E-4\
75+
-sub-lim=1000\
76+
-use-backup-trail\
77+
-use-ccnr\
78+
-use-rephasing\
79+
-var-decay=0.4985624980489927\
80+
-var-decay-conflicts=5000\
81+
-vsids-c=12000000\
82+
-vsids-p=3000000000\
83+
"$INPUT_FILE"

‎tools/eda-ai/run_config_default.sh‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
#!/bin/bash
2+
#
3+
# Tuned EDA AI Configuration:
4+
5+
6+
# locate the script to be able to call related scripts
7+
SCRIPT=$(readlink -e "$0")
8+
SCRIPTDIR=$(dirname "$SCRIPT")
9+
10+
# fail on error
11+
set -e
12+
13+
INPUT_FILE="$1"
14+
15+
if [ ! -r "$INPUT_FILE" ]; then
16+
echo "Cannot read input file $INPUT_FILE, abort"
17+
exit 1
18+
fi
19+
20+
exec "$SCRIPTDIR"/mergesat \
21+
"$INPUT_FILE"

0 commit comments

Comments
 (0)