alepharchives / minisat-spfs Goto Github PK
View Code? Open in Web Editor NEWThis project forked from jod/minisat-spfs
A minimalistic and high-performance SAT solver implementing Symmetry Propagation
License: Other
This project forked from jod/minisat-spfs
A minimalistic and high-performance SAT solver implementing Symmetry Propagation
License: Other
This is the code for the Minisat+SP SAT solver which implements Symmetry Propagation (SP). A paper describing the algorithm has been accepted at ICTAI 2012, and will be published in due time. An older (and hence uncopyrighted) version of the paper is available at this repository under the name "Symmetry Propagation: Improved DynamicSymmetry Breaking in SAT.pdf". For full benchmark results, see the folder "full benchmark results". For cnf test files, see the folder "cnf test files". To compile and run Minisat+SP, go to the last paragraph of this readme. To download this repository without using git, click on the "ZIP" button in the upper left corner of the web page "https://github.com/JoD/minisat-SPFS". ================================================================================ Quick Install - Decide where to install the files . The simplest approach is to use GNU standard locations and just set a "prefix" for the root install directory (reffered to as $PREFIX below). More control can be achieved by overriding other of the GNU standard install locations (includedir, bindir, etc). Configuring with just a prefix: > make config prefix=$PREFIX - Compiling and installing: > make install ================================================================================ Configuration - Multiple configuration steps can be joined into one call to "make config" by appending multiple variable assignments on the same line. - The configuration is stored in the file "config.mk". Look here if you want to know what the current configuration looks like. - To reset from defaults simply remove the "config.mk" file or call "make distclean". - Recompilation can be done without the configuration step. [ TODO: describe configartion possibilities for compile flags / modes ] ================================================================================ Building [ TODO: describe seperate build modes ] ================================================================================ Install [ TODO: ? ] ================================================================================ Directory Overview: minisat/mtl/ Mini Template Library minisat/utils/ Generic helper code (I/O, Parsing, CPU-time, etc) minisat/core/ A core version of the solver minisat/simp/ An extended solver with simplification capabilities doc/ Documentation README LICENSE ================================================================================ Examples: Run minisat with same heuristics as version 2.0: > minisat <cnf-file> -no-luby -rinc=1.5 -phase-saving=0 -rnd-freq=0.02 ================================================================================ Minisat with Symmetry Propagation (SP): After running the Quick Install (see above), simply compile Minisat the normal way. For the tests, we used the following command: > make cr which compiles the Minisat release version without the simplification extension. Next, run minisat with a given cnf-file: > ./minisat_core <cnf-file> The SP-code will automatically check whether a file with the name <cnf-file>.txt is available at the same location as <cnf-file>. If this is the case, it will extract symmetries from this file, which should be in the format as generated by Shatter (http://www.aloul.net/Tools/shatter).
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.