-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
27 changed files
with
924 additions
and
17 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
Choco-solver is a java library for constraint satisfaction problems and constraint optimization problems. | ||
|
||
This experimental version of choco-solver combines SAT with CP to generate lazy clauses. | ||
However, the code has not been stabilised. | ||
|
||
Main authors of this version is Charles Prud’homme (TASC, LS2N UMR 6241). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
Choco-solver is a java library for constraint satisfaction problems and constraint optimization problems. | ||
|
||
The Choco-solver library contains numerous variables, constraints and search procedures, to provide wide modeling perspectives. | ||
Most common variables are integer variables (including binary variables and views) but the distribution also includes set variables, graph variables and real variables. | ||
The constraint library provided by Choco-solver contains many global constraints, which gives a very expressive modeling language. | ||
The search process can also be greatly improved by various built-in search strategies (such as DomWDeg, CHS, ABS, first-fail, etc.) and some optimization procedures (LNS, fast restart, etc.). | ||
Moreover, Choco-solver natively supports explained constraints. | ||
Last, several useful extra features, such as a FlatZinc (the target language of MiniZinc) parser, are provided as well. | ||
|
||
Choco-solver is used by the academy for teaching and research and by the industry to solve real-world problems, such as program verification, smart grid management, timetabling, scheduling and routing. | ||
|
||
Main authors of Choco-solver are Charles Prud’homme (TASC, LS2N UMR 6241), Jean-Guillaume Fages (COSLING S.A.S.), Arthur Godet (Groupe SNCF) and Dimitri Justeau-Allaire (IRD). | ||
|
||
For any informations visit our website : http://choco-solver.org |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,74 @@ | ||
Chuffed - A lazy clause solver | ||
|
||
Geoffrey Chu, Peter J. Stuckey, Andreas Schutt, Thorsten Ehlers, Graeme Gange, Kathryn Francis | ||
|
||
Data61, CSIRO, Australia | ||
|
||
Department of Computing and Information Systems | ||
University of Melbourne, Australia | ||
|
||
|
||
Chuffed is a state of the art lazy clause solver designed from the ground up | ||
with lazy clause generation in mind. Lazy clause generation is a hybrid | ||
approach to constraint solving that combines features of finite domain | ||
propagation and Boolean satisfiability. Finite domain propagation is | ||
instrumented to record the reasons for each propagation step. This creates an | ||
implication graph like that built by a SAT solver, which may be used to create | ||
efficient nogoods that record the reasons for failure. These nogoods can be | ||
propagated efficiently using SAT unit propagation technology. The resulting | ||
hybrid system combines some of the advantages of finite domain constraint | ||
programming (high level model and programmable search) with some of the | ||
advantages of SAT solvers (reduced search by nogood creation, and effective | ||
autonomous search using variable activities). | ||
|
||
The FD components of Chuffed are very tightly integrated with a SAT solver. For | ||
"small" variables (|D| <= 1000), SAT variables representing [x = v] or [x >= v] | ||
are eagerly created at the start of the problem. Channelling constraints are | ||
natively enforced by the variable objects in order to keep the FD solver and | ||
the SAT solver's view of the domains fully consistent at all times. For "large" | ||
variables (|D| > 1000), the SAT variables are lazily generated as needed. Every | ||
propagator in Chuffed has been instrumented so that all propagation can be | ||
explained by some combination of the literals in the SAT solver. An explanation | ||
is of the form a_1 /\ ... /\ a_n -> d, where a_i represent domain restrictions | ||
which are currently true, and d represents the domain change that is implied. | ||
e.g. Suppose z >= x + y, and we have x >= 3, y >= 2. Then the propagator would | ||
propagate x >= 5 with explanation clause x >= 3 /\ y >= 2 -> z >= 5. | ||
|
||
The explanations for each propagation form an implication graph. This allows us | ||
to do three very important things. Firstly, we can derive a nogood to explain | ||
each failure. Such nogoods often allow us to avoid a very large amount of | ||
redundant work, thus producing search trees which are orders of magnitude | ||
smaller. Secondly, nogoods allow us to make informed choices about | ||
non-chronological back-jumping. When no literal from a decision level appears | ||
in the nogood, it is indicative of the fact that the decision made at that | ||
level was completely irrelevant to the search. Thus by back-jumping over such | ||
decisions, we retrospectively avoid making such bad decisions, and hopefully | ||
make good decisions instead which drive the search towards failure. Thirdly, by | ||
analysing the conflict, we can actively gain some information about what good | ||
decision choices are. The Variable State Independent Decaying Sum (VSIDS) | ||
heuristic is an extremely effective search heuristic for SAT problems, and is | ||
also extremely good for a range of CP problems. Each variables has an | ||
associated activity, which is increased whenever the variable is involved in | ||
the conflict. Variables with the highest activity is chosen as the decision | ||
variable at each node. The activities are decayed to reflect the fact that the | ||
set of important variables changes with time. | ||
|
||
Although Chuffed implements lazy clause generation, which is cutting edge and | ||
rather complex, the FD parts of Chuffed are relatively simple. In fact, it is | ||
quite minimalistic. Chuffed only supports 3 different propagator priorities. | ||
Chuffed implements a number of global propagators (alldiff, inverse, | ||
minimum, table, regular, mdd, cumulative, disjunctive, circuit, difference). | ||
It also only supports two kinds of integer variables. Small integer variables | ||
for which the domain is represented by a byte string. | ||
And large integer variables for which the domain is represented only by its | ||
upper and lower bound (no holes allowed). All boolean variables and boolean | ||
constraints are handled by the builtin SAT solver. | ||
|
||
Great pains have been taken to make everything as simple and efficient as | ||
possible. The solver, when run with lazy clause generation disabled, is | ||
somewhat comparable in speed with older versions of Gecode. The overhead from | ||
lazy clause generation ranges from negligible to perhaps around 100%. The | ||
search reduction, however, can reach orders of magnitude on appropriate | ||
problems. Thus lazy clause generation is an extremely important and useful | ||
technology. The theory behind lazy clause generation is described in much | ||
greater detail in various papers. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
CpoFzn is a CP Optimizer solver interface for MiniZinc. | ||
|
||
See https://github.com/IBMDecisionOptimization/cpofzn for more information. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
The Gecode entry to the MiniZinc challenge 2024 | ||
|
||
This solver is based on the Gecode C++ constraint solving library | ||
(upcoming version 6.0.0 + some modifications), and the Gecode/FlatZinc | ||
interface. Both Gecode and Gecode/FlatZinc are available under the MIT | ||
license from the web site http://www.gecode.org. | ||
|
||
The par version of this entry uses a mix of search strategies: | ||
- the strategy specified in the model | ||
- a dynamic strategy (based on AFC, aka dom_w_deg) with restarts | ||
- an LNS strategy to generate solutions quickly (only for optimisation problems) | ||
|
||
Main authors: | ||
Christian Schulte, | ||
ICT, KTH - Royal Institute of Technology, Sweden | ||
Mikael Lagerkvist, | ||
ICT, KTH - Royal Institute of Technology, Sweden | ||
Guido Tack, | ||
Department of Computer Science at K.U. Leuven, Belgium | ||
|
||
A full list of authors as well as licensing information is available from | ||
http://www.gecode.org/gecode-doc-latest/PageLic.html. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
Gecode/Dexter | ||
|
||
Gecode Authors: Christian Schulte, Guido Tack, and Mikael Z. Lagerkvist. | ||
Gecode/Dexter Authors: Dexter Leander. | ||
|
||
Gecode/Dexter uses a portfolio search built into the classical constraint programming solver Gecode for MiniZinc, to solve optimisation problems. When solving satisfaction problems or when the solver is run with one thread, regular Gecode is used. As such, this solver is a variant of the Gecode solver. | ||
|
||
The portfolio supports up to eleven assets and was implemented as part of a master thesis. Six of these assets utilise LNS to navigate the search space, and they include: random, propagation-guided, reverse propagation-guided, objective relaxation, cost impact-guided, and static variable-relationship-guided LNS. Moreover, one asset compares all LNS assets and selects the one most fit for the problem at hand. Additionally, two assets are modifications of standard Gecode search, and one is identical. The portfolio also includes a shaving asset that helps find infeasible values for variables during the search. | ||
|
||
A more in-depth description of the assets of the portfolio and the portfolio itself can be found in the thesis at: https://www.diva-portal.org/smash/record.jsf?pid=diva2%3A1876143&dswid=-6428 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,36 @@ | ||
============================================================ | ||
iZplus (fzn_izplus) -- iZ based solver for MiniZinc Challenge | ||
Copyright (C) 2012-2024 NTT DATA SEKISUI SYSTEMS CORPORATION. | ||
============================================================ | ||
|
||
* What is iZplus | ||
|
||
iZplus is a FlatZinc solver using iZ-C constraint programming | ||
library which is developed by NTT DATA SEKISUI SYSTEMS CORPORATION. | ||
|
||
iZ-C provides : | ||
* many built-in constraints | ||
* constraint propagation mechanism | ||
* simple search strategy | ||
|
||
And in iZplus, following algorithms are 'plus'ed. | ||
* Randomized restarting in search | ||
* Local search for optimization problem | ||
* Local search for satisfying problem | ||
* Variable reordering | ||
* NG learning | ||
|
||
* Author | ||
|
||
Toshimitsu FUJIWARA <[email protected]> | ||
developer at NTT DATA SEKISUI SYSTEMS CORPORATION | ||
|
||
* Acknowledgement | ||
|
||
FlatZinc parser in fzn_izplus is based on 'FlatZinc parser skeleton' | ||
written by Guido Tack. | ||
|
||
iZ-C is a constraint programming library developed by | ||
NTT DATA SEKISUI SYSTEMS CORPORATION. | ||
|
||
http://www.constraint.org/en/izc_download.html |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
JaCoP - Java Constraint Programming Solver | ||
|
||
JaCoP solver is Java-based open source solver developed and maintained mainly by two people Krzysztof Kuchcinski - Dept. of Computer Science, Lund University, Sweden, and Radoslaw Szymanek - Utopix, Switzerland. | ||
|
||
Moreover a number of students have contributed to the solver by programming first versions of different global constraints and set constraints. The solver is being used in academia for research and teaching as well as in industry for commercial purposes. The most successful use of the solver is within Electronic Design Automation community, since both main authors come from that community. | ||
|
||
JaCoP supports finite domains of integers and sets of integers as well as floating-point domain. It offers a significant number of primitive and global constraints on these variables to facilitate modeling as well as modular design of search. This allows to tailor search to characteristics of the problem being addressed. It has currently more than 100,000 lines of code, not including examples and testing code. The examples which are the preferred way to document the abilities of JaCoP have more than 20.000 lines of code. The core developers have been working on JaCoP for past 10 years during their free time as a hobby activity. It has been refactored, transformed, and improved many times. Initial versions of JaCoP were even 3 orders of magnitude slower than the current version. JaCoP implementation has been influenced heavily by more than 20 research articles. Moreover, JaCoP was used as a tool to conduct experiments for CP publications. | ||
|
||
The major focus of JaCoP are its constraints. These constraints include rich set of primitive, logical, and conditional constraints as well as many global constraints. The most important global constraints are as follows. | ||
|
||
- diff2, | ||
- cumulative, | ||
- alldifferent (with bounds consistency and complete algorithm based | ||
on Régin's algorithm), | ||
- gcc, | ||
- extensional support (with three different state-of-the-art approaches) | ||
and extensional conflict, | ||
- among, | ||
- element, | ||
- circuit and subcircuit, | ||
- knapsack, | ||
- binpacking, | ||
- regular, | ||
- netflow, and | ||
- geost. | ||
|
||
|
||
JaCoP solver can be used directly from Java but it has several front-ends. It has FlatZinc language interface that makes it possible to execute MiniZinc models. It allows us to perform extensive testing with the help of other solvers as we can compare results from different solvers. It has also Scala based domain-specific language so it is easier to create your own constraint programs even in more intuitive manner. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
MiniZinc 2.8 MILP interface for OSICBC 2.10 | ||
MiniZinc Release 2.8.5 | ||
http://www.minizinc.org/software.html | ||
|
||
Gleb Belov, Peter J. Stuckey, Guido Tack, Mark Wallace. Improved Linearization of Constraint Programming Models. In M. Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. LNCS 9892, pp. 49-65, Springer, 2016. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
MiniZinc 2.8 MILP interface for IBM ILOG CPLEX 22.11 | ||
MiniZinc Release 2.8.5 | ||
http://www.minizinc.org/software.html | ||
|
||
Gleb Belov, Peter J. Stuckey, Guido Tack, Mark Wallace. Improved Linearization of Constraint Programming Models. In M. Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. LNCS 9892, pp. 49-65, Springer, 2016. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
MiniZinc 2.8 MILP interface for Gurobi 11.0.3 | ||
MiniZinc Release 2.8.5 | ||
http://www.minizinc.org/software.html | ||
|
||
Gleb Belov, Peter J. Stuckey, Guido Tack, Mark Wallace. Improved Linearization of Constraint Programming Models. In M. Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. LNCS 9892, pp. 49-65, Springer, 2016. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
MiniZinc 2.8 MILP interface for HiGHS 1.7.2 | ||
MiniZinc Release 2.8.5 | ||
http://www.minizinc.org/software.html | ||
|
||
Gleb Belov, Peter J. Stuckey, Guido Tack, Mark Wallace. Improved Linearization of Constraint Programming Models. In M. Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. LNCS 9892, pp. 49-65, Springer, 2016. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,5 @@ | ||
MiniZinc 2.8 MILP interface for SCIP 9.1.0 | ||
MiniZinc Release 2.8.5 | ||
http://www.minizinc.org/software.html | ||
|
||
Gleb Belov, Peter J. Stuckey, Guido Tack, Mark Wallace. Improved Linearization of Constraint Programming Models. In M. Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings. LNCS 9892, pp. 49-65, Springer, 2016. |
Oops, something went wrong.