MiniZinc 2017 Competition Solver Description Solver: LCG-glucose-4.1 (the version tracks the Glucose version) Author: Nick Downing, The University of Melbourne, Data61 CSIRO Efficient Lazy Clause Generation solver based on a modified glucose-syrup-4.1 backend, the backend is modified quite heavily, although in principle most of the modifications are inserting hooks to interleave Lazy Clause Generation code (finite domain propagation, Boolean models of integer variables, and the lazy explanation system) into the SAT solving algorithm at appropriate points. As stated last year, key points are propagation speed and minimal propagators. The starting point for the solver is a refactored version of the MiniZinc 2016 Competition entry, although the refactored version would execute more-or-less the same as in 2016. The most significant tidy-ups and refactorings include: - Implementing callbacks between layers. There are several layers between the MiniZinc layer and the Glucose layer, each presents an interface representing the current problem (variable and constraint database, variable values etc) to the layer above. Each layer can receive callbacks during solving, during which it can interrogate the problem via the interface provided by the layer below, create new variables, post new constraints etc, and/or reflect the callback to the layer above with some transformation. We imagine CPLEX probably uses a similar scheme internally, to hide the effects of presolving from the CPLEX callable library client. Our callbacks interface is somewhat similar to CPLEX. - Removing the ability to generate CNF/WCNF/OPB/LP versions of the MiniZinc- format input. The solver can still generate and solve the decomposed versions internally. In future, this ability will be provided in a more elegant way, by moving the CNF/WCNF/OPB/LP decompositions from the LCG-glucose backend into the problem transformation layer, and then providing alternative backends that can output CNF/WCNF/OPB/LP, solve via an external solver that can provide competition-format solutions, and then output the solutions in MiniZinc style. - Reinstating the "shim" which allows to link with Chuffed propagators, since we have a reasonably large library of explanation-capable propagators in Chuffed. For the time being, only the Chuffed regular propagator (via MDDs, by Gange et al.) and the Chuffed cumulative propagator (by Schutt et al.) are in, since the problem transformation layer also needs to know the signatures of the propagators, which is a bit time-consuming to implement (in future these signatures can be generated automatically from MiniZinc predicate definitons). - The FlatZinc solver (fzn-lcg_glucose; formerly fzn-glucose) links against a systemwide (or home directory) installation of libminizinc 2.1.5 for parsing the FlatZinc input, rather than having an older (and modified) version baked in. Also, share/minizinc/lcg_glucose/builtins.mzn is generated automatically by the build system by patching share/minizinc/std/builtins.mzn, not manually. In future we plan to make e.g. Debian packages, using *.so libraries for both libminizinc and liblcg_glucose, for the command-line solvers to link against. For the competition however, we use statically linked executables for safety. - Linking in Glucose's (actually MiniSAT's) built-in simplifying preprocessor, i.e. the subsumption checks and Boolean variable elimination. We do not think this will yield much useful benefit, except if the problem is a SAT instance encoded into MiniZinc, so this feature is off by default. Enable with "-pre". After the refactorings, we then made the following functional improvements: - Implementing a MiniZinc solver (mzn-lcg_glucose; accepts the same command syntax as libminizinc-provided MiniZinc solvers like mzn-gecode or mzn-cplex), this is supposed to save some fractions of seconds spent transferring the FlatZinc model to the solver by disk and the solutions back to MiniZinc by pipe. We use libminizinc's in-memory format exclusively (for both model and solutions). It is also more convenient, as mzn2fzn/solns2out are not needed. - Changing the Glucose backend from glucose-3.0 (erroneously I had said 3.01 in the previous document) to glucose-syrup-4.1, i.e. Glucose parallel version. - Implementing a multi-threaded version of the problem transformation layer. This is quite basic at present, it can post new constraints during solving in any thread during a callback from that thread (but only clausal and linear constraints, which is a restriction of the underlying solver), but it can only create new variables during solving in thread 0. Also, only one thread can be executing in the problem transformation layer at a time (because it uses, for example, std::vector to maintain a list of variables, which is not thread safe). Hence, there will be some slight synchronization overhead if multiple threads issue callbacks (for example, they all find solutions) simultaneously. - Implementing a multi-threaded version of the Chuffed propagators "shim", and memory checks. Chuffed uses global variables, which we now define as __thread. - Adding the ability to post clauses and linear constraints during solving, without having to backtrack to the start (partially reusing the framework we had for defining the integer variable model during solving), and making "all solutions" (satisfaction) and branch-and-bound (optimization) modes use this feature. We implemented this as a way to allow sharing of solution information between threads as solutions are discovered, without needlessly disrupting the other threads. However, it is also a big win for the single-threaded solver. NOTE: For now, "all solutions" mode correctly posts the blocking clause in the particular thread without restarting, but does not yet post to other threads, therefore repeated solutions are possible (this mode not used in competition). - Implementing semantic literal sharing in glucose-syrup, so that if different threads created different lazy literals for the integer variable model, then these literals will be translated across threads. We also made glucose-syrup's clause-sharing scheme share clauses more frequently, it used to wait until the next restart happened to occur, which could be a long time, given Glucose uses adaptive restarts. It now shares them instantly, without having to backtrack. - Adding "int_pow(var int: x, var int: y, var_int: z) === x ^ y = z", noting that it won't post unless x >= 0, y >= 1, z >= 0. It is implemented in almost the same way as the "int_times" propagator, that is, it becomes "x ^ y >= z" and "x ^ y <= z", with only the necessary halves being emitted, depending on how z appears elsewhere in the model. Requiring y >= 1 makes each variable monotonic with respect to the other two, similarly to how we require all >= 0 in the "times" propagator. The long term goal is to provide a higher level decomposition in the problem transformation layer, so that it will handle the zero/negative cases with a separate propagator (or clausal decomposition etc). - Implementing a "portfolio lite" scheme and better memory management for the parallel solver. If memory runs low during parsing/problem construction, it will reduce the number of threads to use. Then, if the problem is optimization then the first available thread runs the OLL unsatisfiable-core algorithm. If there is a MiniZinc search specification and there are at least two threads remaining, the next available thread runs the MiniZinc search specification. All threads except the unsatisfiable-core thread, if any, run branch-and-bound for optimization problems. All threads except the MiniZinc search thread, if any, run Glucose's activity-based search (VSIDS) and adaptive restarts scheme.