quick start

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 ubcsat@googlegroups.com if you have any trouble at all building the software.


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

> ubcsat

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)


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


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).


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.