-
Notifications
You must be signed in to change notification settings - Fork 1
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
0 parents
commit a2938d7
Showing
48 changed files
with
10,342 additions
and
0 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,30 @@ | ||
| Version 4.1 | ||
| - Adaptative (activated by default) strategies. See SAT 2016 paper. | ||
|
|
||
| Version 4.0 | ||
| - Add a Multithread version, called syrup (many glucose ;-) | ||
| See SAT14 paper: Lazy Clause Exchange Policy for parallel SAT solvers. | ||
|
|
||
| - Can work indepentently in sequential or with many cores | ||
|
|
||
| Version 3.0 (2013) | ||
| - Add incremental features. | ||
| See SAT13 paper: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction | ||
|
|
||
| - Add certified UNSAT proof. | ||
|
|
||
| Version 2.3 (2012) | ||
| - Add new restart strategy | ||
| See CP12 paper: Refining Restarts Strategies For SAT and UNSAT | ||
|
|
||
| - Add additionnal features to speed the search | ||
|
|
||
| Version 2.0 (2011) | ||
| - Add additionnal features (freeze potential good clauses for one turn) | ||
|
|
||
| - Based on Minisat 2.2 | ||
|
|
||
| Version 1.0 (2009) | ||
| - Based on Minisat 2.0 | ||
| First release of glucose. | ||
| See ijcai 2009 paper: Predicting Learnt Clauses Quality in Modern SAT Solver |
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,47 @@ | ||
| Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon | ||
| CRIL - Univ. Artois, France | ||
| LRI - Univ. Paris Sud, France (2009-2013) | ||
| Labri - Univ. Bordeaux, France | ||
|
|
||
| Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon | ||
| CRIL - Univ. Artois, France | ||
| Labri - Univ. Bordeaux, France | ||
|
|
||
| Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of | ||
| Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it | ||
| is based on. (see below). | ||
|
|
||
| Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel | ||
| version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software | ||
| without restriction, including the rights to use, copy, modify, merge, publish, distribute, | ||
| sublicence, 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 and below copyrights notices and this permission notice shall be included in all | ||
| copies or substantial portions of the Software; | ||
| - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot | ||
| be used in any competitive event (sat competitions/evaluations) without the express permission of | ||
| the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event | ||
| using Glucose Parallel as an embedded SAT engine (single core or not). | ||
|
|
||
|
|
||
| --------------- Original Minisat Copyrights | ||
|
|
||
| Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson | ||
| Copyright (c) 2007-2010, Niklas Sorensson | ||
|
|
||
| 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. | ||
|
|
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,221 @@ | ||
| # Windows builds for The Glucose SAT Solver | ||
| Glucose is based on a new scoring scheme for the clause learning mechanism of so called "Modern" SAT solvers (it is based on [this paper](https://www.ijcai.org/Proceedings/09/Papers/074.pdf)). | ||
|
|
||
| Glucose is designed to be parallel since 2014. The name of the Solver is a contraction of the concept of "glue clauses", a particular kind of clauses that glucose detects and preserves during search. | ||
|
|
||
| ## Directory Overview | ||
| | Directory | Description | | ||
| | ----------- | ----------- | | ||
| | [mtl/](mtl/) | Minisat Template Library | | ||
| | [core/](core/) | A core version of the solver | | ||
| | [simp/](simp/) | An extended single-core solver with simplification capabilities (glucose) | | ||
| | [parallel/](parallel/) | A multi-core version of glucose called glucose-syrup | | ||
|
|
||
| ## Building | ||
| ``` | ||
| $ cd { simp | parallel } | ||
| $ make rs | ||
| ``` | ||
|
|
||
| ## Installation | ||
| ### Chocolatey | ||
| Glucose is available as a Chocolatey package [glucose](https://community.chocolatey.org/packages/glucose). Install by executing | ||
| ``` | ||
| > choco install glucose | ||
| ``` | ||
|
|
||
| ### Manual | ||
| Grab [the latest release](https://github.com/jakublevy/glucose-win/releases) and put it somewhere on your computer. | ||
|
|
||
| ## Usage | ||
| For the single-core solver: | ||
| ``` | ||
| > glucose --help | ||
| c | ||
| c This is glucose 4.1 -- based on MiniSAT (Many thanks to MiniSAT team) | ||
| c | ||
| c USAGE: glucose.exe [options] <input-file> <result-output-file> | ||
| where input may be either in plain or gzipped DIMACS. | ||
| CORE OPTIONS: | ||
| -forceunsat, -no-forceunsat (default: on) | ||
| -adapt, -no-adapt (default: on) | ||
| -fix-phas-rest, -no-fix-phas-rest (default: off) | ||
| -luby, -no-luby (default: off) | ||
| -gr, -no-gr (default: on) | ||
| -rnd-init, -no-rnd-init (default: off) | ||
| -gc-frac = <double> ( 0 .. inf) (default: 0.2) | ||
| -rinc = <double> ( 1 .. inf) (default: 2) | ||
| -rnd-seed = <double> ( 0 .. inf) (default: 9.16483e+07) | ||
| -rnd-freq = <double> [ 0 .. 1] (default: 0) | ||
| -cla-decay = <double> ( 0 .. 1) (default: 0.999) | ||
| -max-var-decay = <double> ( 0 .. 1) (default: 0.95) | ||
| -var-decay = <double> ( 0 .. 1) (default: 0.8) | ||
| -phase-restart = <int32> [ 0 .. 3] (default: 0) | ||
| -phase-saving = <int32> [ 0 .. 2] (default: 2) | ||
| -ccmin-mode = <int32> [ 0 .. 2] (default: 2) | ||
| CORE -- CERTIFIED UNSAT OPTIONS: | ||
| -certified, -no-certified (default: off) | ||
| -vbyte, -no-vbyte (default: off) | ||
| -certified-output = <string> | ||
| CORE -- MINIMIZE OPTIONS: | ||
| -minLBDMinimizingClause = <int32> [ 3 .. imax] (default: 6) | ||
| -minSizeMinimizingClause = <int32> [ 3 .. imax] (default: 30) | ||
| CORE -- REDUCE OPTIONS: | ||
| -chanseok, -no-chanseok (default: off) | ||
| -firstReduceDB = <int32> [ 0 .. imax] (default: 2000) | ||
| -incReduceDB = <int32> [ 0 .. imax] (default: 300) | ||
| -luby-factor = <int32> [ 1 .. imax] (default: 100) | ||
| -minLBDFrozenClause = <int32> [ 0 .. imax] (default: 30) | ||
| -specialIncReduceDB = <int32> [ 0 .. imax] (default: 1000) | ||
| -co = <int32> [ 2 .. imax] (default: 5) | ||
| CORE -- RESTART OPTIONS: | ||
| -K = <double> ( 0 .. 1) (default: 0.8) | ||
| -R = <double> ( 1 .. 5) (default: 1.4) | ||
| -szLBDQueue = <int32> [ 10 .. imax] (default: 50) | ||
| -szTrailQueue = <int32> [ 10 .. imax] (default: 5000) | ||
| MAIN OPTIONS: | ||
| -pre, -no-pre (default: on) | ||
| -model, -no-model (default: off) | ||
| -mem-lim = <int32> [ 0 .. imax] (default: 2147483647) | ||
| -verb = <int32> [ 0 .. 2] (default: 1) | ||
| -cpu-lim = <int32> [ 0 .. imax] (default: 2147483647) | ||
| -vv = <int32> [ 1 .. imax] (default: 10000) | ||
| -dimacs = <string> | ||
| SIMP OPTIONS: | ||
| -elim, -no-elim (default: on) | ||
| -rcheck, -no-rcheck (default: off) | ||
| -asymm, -no-asymm (default: off) | ||
| -simp-gc-frac = <double> ( 0 .. inf) (default: 0.5) | ||
| -grow = <int32> [imin .. imax] (default: 0) | ||
| -sub-lim = <int32> [ -1 .. imax] (default: 1000) | ||
| -cl-lim = <int32> [ -1 .. imax] (default: 20) | ||
| HELP OPTIONS: | ||
| --help Print help message. | ||
| --help-verb Print verbose help message. | ||
| ``` | ||
|
|
||
| For the multi-core solver: | ||
| ``` | ||
| > glucose-syrup --help | ||
| c | ||
| c This is glucose-syrup 4.1 (glucose in many threads) -- based on MiniSAT (Many thanks to MiniSAT team) | ||
| c | ||
| c USAGE: glucose-syrup.exe [options] <input-file> <result-output-file> | ||
| where input may be either in plain or gzipped DIMACS. | ||
| CORE OPTIONS: | ||
| -rnd-init, -no-rnd-init (default: off) | ||
| -gr, -no-gr (default: on) | ||
| -luby, -no-luby (default: off) | ||
| -fix-phas-rest, -no-fix-phas-rest (default: off) | ||
| -adapt, -no-adapt (default: on) | ||
| -forceunsat, -no-forceunsat (default: on) | ||
| -rinc = <double> ( 1 .. inf) (default: 2) | ||
| -gc-frac = <double> ( 0 .. inf) (default: 0.2) | ||
| -rnd-seed = <double> ( 0 .. inf) (default: 9.16483e+07) | ||
| -rnd-freq = <double> [ 0 .. 1] (default: 0) | ||
| -cla-decay = <double> ( 0 .. 1) (default: 0.999) | ||
| -max-var-decay = <double> ( 0 .. 1) (default: 0.95) | ||
| -var-decay = <double> ( 0 .. 1) (default: 0.8) | ||
| -ccmin-mode = <int32> [ 0 .. 2] (default: 2) | ||
| -phase-restart = <int32> [ 0 .. 3] (default: 0) | ||
| -phase-saving = <int32> [ 0 .. 2] (default: 2) | ||
| CORE -- MINIMIZE OPTIONS: | ||
| -minSizeMinimizingClause = <int32> [ 3 .. imax] (default: 30) | ||
| -minLBDMinimizingClause = <int32> [ 3 .. imax] (default: 6) | ||
| CORE -- REDUCE OPTIONS: | ||
| -chanseok, -no-chanseok (default: off) | ||
| -co = <int32> [ 2 .. imax] (default: 5) | ||
| -minLBDFrozenClause = <int32> [ 0 .. imax] (default: 30) | ||
| -specialIncReduceDB = <int32> [ 0 .. imax] (default: 1000) | ||
| -incReduceDB = <int32> [ 0 .. imax] (default: 300) | ||
| -firstReduceDB = <int32> [ 0 .. imax] (default: 2000) | ||
| -luby-factor = <int32> [ 1 .. imax] (default: 100) | ||
| CORE -- RESTART OPTIONS: | ||
| -K = <double> ( 0 .. 1) (default: 0.8) | ||
| -R = <double> ( 1 .. 5) (default: 1.4) | ||
| -szLBDQueue = <int32> [ 10 .. imax] (default: 50) | ||
| -szTrailQueue = <int32> [ 10 .. imax] (default: 5000) | ||
| CORE/PARALLEL -- UNSTABLE FEATURES OPTIONS: | ||
| -plingeling, -no-plingeling (default: off) | ||
| -reusedClauses, -no-reusedClauses (default: off) | ||
| MAIN OPTIONS: | ||
| -pre, -no-pre (default: on) | ||
| -model, -no-model (default: off) | ||
| -verb = <int32> [ 0 .. 2] (default: 1) | ||
| -vv = <int32> [ 1 .. imax] (default: 10000) | ||
| -cpu-lim = <int32> [ 0 .. imax] (default: 2147483647) | ||
| -mem-lim = <int32> [ 0 .. imax] (default: 2147483647) | ||
| PARALLEL OPTIONS: | ||
| -removeolder, -no-removeolder (default: off) | ||
| -maxmemory = <int32> [imin .. imax] (default: 20000) | ||
| -statsinterval = <int32> [imin .. imax] (default: 5) | ||
| -maxnbthreads = <int32> [imin .. imax] (default: 4) | ||
| -fifosize = <int32> [imin .. imax] (default: 100000) | ||
| -nthreads = <int32> [imin .. imax] (default: 0) | ||
| SIMP OPTIONS: | ||
| -asymm, -no-asymm (default: off) | ||
| -rcheck, -no-rcheck (default: off) | ||
| -elim, -no-elim (default: on) | ||
| -simp-gc-frac = <double> ( 0 .. inf) (default: 0.5) | ||
| -cl-lim = <int32> [ -1 .. imax] (default: 20) | ||
| -sub-lim = <int32> [ -1 .. imax] (default: 1000) | ||
| -grow = <int32> [imin .. imax] (default: 0) | ||
| HELP OPTIONS: | ||
| --help Print help message. | ||
| --help-verb Print verbose help message. | ||
| ``` | ||
|
|
||
| ## For more information about Glucose see [the official page](https://www.labri.fr/perso/lsimon/glucose). |
Oops, something went wrong.