diff --git a/CHANGELOG b/CHANGELOG index cb3c120f..a37e2cde 100644 --- a/CHANGELOG +++ b/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 diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 185ac349..63ec00d8 100644 --- a/minisat/core/Solver.cc +++ b/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) { diff --git a/tools/aws_docker/README.md b/tools/aws_docker/README.md index b517f4e8..65095936 100644 --- a/tools/aws_docker/README.md +++ b/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 \ No newline at end of file diff --git a/tools/aws_docker/build_images.sh b/tools/aws_docker/build_images.sh index 6ff5a5ef..b47f2cc1 100755 --- a/tools/aws_docker/build_images.sh +++ b/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,10 +18,12 @@ 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 @@ -26,21 +31,37 @@ build_competition_base_images() ( 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 diff --git a/tools/aws_docker/leader/Dockerfile b/tools/aws_docker/leader/Dockerfile index 0f52636b..c3f367d6 100644 --- a/tools/aws_docker/leader/Dockerfile +++ b/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,7 +17,8 @@ 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 @@ -19,6 +26,10 @@ 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 diff --git a/tools/dockerfile/Dockerfile b/tools/dockerfile/Dockerfile index 6c389cf4..4ae12c31 100644 --- a/tools/dockerfile/Dockerfile +++ b/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