Docker solvers

CHANGELOG

@@ -5,7 +5,11 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
-## [unreleased]
+## [4.0]
+
+ * improve AWS docker setup
+
+## [4.0-rc4]
 
  * add AWS docker infrastructure
  * add gate detection for portfolio configurations

minisat/core/Solver.cc

@@ -94,7 +94,7 @@ static IntOption opt_ccmin_mode(_cat,
                                 IntRange(0, 3));
 static IntOption
 opt_phase_saving(_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
-static IntOption opt_init_act(_cat, "rnd-init", "Initial activity is 0:0, 1:random, 2:1000/v, 3:v", 0, IntRange(0, 3));
+static IntOption opt_init_act(_cat, "rnd-init", "Initial activity is 0:0, 1:random, 2:1000/v, 3:v", 2, IntRange(0, 3));
 static IntOption opt_init_act_init(_cat, "rnd-init-init", "Initial activity for rnd-init=2", 1000, IntRange(1, INT32_MAX));
 static IntOption opt_restart_first(_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX));
 static IntOption opt_restart_strategy(_cat, "restart", "How to schedule restarts (split,luby,dynamic)", 1, IntRange(1, 3));
@@ -235,7 +235,7 @@ opt_na_maxCls(_cat, "na-max-cls", "Test at most X binary clauses for necessary a
 static IntOption opt_na_attemptEvery(_cat,
                                      "na-attempt-every",
                                      "Attempt necessary assignment every X-th level 1 decision (0 == off)",
-                                     0,
+                                     4,
                                      IntRange(0, INT32_MAX));
 static IntOption opt_na_recheckInc(_cat,
                                    "na-recheck-every",
@@ -3567,13 +3567,17 @@ void Solver::diversify(int rank, int size)
     /* use previous release configurations as first configs */
     if (rank == 1) {
         /* initialize activity as in v3 */
-        init_act = 2;
+        init_act = 0;
+        /* do not use necessary assignment */
+        nAssignment.setAttemptEvery(0);
     }
     if (rank == 2) {
         /* do not use SLS, and initialize activities as in v3 */
         init_act = 0;
         use_ccnr = false;
         state_change_time = 1000000000;
+        /* do not use necessary assignment */
+        nAssignment.setAttemptEvery(0);
     }
     if (rank < 3) return;
 
@@ -3582,7 +3586,7 @@ void Solver::diversify(int rank, int size)
     if (rank % 5 == 2) restart = Restart(0);
     if (rank % 5 == 3) restart = Restart(1);
     if (rank % 7 == 3) core_lbd_cut = 4;
-    if (rank % 7 == 6) nAssignment.setAttemptEvery(4);
+    if (rank % 7 == 6) nAssignment.setAttemptEvery(0);
     if (rank % 11 == 4) init_act = 0;
     if (rank % 11 == 7) init_act = 3;
     if (rank % 13 == 8) {

tools/aws_docker/README.md

@@ -31,3 +31,17 @@ as well as solving an example formula with the solver.
 
     ./build_images.sh
     ./run_parallel.sh satcomp-mergesat example_cnfs/rook-8-0-0.cnf 
+
+## Building a Separate Solver
+
+In case you want to build a different solver than the default, then you can
+specify the image name to be built. This name then has to be the first
+parameter of the ./build_images.sh script. This feature is especially useful
+when multiple solvers should be build from the code base.
+
+    ./build_images.sh mergesat-pcasso
+
+Next, you can use this docker image name to solve formulas again, e.g.
+via the command below:
+
+    ./run_parallel.sh mergesat-pcasso example_cnfs/rook-8-0-0.cnf

tools/aws_docker/build_images.sh

@@ -1,7 +1,10 @@
 #!/usr/bin/env bash
 
-declare -r COMMON_TAG="satcomp-mergesat:common"
-declare -r LEADER_TAG="satcomp-mergesat:leader"
+SOLVER_NAME=${1:-satcomp-mergesat}
+echo "Building MergeSat docker images with tag base: '$SOLVER_NAME' ..."
+
+declare -r COMMON_TAG="$SOLVER_NAME:common"
+declare -r LEADER_TAG="$SOLVER_NAME:leader"
 
 build_competition_base_images() (
     if docker image ls satcomp-infrastructure:leader | grep "satcomp-infrastructure" &&
@@ -15,32 +18,50 @@ build_competition_base_images() (
     TMP_DOCKER_DIR$(mktemp -d)
     pushd "$TMP_DOCKER_DIR"
     # operate in temporary directory
+    echo "Cloning https://github.com/aws-samples/aws-batch-comp-infrastructure-sample.git ..."
     git clone https://github.com/aws-samples/aws-batch-comp-infrastructure-sample.git
     cd aws-batch-comp-infrastructure-sample/
     cd docker/
     cd satcomp-images/
+    echo "Building SAT comp images ..."
     ./build_satcomp_images.sh
     docker images ls
     popd
 )
 
 if ! docker info &>/dev/null; then
     echo "ERROR Failed to access docker"
+    exit 1
 fi
 
 build_competition_base_images
 
-pushd common
-if ! docker build -t "$COMMON_TAG" . | grep "Successfully tagged $COMMON_TAG"; then
-    docker build -t "$COMMON_TAG" .
-    echo "ERROR Failed to build common docker image."
-    exit 1
-fi
-popd
+# Build common image, which holds the SAT solver binary
+build_common_image ()
+{
+    echo "Building solver common image from MergeSat's default Dockerfile ..."
+    local git_root=$(git rev-parse --show-toplevel)
+
+    if [ ! -d "$git_root" ]; then
+        echo "Failed to detect git repository root directory ('$git_root') of MergeSat, aborting"
+        exit 1
+    fi
+
+    pushd "$git_root"
+    echo "Building common image for tag '$COMMON_TAG' ..."
+    if ! docker build -t "$COMMON_TAG" . | grep "Successfully tagged $COMMON_TAG"; then
+        docker build -t "$COMMON_TAG" .
+        echo "ERROR Failed to build common docker image."
+        return 1
+    fi
+    popd
+}
+build_common_image || exit 1
 
 pushd leader
-if ! docker build -t "$LEADER_TAG" . | grep "Successfully tagged $LEADER_TAG"; then
-    docker build -t "$LEADER_TAG" .
+echo "Building leader image for tag '$LEADER_TAG', using MergeSat common image with tag '$COMMON_TAG'"
+if ! docker build --build-arg MERGESAT_DOCKERFILE_SRC=$COMMON_TAG -t "$LEADER_TAG" . | grep "Successfully tagged $LEADER_TAG"; then
+    docker build --build-arg MERGESAT_DOCKERFILE_SRC=$COMMON_TAG -t "$LEADER_TAG" .
     echo "ERROR Failed to build leader docker image."
     exit 1
 fi

tools/aws_docker/leader/Dockerfile

@@ -1,5 +1,11 @@
 ################### Use MergeSat
-FROM satcomp-mergesat:common AS builder
+
+# Allow to alter the MergeSat image that is used here. This allow to build
+# multiple solvers from the same Dockerfile infrastructure.
+#
+#
+ARG MERGESAT_DOCKERFILE_SRC=satcomp-mergesat:common
+FROM $MERGESAT_DOCKERFILE_SRC AS builder
 USER root
 
 
@@ -11,14 +17,19 @@ WORKDIR /
 RUN ls /competition
 
 # Copy solver binary and solver scripts
-COPY --from=builder --chown=ecs-user /mergesat/build/release/bin/mergesat /competition/mergesat
+# Staitcally linked binary from MergeSat's default docker container
+COPY --from=builder --chown=ecs-user /opt/mergesat/build/release/bin/mergesat /competition/mergesat
 COPY --chown=ecs-user ./init_solver.sh /competition
 COPY --chown=ecs-user ./run_solver.sh /competition
 COPY --chown=ecs-user ./solver /competition
 
 # Show all files we copied
 RUN ls /competition
 
+
+# Enable using transparent huge pages via glibc tunables, since 2.35
+ENV GLIBC_TUNABLES=glibc.malloc.hugetlb=1
+
 USER ecs-user
 RUN chmod +x /competition/mergesat
 RUN chmod +x /competition/init_solver.sh

tools/dockerfile/Dockerfile

@@ -11,7 +11,10 @@ RUN yum -y install openssh-server openmpi-devel python3-pip
 RUN pip3 install awscli boto3 flask pytz polling2 supervisor waitress
 
 # Import and build the solver
-ADD . /opt/mergesat
+RUN mkdir -p /opt/mergesat
+ADD minisat /opt/mergesat/minisat
+ADD Makefile /opt/mergesat/Makefile
+ADD LICENSE /opt/mergesat/LICENSE
 
 # Clean solver
 RUN cd /opt/mergesat && make clean