- Notifications
You must be signed in to change notification settings - Fork0
License
lip6/cosy
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
cosy is a library that exploits the symmetries of a SAT problemto cut off isomorphic parts of the search tree. It is a C++ implementation that can be virtuallyinterfaced with any CDCL SAT solver.
Authors: Hakan Metin, Souheib Baarir
Contacts:Souheib.baarir@lip6.fr
cosy/ adapters/ <- Some adapters include/ <- Headers files lib/ <- Libraries files LICENCE.md <- Licence file Makefile <- Top Level Makefile makefiles/ <- Subsidiary makefiles README.md <- This file scripts/ <- Some scripts solvers/ <- Some adapted solvers solvers/minisat/ <- Adapted Minisat SAT solver solvers/glucose-3.0/ <- Adapted Glucose 3.0 SAT solver launcher/ <- Store symmetry computer tools launcher/bliss/ <- Store bliss symmetry computer tools launcher/saucy/ <- Store saucy symmetry computer tools solvers/ <- Some adapted solvers src/ <- Source code tests/ <- Some testsTo install cosy locally:
make installit creates alib directory with the static cosy library and the headers files.
make run-testRuns a set of unit tests that are based ongoogletest library.dependencies will be downloaded inthird_party directory.
This project is licensed under the GPLv3 - see the LICENSE.md file for details.
Integrated solvers are stored insolvers directory.
Original source code of glucose-3.0 can be foundhere
Execute following commands
cd solvers/minisat/core/export MROOT=..export LIBRARY_PATH='path_of_cosy_lib'makeOriginal source code of glucose-3.0 can be foundhere
Execute following commands
cd solvers/glucose-3.0/core/export MROOT=..export LIBRARY_PATH='path_of_cosy_lib'makeWith Bliss:
./launcher/bliss/launch.sh path_of_solver path_of_cnf_instanceBliss automorphism tool is used, see Bliss on LICENCE.md file.
With Saucy3:
./launcher/saucy/launch.sh path_of_solver path_of_cnf_instanceThe graph generated to found symmetries is based on BreakID implementation.See BreakID in LICENCE.md files.
Saucy graph automorphism tool is used, see Saucy3 on LICENCE.md file.