Merge pull request #68 from conp-solutions/wip-support

Wip support

.github/workflows/check-diversity.yml

@@ -0,0 +1,23 @@
+name: Check diversity configurations
+
+on: [push]
+
+jobs:
+  Linux:
+
+    runs-on: ubuntu-20.04
+
+    steps:
+    - name: Install Packages
+      run: sudo apt-get install zlib1g-dev make cmake picosat
+
+    - uses: actions/checkout@v1
+
+    - name: run CI script
+      env:
+        RUNDIVERSIFY: 1
+        RUNFUZZ: 0
+        RUNSTAREXEC: 0
+        RUNIPASIR: 0
+        RUNOPENWBO: 0
+      run: ./tools/ci.sh

minisat/core/Solver.cc

@@ -916,7 +916,7 @@ Var Solver::newVar(bool sign, bool dvar)
     if (init_act == 1)
         new_activity = drand(random_seed) * 0.00001;
     else if (init_act == 2)
-        new_activity = 1000 / v;
+        new_activity = 1000 / (v + 1);
     else if (init_act == 3)
         new_activity = v;
     activity_VSIDS.push(new_activity);

minisat/simp/Main.cc

@@ -134,6 +134,11 @@ int main(int argc, char **argv)
         StringOption drup_file("MAIN", "drup-file", "DRUP UNSAT proof ouput file.", "");
         StringOption pcs_file("MAIN", "pcs-file", "Print solver parameter configuration to this file.", "");
 
+        IntOption opt_diversify_rank("MAIN", "diversify-rank", "Select a diversification rank to quickly test another configuration",
+                                     INT32_MAX, IntRange(-1, INT32_MAX));
+        IntOption opt_diversify_size("MAIN", "diversify-size", "Select a diversification size to quickly test another configuration",
+                                     32, IntRange(1, INT32_MAX));
+
         parseOptions(argc, argv, true);
 
         if (!pcs_file.is_empty()) print_pcs_file(pcs_file);
@@ -198,6 +203,12 @@ int main(int argc, char **argv)
             printf("c |                                                                             |\n");
         }
 
+        if (opt_diversify_rank >= 0) {
+            printf("c |  Diversify with rank:  %12d size:  %12d                     |\n",
+                   opt_diversify_rank % opt_diversify_size, (int)opt_diversify_size);
+            S.diversify(opt_diversify_rank % opt_diversify_size, opt_diversify_size);
+        }
+
         parse_DIMACS(in, S);
         fclose(in);
         FILE *res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;

tools/checker/fuzz-check-diversity.sh

@@ -0,0 +1,33 @@
+#!/bin/bash
+#
+# This script runs a set of configurations on a set of randomly generated CNF
+# formulas.
+
+# Formulas to test per iteration
+declare -i FORMULA_PER_CONFIG_RELEASE=1500
+
+# Current directory
+SCRIPT_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+
+cd "$SCRIPT_DIR"
+
+declare -i overall_status=0
+for RANK in {0..32}; do
+    echo ""
+    echo "test rank: $RANK"
+    echo "../../build/release/bin/mergesat -diversify-rank=$RANK \$1" >check-solver-config.sh
+    chmod u+x check-solver-config.sh
+
+    status=0
+
+    # select number of formulas to test based on configuration
+    FORMULA_PER_CONFIG="$FORMULA_PER_CONFIG_RELEASE"
+
+    ./fuzzcheck.sh ./check-solver-config.sh "$FORMULA_PER_CONFIG" || status=$?
+    if [ "$status" -ne 0 ]; then
+        echo "configuration failed!"
+        overall_status=$status
+    fi
+done
+
+exit $overall_status

tools/checker/fuzzcheck.sh

@@ -39,7 +39,7 @@ do
   # control whether algorithm should sleep
   seed=`grep 'c seed' $cnf|head -1|awk '{print $NF}'`
   head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
+  # printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
   i=`expr $i + 1`
   rm -f $sol
 

tools/ci.sh

@@ -10,6 +10,7 @@ TESTFUZZ=${RUNFUZZ:-1}
 TESTSTAREXEC=${RUNSTAREXEC:-1}
 TESTOPENWBO=${RUNOPENWBO:-1}
 TESTPIASIR=${RUNIPASIR:-1}
+TESTDIVERSIFY=${RUNDIVERSIFY:-0}
 
 IPASIR_TIMEOUT=${IPASIR_TIMEOUT:-3600}
 
@@ -26,21 +27,49 @@ CHECKERDIR=$(readlink -e tools/checker)
 
 STATUS=0
 
-if [ $TESTFUZZ -eq 1 ]; then
+test_fuzzing ()
+{
     # Enter checker repository
     pushd tools/checker
 
     # Checkout and build required tools
     ./prepare.sh
 
     # Perform a basic run, and forward its exit code
-    echo "Solve and check 100 formulas with a 5s timeout"
+    echo "Solve and check $FUZZ_ROUNDS formulas with a 5s timeout"
     ./fuzz-drat.sh $FUZZ_ROUNDS 5 || STATUS=$?
 
+    echo "Fuzz diversity rank configurations ..."
+    ./fuzz-check-configurations.sh || STATUS=$?
+
+    popd
+}
+
+if [ $TESTFUZZ -eq 1 ]; then
+    echo "[$SECONDS s] start fuzzing"
+    test_fuzzing
+    echo "[$SECONDS s] end fuzzing"
+fi
+
+test_diversify ()
+{
+    # Enter checker repository
+    pushd tools/checker
+
+    # Checkout and build required tools
+    ./prepare.sh
+
+    # Perform a basic run, and forward its exit code
     echo "Fuzz some pre-defined configurations ..."
     ./fuzz-check-configurations.sh || STATUS=$?
 
     popd
+}
+
+if [ $TESTDIVERSIFY -eq 1 ]; then
+    echo "[$SECONDS s] start diverisfy testing"
+    test_diversify
+    echo "[$SECONDS s] end diverisfy testing"
 fi
 
 # locate release library
@@ -54,7 +83,9 @@ STATIC_LIB=$(readlink -e build/release/lib/libmergesat.a)
 MERGEZIP=$(ls MergeSAT*.zip | sort -V | tail -n 1)
 MERGEZIP=$(readlink -e $MERGEZIP)
 
-if [ $TESTSTAREXEC -eq 1 ]; then
+test_starexec ()
+{
+
     [ $CLEANUP -eq 0 ] || trap 'rm -rf $TMPD' EXIT
     TMPD=$(mktemp -d)
     cp "$MERGEZIP" "$TMPD"
@@ -76,6 +107,12 @@ if [ $TESTSTAREXEC -eq 1 ]; then
     done
     # finish starexec fuzzing
     popd
+}
+
+if [ $TESTSTAREXEC -eq 1 ]; then
+    echo "[$SECONDS s] start starexec testing"
+    test_starexec
+    echo "[$SECONDS s] end startexec testing"
 fi
 
 test_openwbo() {
@@ -119,7 +156,9 @@ test_openwbo() {
 
 # test openwbo with mergesat backend
 if [ $TESTOPENWBO -eq 1 ]; then
+    echo "[$SECONDS s] start openwbo testing"
     test_openwbo
+    echo "[$SECONDS s] end openwbo testing"
 fi
 
 test_ipasir() {
@@ -234,7 +273,9 @@ test_ipasir() {
 
 # test ipasir with mergesat backend
 if [ $TESTPIASIR -eq 1 ]; then
+    echo "[$SECONDS s] start ipasir testing"
     test_ipasir
+    echo "[$SECONDS s] end ipasir testing"
 fi
 
 # Forward exit status from fuzzing

tools/container-default-command.sh

@@ -26,21 +26,6 @@ then
 fi
 
 
-# In case we cannot unzip the file ourselves, try a tool
-if [[ "${INPUT_CNF}" == *".xz" ]];
-then
-    BASE_INPUT=$(basename "$INPUT_CNF" .xz)
-    cp "$INPUT_CNF" /tmp/
-    unxz /tmp/"${BASE_INPUT}.xz"
-    INPUT_CNF=/tmp/"$BASE_INPUT"
-elif [[ "${INPUT_CNF}" == *".bz2" ]];
-then
-    BASE_INPUT=$(basename "$INPUT_CNF" .bz2)
-    cp "$INPUT_CNF" /tmp/
-    bunzip2 /tmp/"${BASE_INPUT}.bz2"
-    INPUT_CNF=/tmp/"$BASE_INPUT"
-fi
-
 # Final check wrt input file
 if [ ! -r "$INPUT_CNF" ]
 then

tools/dockerfile/Dockerfile

@@ -7,41 +7,24 @@ RUN apt-get -y install g++ git
 
 RUN DEBIAN_FRONTEND=noninteractivei apt-get -y install build-essential software-properties-common
 
-# Get the solver, as it has the relevant scripts
-ADD . /opt/mergesat
-
-# Modify docker glibc
-
-# Install modified glibc 2.23
-# Get dependencies
-RUN apt-get -y install fakeroot dpkg-dev \
-    systemtap-sdt-dev \
-    gawk \
-    perl \
-    autoconf \
-    gettext \
-    bison \
-    wget \
-    texi2html \
-    texinfo
+# Enable transparent huge pages, always
+RUN DEBIAN_FRONTEND=noninteractive apt -y install hugepages
+RUN hugeadm --thp-always
 
 # Relevant for interaction with aws
 RUN apt-get install -y unzip
 RUN DEBIAN_FRONTEND=noninteractive apt install -y iproute2 cmake python python-pip gfortran curl
 RUN pip install supervisor awscli
 
-# Get glibc, patch, build, and install (build with default gcc)
-RUN /opt/mergesat/tools/inject-thp-glibc.sh install
-
 # Get a more recent gcc
-#RUN add-apt-repository ppa:ubuntu-toolchain-r/test -y
-#RUN apt-get update -q
-#RUN apt-get remove -y gcc g++
-#RUN DEBIAN_FRONTEND=noninteractive apt-get install g++-9 gcc-9 -y
-#RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 60 --slave /usr/bin/g++ g++ /usr/bin/g++-9
-#RUN update-alternatives --install /usr/bin/gcc-ar gcc-ar /usr/bin/gcc-ar-9 60
-#RUN update-alternatives --install /usr/bin/gcc-ranlib gcc-ranlib /usr/bin/gcc-ranlib-9 60
-#RUN update-alternatives --install /usr/bin/x86_64-linux-gnu-gcc x86_64-linux-gnu-gcc /usr/bin/x86_64-linux-gnu-gcc-9 60 --slave /usr/bin/x86_64-linux-gnu-g++ x86_64-linux-gnu-g++ /usr/bin/x86_64-linux-gnu-g++-9
+RUN add-apt-repository ppa:ubuntu-toolchain-r/test -y
+RUN apt-get update -q
+RUN apt-get remove -y gcc g++
+RUN DEBIAN_FRONTEND=noninteractive apt-get install g++-9 gcc-9 -y
+RUN update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 60 --slave /usr/bin/g++ g++ /usr/bin/g++-9
+RUN update-alternatives --install /usr/bin/gcc-ar gcc-ar /usr/bin/gcc-ar-9 60
+RUN update-alternatives --install /usr/bin/gcc-ranlib gcc-ranlib /usr/bin/gcc-ranlib-9 60
+RUN update-alternatives --install /usr/bin/x86_64-linux-gnu-gcc x86_64-linux-gnu-gcc /usr/bin/x86_64-linux-gnu-gcc-9 60 --slave /usr/bin/x86_64-linux-gnu-g++ x86_64-linux-gnu-g++ /usr/bin/x86_64-linux-gnu-g++-9
 
 # Build the solver
 ADD . /opt/mergesat

tools/make-starexec.sh

@@ -118,6 +118,10 @@ then
 	exit 1
 fi
 
+GIT_DETAILED_VERSION="$(git describe)"
+[ -n "$GIT_DETAILED_VERSION" ] && GIT_DETAILED_VERSION="-${GIT_DETAILED_VERSION}"
+ZIP_NAME="MergeSAT${GIT_DETAILED_VERSION}.zip"
+
 RISSOPT=""
 SPARROWOPT=""
 # do we want to package Riss(for Coprocessor) or Sparrow as well?
@@ -164,8 +168,8 @@ popd
 echo "Note, sub-packages might come with different licenses!" > LICENSE
 
 # compress
-zip -r -y -9 MergeSAT.zip *
+zip -r -y -9 "$ZIP_NAME" *
 
 # jump back and move MergeSAT.zip here
 popd
-mv "$TMPD"/MergeSAT.zip .
+mv "$TMPD"/"$ZIP_NAME" .

tools/starexec_template/bin/starexec_run_default

@@ -13,5 +13,5 @@ then
 	TMPDIR=$(readlink -e "${DEFAULT_MERGESAT_TMPDIR:-}")
 fi
 
-# call the solver without a special configuration, no proof will be generated
+# call the solver without a special configuration, proof will be generated
 "$SOLVERDIR"/mergesat "$1" -verb=0 -drup-file="$TMPDIR"/proof.out

tools/starexec_template/bin/starexec_run_nosimp

@@ -0,0 +1,17 @@
+#!/bin/bash
+#
+# Run mergesat with simplification, and emitting a proof.
+# The proof is written to the file in the directory specified in the second
+# argument, in a file called "proof.out".
+
+# call solver from the directory where this script is located
+SOLVERDIR="$(dirname "${BASH_SOURCE[0]}" )"
+
+TMPDIR=$2
+if [ -n "${DEFAULT_MERGESAT_TMPDIR:-}" ]
+then
+	TMPDIR=$(readlink -e "${DEFAULT_MERGESAT_TMPDIR:-}")
+fi
+
+# disable formula simplification, produce proofs
+"$SOLVERDIR"/mergesat "$1" -no-pre -verb=0 -drup-file="$TMPDIR"/proof.out

tools/starexec_template/bin/starexec_run_unsat

@@ -0,0 +1,17 @@
+#!/bin/bash
+#
+# Run mergesat with simplification, and emitting a proof.
+# The proof is written to the file in the directory specified in the second
+# argument, in a file called "proof.out".
+
+# call solver from the directory where this script is located
+SOLVERDIR="$(dirname "${BASH_SOURCE[0]}" )"
+
+TMPDIR=$2
+if [ -n "${DEFAULT_MERGESAT_TMPDIR:-}" ]
+then
+	TMPDIR=$(readlink -e "${DEFAULT_MERGESAT_TMPDIR:-}")
+fi
+
+# call the solver and disabling SLS and rephasing, no proof will be generated
+"$SOLVERDIR"/mergesat "$1" -verb=0 -no-use-ccnr -no-use-rephasing -drup-file="$TMPDIR"/proof.out