Note: This Quick Start is a little out of date, but good enough for now.
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 email@example.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 version 1.1.0
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
# Output Columns: |run|found|best|beststep|steps|
# 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]
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.