forked from niklasso/minisat
-
Notifications
You must be signed in to change notification settings - Fork 0
A minimalistic and high-performance SAT solver
License
CoroianMarius/minisat
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
================================================================================ 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 Organigram: Anghel Costel-Junior: Tested Equivalence-Chain-Principle benchmark family, tested particular cases for benchmarks, identified benchmark results patterns, described results and wrote/generated bibliography. Coroian Dan-Marius: Tested Tseitin-Formulas benchmark family, identified possible improvements, described reults, developed script used in benchmark running. Coverca Elena-Daniela: Analysed and identified main classes, data structures and alogirthms, documentating the source code. Bogdan Simina: Wrote summary and introduction, installation guide for MiniSat, did the UML diagram for source code. Week 10: Team sync regarding final project version Coroian Dan-Marius: Participated in discussion to establish future tasks. Coverca Elena-Daniela: Participated in discussion to establish future tasks. Anghel Costel-Junior: Participated in discussion to establish future tasks. Bogdan Simina: Participated in discussion to establish future tasks. Week 11: Team sync regarding code changes and future takes based on received feedback on friday meet Coroian Dan-Marius: We all had a meet where we managed to change code to display learned clauses in a separate file Coverca Elena-Daniela: We all had a meet where we managed to change code to display learned clauses in a separate file Anghel Costel-Junior: We all had a meet where we managed to change code to display learned clauses in a separate file Bogdan Simina: We all had a meet where we managed to change code to display learned clauses in a separate file Week 12: Coroian Dan-Marius: Code understanding Coverca Elena-Daniela: Sequence diagrams Anghel Costel-Junior: Benchmark further documentation based on papers Bogdan Simina: Code understanding Week 13: Team sync regarding code changes for uip identification for conflict analyzing Coroian Dan-Marius: Coverca Elena-Daniela: Anghel Costel-Junior: Bogdan Simina: Week 14: Team sync call regarding documentation improvements and presentationa and videos structure and contents Coroian Dan-Marius: Coverca Elena-Daniela: Anghel Costel-Junior: Bogdan Simina:
About
A minimalistic and high-performance SAT solver
Resources
License
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published
Languages
- C++ 92.4%
- Makefile 4.5%
- CMake 1.3%
- Other 1.8%