This directory contains the source to MolecularSimulation, a simulation environment for experimentation with DNA computation.
Three molecular algorithms to solve Satsfiability are included in the implementation. These are:
- Liptons's algorithm (Brute force)
- Ogihara and Ray's algorithm (Branching heuristics)
- Distribution algorithm (Constructive)
Molecular Simulation is released under the MIT license.
See LICENSE for details.
This program was designed to execute in a 64-bit *NIX environment. Samples were executed on a 64-bit architecture with 4 GB of memory running Apple OS X 10.7.4.
*GCC
*Perl
Molecular Simulation simulates the execution of three molecular algorithms for Satisfiability.
Introduced in 1995 by Richard Lipton, this algorithm creates an exponential search space for the CNF expression. Once the space is created, each variable is evaluated and the space is reduced to only the solutions that satisfy all remaining strings. This algorithm is analogous to a conventional brute-force search for all solutions.
Originally introduced in 1996 by Mitsunori Ogihara, and extended in 1997 with Animesh Ray, this algorithm builds a solution space with a breadth-first search evaluation. Prior to execution to the algorithm, each of the clauses variable's in the CNF expression are sorted.
The Distribution algorithm parses an input CNF expression into growing and self regulated set of possible combinations. A possible combination begins with all members of the first clause, and subsequent variables from independent clauses are built upon the reduced state. If there exist self-complementary assignments spanning a clause, then the clause is eliminated.
Automation of execution can be done simply by executing the Perl script from the directory: MolecularSimulation/
$ perl runSimulation.pl
This file will sequentially invoke build.pl
and executeMolecularSat.pl
Argument | Parameters | Description |
-d |
Distribution algorithm | |
-l |
Lipton's algorithm | |
-o |
Ogihara and Ray's algorithm | |
-debug |
Debug | |
-p |
[CNF file path] |
Specify CNF file path. |
-f |
Write output to file. |
Output consists of a summary of the execution for a DIMACS CNF file. This output conforms to the SAT Competition format for the status of the *.cnf
expression. If desired, the output may be directed to a file. Conditional formatting of comment fields provide execution details.