Movatterモバイル変換

[0]ホーム
URL:

Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly

 Sign up
Appearance settings
/cosyPublic

License

NotificationsYou must be signed in to change notification settings

lip6/cosy

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

12 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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

Files:

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 tests

Build

To install cosy locally:

make install

it creates alib directory with the static cosy library and the headers files.

Running the tests

make run-test

Runs a set of unit tests that are based ongoogletest library.dependencies will be downloaded inthird_party directory.

License

This project is licensed under the GPLv3 - see the LICENSE.md file for details.

Some solvers with cosy integrated

Integrated solvers are stored insolvers directory.

Minisat

Original source code of glucose-3.0 can be foundhere

Compile

Execute following commands

cd solvers/minisat/core/export MROOT=..export LIBRARY_PATH='path_of_cosy_lib'make

Glucose-3.0

Original source code of glucose-3.0 can be foundhere

Compile

Execute following commands

cd solvers/glucose-3.0/core/export MROOT=..export LIBRARY_PATH='path_of_cosy_lib'make

Launch solver (computation of symmetries included)

With Bliss:

./launcher/bliss/launch.sh path_of_solver path_of_cnf_instance

Bliss automorphism tool is used, see Bliss on LICENCE.md file.

With Saucy3:

./launcher/saucy/launch.sh path_of_solver path_of_cnf_instance

The 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.

Releases

No releases published

Packages

No packages published

Contributors2

  •  
  •  

Languages

[8]ページ先頭
©2009-2025 Movatter.jp