quick start

Note: This Quick Start is a little out of date, but good enough for now.

BUILDING UBCSAT

If you are using linux or Microsoft Windows on an Intel machine, you don't have to build the software; the binaries are provided and named ubcsat and ubcsat.exe, respectively.

If you are building on another platform, the Makefile provided should be sufficient. Please email us at ubcsat@googlegroups.com if you have any trouble at all building the software.

RUNNING UBCSAT FOR THE FIRST TIME

If you run ubcsat for the first time, you will see a message similar to:

> ubcsat

UBCSAT version 1.1.0

GENERAL HELP

============

UBCSAT is a collection of Stochastic Local Search (SLS) algorithms for solving

Satisfiability (SAT) instances, and a tool for analyzing the behaviour of those

SLS algorithms with numerous reports and statistics.

UBCSAT always requires two key command-line parameters:

1) an algorithm to use, specified with the [-alg] parameter, and

2) a SAT instance file to solve, specified with [-i] parameter

For example, to use the SAPS algorithm to solve the instance file sample.cnf

>ubcsat -alg saps -i sample.cnf

If your primary goal is to find a solution, use the [-solve] parameter

>ubcsat -alg saps -i sample.cnf -solve

To analyze the behaviour of an SLS algorithm, you must run it several times.

To run the same algorithm 100 times with a maximum of a million steps per run:

>ubcsat -alg saps -i sample.cnf -runs 100 -cutoff 1000000

For additional help, consult one of the following:

ubcsat -hp list all of the [p]arameters

ubcsat -ha list the available [a]lgorithms

ubcsat -hw list the available [w]eighted algorithms

ubcsat -hr list the available [r]eports

ubcsat -hc For help with the [c]olumns of the default output report

ubcsat -hs For help with the [s]tatistics report

UBCSAT itself is not a SAT solving algorithm, but rather a collection of algorithms.

You must specify which algorithm you wish to use with the -alg parameter.

For now, you can choose the GSAT algorithm, which is one of the most famous Stochastic Local Search (SLS) algorithms for SAT.

> ubcsat -alg gsat

# UBCSAT version 1.1.0

# ubcsat -h for help

# no -inst file specified: reading instance from console (stdin)

# -- e.g.: ubcsat < myfile.cnf

So now ubcsat knows what algorithm to use, but it doesn't have a SAT problem to solve. You can either specify the file with the -inst parameter, or use redirection (<) as suggested by the output above. UBCSAT reads SAT instances in the DIMACS (.cnf) file format. We have provided a sample.cnf file for you.

Because we didn't specify an -inst file, ubcsat is trying to read the instance from the standard input (your keyboard :) -- Press Ctrl-C to cancel the program, and then type

> ubcsat -alg gsat -inst sample.cnf

Congratulations! You've run ubcsat. You'll be shown a lot of output (which will be explained in a later section)

SOLVING AN INSTANCE

Quite often you only need to solve a problem once, and after you've solved it, you'll want to know the solution. To have ubcsat show you a solution (or model) use the -solve parameter. Try using the same parameters as above and the -solve parameter:

> ubcsat -alg gsat -inst sample.cnf -solve

....

# No Solution found for -target 0

You'll most likely get an output statement (at the end) saying it couldn't find a solution. The -target parameter it refers to specifies the target solution quality, or the target number of unsatisfied (false) clauses. The default (0) means the instance is completely satisfied -- which is usually what you desire. Try again with a target of 10:

> ubcsat -alg gsat -inst sample.cnf -solve -target 10

...

# Solution found for -target 10

-1 -2 3 -4 5 6 7 8 -9 -10

11 12 -13 -14 -15 16 17 -18 -19 -20

...

It will easily find a solution that has 10 clauses unsatisfied. The output produced shows you the model for the solution. In this case, it would be: x1 = F; x2 = F; x3 = T; x4 = F; etc...

But you're usually looking for a solution with no unsatisfied clauses. A better approach might be to run the algorithm more than once. To do this, use the -runs parameter. If you run the GSAT algorithm 100 times, it will most likely find a solution:

> ubcsat -alg gsat -inst sample.cnf -solve -runs 100

...

Solution found for -target 0

...

Although the GSAT algorithm is famous, for many SAT problems it does not perform very well. We suggest you try -alg novelty+ or -alg saps instead of GSAT if you wish to find a solution faster.

> ubcsat -alg novelty+ -inst sample.cnf -solve

> ubcsat -alg saps -inst sample.cnf -solve

EXAMINING THE OUTPUT OF UBCSAT

If you want to analyse the behaviour of an SLS algorithm on a problem instance, you have to run the algorithm many times on the same instance. Try running -alg novelty+ -runs 100 on the sample instance:

> ubcsat -alg novelty+ -inst sample.cnf -runs 100

We will now look at the output and see what information ubcsat has provided:

Note: The outputs may look different on your screen for two reasons: 1) Cosmetic changes to ubcsat may have occurred and 2) This is a stochastic process, and so the search steps and other statistics will be different

First, we have the ubcsat header:

# UBCSAT version 1.1.0

# ubcsat -h for help

Followed by the ubcsat parameters used. Note that for unspecified parameters (for example, -cutoff) the default values are shown.

# -alg novelty+

# -runs 100

# -cutoff 100000

# -timeout 0

# -gtimeout 0

# -noimprove 0

# -target 0

# -wtarget 0

# -seed 794239013

# -solve 0

# -find,-numsol 0

# -findunique 0

# -srestart 0

# -prestart 0

# -drestart 0

# -novnoise 0.5

# -wp 0.01

After the parameters, we have the "output" report. There are actually several different reports in ubcsat (-hr to see a list). For this output report, we are shown the columns used in this report, with a description of each column:

# UBCSAT default output:

# 'ubcsat -r out null' to suppress, 'ubcsat -hc' for customization help

# run: Run Number

# found: Target Solution Quality Found? (1 => yes)

# best: Best (Lowest) # of False Clauses Found

# beststep: Step of Best (Lowest) # of False Clauses Found

# steps: Total Number of Search Steps

Followed by some column headers:

# F Best Step Total

# Run N Sol'n of Search

# No. D Found Best Steps

And then finally the actual output from ubcsat, which shows the results from each run (in this case, numbered 1..100).

1 1 0 9672 9672

...

100 1 0 16798 16798

That is the end of the output report (-r out).

The output report is immediately followed by the statistics report (-r stats):

Variables = 250

Clauses = 1065

TotalLiterals = 3195

TotalCPUTimeElapsed = 2.278

FlipsPerSecond = 846740

RunsExecuted = 100

SuccessfulRuns = 99

PercentSuccess = 99.00

Steps_Mean = 19288.74

Steps_CoeffVariance = 0.99652183317

Steps_Median = 12524.5

CPUTime_Mean = 0.0227800011635

CPUTime_CoeffVariance = 0.99652183317

CPUTime_Median = 0.0147914339958

You'll note that the percent success for these runs was only 99%. In practice, if you are going to be reporting results, you should ensure that 100% of your runs are successful by increasing the -cutoff parameter (which determines the maximum number of search steps allowed per run).

CUSTOMIZING THE OUTPUT OF UBCSAT

The columns that are provided in the output and the statistics generated can be customised: use the -hc (help columns) and -hs (help statistics) parameters respectively.

If you prefer to redirect the output to files, you can specify the output file with the (-r out filename) and you can redirect the statistics to a file with the (-r stats filename) parameter. To prevent them from being calculated (and make the execution slightly faster) use -r out null -r stats null.

For perspective, the default ubcsat parameters are:

-r out stdout run,found,best,beststep,steps

-r stats stdout numvars,numclauses,numlits,totaltime,fps,runs,percentsolve,steps[mean+cv+median],timesteps[mean+cv+median]

AND BEYOND...

Hopefully you've gotten your feet wet enough that you can start exploring ubcsat on your own. Feel free to e-mail us with your questions, and subscribe to the newsgroup to receive product updates.