Command line tools

Command line tools

Since this implementation is written in 100% pure Java you can run it using the java command with main class com.anjlab.sat3.Program and all the jars from lib folder in CLASSPATH.

To make it easier to run we created two shell scripts: solve and solve-batch (files with *.bat extension for Windows, and files without extension are ruby scripts that you can use for Linux/Max OS X).

solve tool

You use this tool to solve single formula per run.

Just pass path to *.cnf file as argument to this tool and program will solve it:

solve examples/uf50-01000.cnf

By default output files will be created in the same folder as input file, i.e. examples/uf50-01000.cnf-results.txt and examples/uf50-01000.cnf-hss-0.png.

You can run solve tool without arguments to see complete list of supported command line options:

Reference Implementation of Romanov's Polynomial Algorithm for 3-SAT Problem
Copyright (C) 2010 AnjLab
This program comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it under certain conditions.
See LICENSE.txt file or visit <http://www.gnu.org/copyleft/lesser.html> for details.
Version: 1.0.3

usage: com.anjlab.sat3.Program [OPTIONS] <input-file-name>
                               Where <input-file-name> is a path to file
                               containing k-SAT formula instance in DIMACS
                               CNF or Romanov SKT file format.
 -a,--disable-assertions            Disables internal program self-check
                                    during execution. This may improve
                                    performance.
 -c,--create-skt                    Convert input formula to Romanov SKT
                                    file format.
 -e,--evaluate-formula <filename>   Evaluate formula using variable values
                                    from this file.
 -h,--help                          Prints this help message.
 -i,--hss-image-output <filename>   File name where visual representation
                                    of resulting basic graph will be
                                    written (only for SAT instances).
                                    Defaults to
                                    <input-file-name>-hss-0.png
 -o,--output <filename>             File name where result of calculations
                                    will be written (time measurements and
                                    satisfying set for SAT instances).
                                    Defaults to
                                    <input-file-name>-results.txt
 -p,--use-pretty-print              If specified, program will print
                                    detailed information about formulas
                                    including triplet values.
                                    Useful when studying how algorithm
                                    works (especially if variables count
                                    less than 20).
                                    Disabled by default.
 -u,--use-abc-var-names             If specified, program will use ABC
                                    names for variables (like 'a', 'b',
                                    ..., 'z' instead of 'x1', 'x2', etc.)
                                    during formula output.
                                    Disabled by default. Forced disabled
                                    if variables count more than 26.

Using options

In normal cases default options should be okay for you.

One good example of using custom options is when you learn how algorithm works. In this case you may want to see structures that algorithm uses during its work, like set of CTF or CTS for initial formula, unified CTS set, etc. Use '-p' option to see these structures.

See Solving article-example.cnf wiki page for example output.

solve-batch tool

With this tool you can solve all *.cnf files from some folder.

Simply pass folder name as argument to solve-batch and it will solve all *.cnf formulas from that folder:

solve-batch examples/

This tool doesn't support any options.

If corresponding *-results.txt file present for *.cnf then this formula will be skipped.

After all *.cnf formulas will be solved, solve-batch will run another tool to aggregate results in a single file aggregated-results.tab which is TAB-delimited file.