aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKarel Kočí <cynerd@email.cz>2014-12-16 20:24:15 +0100
committerKarel Kočí <cynerd@email.cz>2014-12-16 20:24:15 +0100
commit0b9b90f209851b8db732408df66272f2ed9234b3 (patch)
treee04e1094dd0b6ff351e7032b39d98661299fc5e4
parent4ec68e612e5d6670a154677b4c8914f22153b122 (diff)
downloadlinux-conf-perf-0b9b90f209851b8db732408df66272f2ed9234b3.tar.gz
linux-conf-perf-0b9b90f209851b8db732408df66272f2ed9234b3.tar.bz2
linux-conf-perf-0b9b90f209851b8db732408df66272f2ed9234b3.zip
Add sat_solution
Added script for minisat input build and execute.
-rwxr-xr-xscripts/sat_solution24
1 files changed, 24 insertions, 0 deletions
diff --git a/scripts/sat_solution b/scripts/sat_solution
new file mode 100755
index 0000000..07d5118
--- /dev/null
+++ b/scripts/sat_solution
@@ -0,0 +1,24 @@
+#!/bin/bash
+
+SAT_FOLDER=$1
+RULES="$1/rules"
+SOLUTION="$1/solution"
+
+W_FILE=`mktemp`
+
+if [ -r "$RULES" ]; then
+ cat "$RULES" | sed 's/$/ 0/' > "$W_FILE"
+else
+ echo "Error: No rules file in specified folder." 1>&2
+ exit 1
+fi
+
+RL_COUNT=`wc -l < "$W_FILE"`
+NUM_VAR=`tail -1 "$RULES" | sed 's/ .*//' | sed 's/-//'`
+sed -i "1ip cnf $NUM_VAR $RL_COUNT" "$W_FILE"
+echo "CLAUSELES: $RL_COUNT"
+echo "VARIABLES: $NUM_VAR"
+
+minisat "$W_FILE" "$SOLUTION"
+
+rm "$W_FILE"