Skip to content

CoroianMarius/minisat

 
 

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

No packages published

Languages

  • C++ 92.4%
  • Makefile 4.5%
  • CMake 1.3%
  • Other 1.8%