diff --git a/README.md b/README.md index eecf1c9..c07ade7 100644 --- a/README.md +++ b/README.md @@ -102,7 +102,7 @@ For the Debian-based Linux operating systems, following the below instructions y - Install prerequisites: ```sh - apt-get install python3-dev + apt-get install python3-dev python3-full curl python3 -m pip install cython ``` @@ -136,25 +136,15 @@ For the Debian-based Linux operating systems, following the below instructions y ```sh mkdir /home/tools/ && cd /home/tools/ - wget https://github.com/MiniZinc/MiniZincIDE/releases/download/2.7.4/MiniZincIDE-2.7.4-bundle-linux-x86_64.tgz + LATEST_MINIZINC_VERSION=$(curl -s https://api.github.com/repos/MiniZinc/MiniZincIDE/releases/latest | grep -oP '"tag_name": "\K(.*)(?=")') + wget "https://github.com/MiniZinc/MiniZincIDE/releases/download/$LATEST_MINIZINC_VERSION/MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" mkdir MiniZinc - tar zxvf MiniZincIDE-2.7.4-bundle-linux-x86_64.tgz -C MiniZinc --strip-components=1 - rm MiniZincIDE-2.5.5-bundle-linux-x86_64.tgz + tar -xvzf "MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" -C MiniZinc --strip-components=1 \ + rm "MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" ln -s /home/tools/MiniZinc/bin/minizinc /usr/local/bin/minizinc python3 -m pip install minizinc ``` -- Install Or-Tools - - ```sh - mkdir /home/tools/ && cd /home/tools/ - wget https://github.com/google/or-tools/releases/download/v9.0/or-tools_flatzinc_debian-10_v9.0.9048.tar.gz - mkdir or-tools - tar xvzf or-tools_flatzinc_debian-10_v9.0.9048.tar.gz -C or-tools --strip-components=1 - rm or-tools_flatzinc_debian-10_v8.2.8710.tar.gz - cp /home/tools/autoguess/configfiles/ortools.msc /home/tools/MiniZinc/share/minizinc/solvers - ``` - - Install [SageMath](https://doc.sagemath.org/html/en/installation/binary.html#linux) ```sh diff --git a/autoguess.py b/autoguess.py index d39990d..9a4d223 100644 --- a/autoguess.py +++ b/autoguess.py @@ -7,6 +7,28 @@ @contact: hsn.hadipour@gmail.com For more information, feedback or any questions, please contact hsn.hadipour@gmail.com + +MIT License + +Copyright (c) 2021 Hosein Hadipour + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. ''' from core import search @@ -194,9 +216,6 @@ def main(): help="By setting this parameter to 1, the intermediate generated files such as CP/MILP/SAT models as well as\n" "some intermediate results are stored inside the temp folder\n") - - - # Parse command line arguments and construct parameter list. args = parser.parse_args() params = loadparameters(args) diff --git a/core/gdcp.py b/core/gdcp.py index c14d12d..0893d47 100644 --- a/core/gdcp.py +++ b/core/gdcp.py @@ -17,6 +17,18 @@ # logging.basicConfig(filename="./temp/minizinc-python.log", level=logging.DEBUG) +# Check if "OR Tools" appears in the output of "minizinc --solvers" command +import subprocess +try: + output = subprocess.run(['minizinc', '--solvers'], stdout=subprocess.PIPE, stderr=subprocess.PIPE) + if "com.google.ortools.sat" in output.stdout.decode("utf-8"): + ortools_available = True + print("OR Tools is available") + else: + ortools_available = False + print("OR Tools is not available") +except FileNotFoundError: + ortools_available = False class ReduceGDtoCP: """ @@ -65,9 +77,12 @@ def __init__(self, inputfile_name=None, outputfile_name='output', max_guess=0, m # yuck self.supported_cp_solvers = [ 'gecode', 'chuffed', 'cbc', 'gurobi', 'picat', 'scip', 'choco', 'or-tools'] - self.cp_optimization = cp_optimization - assert(self.cp_solver_name in self.supported_cp_solvers) + assert(self.cp_solver_name in self.supported_cp_solvers) + if ortools_available: + if self.cp_solver_name == "ortools": + self.cp_solver_name = "com.google.ortools.sat" self.cp_solver = minizinc.Solver.lookup(self.cp_solver_name) + self.cp_optimization = cp_optimization self.nthreads = 16 self.cp_boolean_variables = [] self.cp_constraints = '' diff --git a/docker/Dockerfile b/docker/Dockerfile index 57ba7da..dbd4f70 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -4,59 +4,66 @@ FROM debian:latest ARG DEBIAN_FRONTEND=noninteractive # Install some basic packages -RUN apt-get update && apt-get install -y build-essential git cmake wget curl python3 python3-pip python3-dev +RUN apt-get update && apt-get install -y build-essential git cmake wget curl python3 python3-pip python3-dev python3-full + +# Install the latest version of MiniZinc +WORKDIR /home/tools/ +RUN LATEST_MINIZINC_VERSION=$(curl -s https://api.github.com/repos/MiniZinc/MiniZincIDE/releases/latest | grep -oP '"tag_name": "\K(.*)(?=")') \ + && wget "https://github.com/MiniZinc/MiniZincIDE/releases/download/$LATEST_MINIZINC_VERSION/MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" \ + && mkdir MiniZinc \ + && tar -xvzf "MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" -C MiniZinc --strip-components=1 \ + && rm "MiniZincIDE-$LATEST_MINIZINC_VERSION-bundle-linux-x86_64.tgz" +RUN ln -s /home/tools/MiniZinc/bin/minizinc /usr/local/bin/minizinc + +# Clone Autoguess +RUN git clone https://github.com/hadipourh/autoguess +WORKDIR /home/tools/autoguess + +# # Install Or-Tools and link it to MiniZinc (This is not necessary for versions of MiniZinc >= 2.8.1) +# WORKDIR /home/tools/ +# RUN wget https://github.com/google/or-tools/releases/download/v9.2/or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz && \ +# mkdir or-tools && \ +# tar xvzf or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz -C or-tools --strip-components=1 && \ +# rm or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz && \ +# cp configfiles/ortools.msc /home/tools/MiniZinc/share/minizinc/solvers + +# Install SageMath +RUN apt-get install -y sagemath + +# Install Graphviz +RUN apt-get install -y graphviz + +# Create and activate a virtual environment +RUN python3 -m venv venv # Install python-sat -RUN python3 -m pip install python-sat[pblib,aiger] +RUN venv/bin/python3 -m pip install python-sat[pblib,aiger] # Install pysmt -RUN python3 -m pip install pysmt +RUN venv/bin/python3 -m pip install pysmt # Install smt solvers supported by pysmt -RUN python3 -m pip install cython -RUN yes | python3 -m pysmt install --btor -RUN yes | python3 -m pysmt install --z3 +RUN venv/bin/python3 -m pip install cython +RUN yes | venv/bin/python3 -m pysmt install --btor +RUN yes | venv/bin/python3 -m pysmt install --z3 # Install Z3 solver -RUN python3 -m pip install z3-solver - -# Install MiniZinc -WORKDIR /home/tools/ -RUN wget https://github.com/MiniZinc/MiniZincIDE/releases/download/2.6.3/MiniZincIDE-2.6.3-bundle-linux-x86_64.tgz && \ - mkdir MiniZinc && \ - tar zxvf MiniZincIDE-2.6.3-bundle-linux-x86_64.tgz -C MiniZinc --strip-components=1 && \ - rm MiniZincIDE-2.6.3-bundle-linux-x86_64.tgz -RUN ln -s /home/tools/MiniZinc/bin/minizinc /usr/local/bin/minizinc +RUN venv/bin/python3 -m pip install z3-solver # Install Python interface of MiniZinc -RUN python3 -m pip install minizinc - -# Install Or-Tools -WORKDIR /home/tools/ -RUN wget https://github.com/google/or-tools/releases/download/v9.2/or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz && \ - mkdir or-tools && \ - tar xvzf or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz -C or-tools --strip-components=1 && \ - rm or-tools_amd64_flatzinc_debian-11_v9.2.9972.tar.gz +RUN venv/bin/python3 -m pip install minizinc # Install Gurobi (Restricted license - for non-production use only) -RUN python3 -m pip install gurobipy - -# Install SageMath -RUN apt-get install -y sagemath - -# Install Graphviz -RUN apt-get install -y graphviz +RUN venv/bin/python3 -m pip install gurobipy # Install Python interface of Graphviz -RUN python3 -m pip install graphviz +RUN venv/bin/python3 -m pip install graphviz # Install dot2tex -RUN python3 -m pip install dot2tex +RUN venv/bin/python3 -m pip install dot2tex -# Clone Autoguess and introduce Or-Tools to MiniZinc -RUN git clone https://github.com/hadipourh/autoguess -WORKDIR /home/tools/autoguess -RUN cp configfiles/ortools.msc /home/tools/MiniZinc/share/minizinc/solvers - -# Clean +# Clean up RUN apt-get clean && rm -rf /var/lib/apt/lists/* + +# Set the default command to run when a container starts +CMD cd /home/tools/autoguess && . venv/bin/activate && /bin/bash \ No newline at end of file diff --git a/docker/MiniZincIDE-2.8.5-bundle-linux-x86_64.tgz b/docker/MiniZincIDE-2.8.5-bundle-linux-x86_64.tgz new file mode 100644 index 0000000..7b9682e Binary files /dev/null and b/docker/MiniZincIDE-2.8.5-bundle-linux-x86_64.tgz differ