The University of British Columbia - ß-Lab
|
|
The Stochastic Local Search SAT Solver
from The University of British Columbia - ß-Lab |
(return the the main ubcsat page) (check out the quick start guide)
1. What is UBCSAT?
In short, UBCSAT is an implementation and experimentation environment for Stochastic Local Search (SLS) Algorithms for the Satisfiability (SAT) and Maximum-Satisfiability (MAX-SAT) problems.
2. What algorithms does UBCSAT support?
We have now added an algorithms page to list them all
3. What input file format does UBCSAT support?
UBCSAT currently only reads from the DIMACS CNF file format which was described in here. UBCSAT can also read from weighted WCNF files, where the first parameter for each clause is a real value. There is a sample .cnf and .wcnf file provided with the latest ubcsat distribution.
4. What are the weighted algorithms?
Weighted algorithms are useful for solving the weighted MAX-SAT problem: where each clause is assigned a weight and the objective is to minimize the weights of all unsatisfied clauses. Weighted algorithms incorporate the clause weights into their algorithm.
5. Does the UBCSAT behave the same as the original algorithm (e.g.: WalkSAT, GSAT) implementation?
Yes. While the exact results may differ (because of different random seeds and random search trajectories, etc.) over several runs, to the best of our knowledge the run-length distributions for UBCSAT are identical to those produced by the original algorithms.
6. Is UBCSAT faster than the original algorithm code?
See the algorithms page for more details, but for most algorithms the UBCSAT code is faster (or just as fast) as the original implementations. In the few circumstances where UBCSAT is slower the difference is usually due to UBCSAT reporting overhead and can be eliminated by turning off reports (use parameters: -r out null -r stats null)
7. Does UBCSAT do any pre-processing such as in the R+AdaptNovelty+ algorithm?
No. UBCSAT does not not make any changes to the instance. However, the behaviour of an algorithm with pre-processing can easily be replicated in UBCSAT by first running the pre-processor to generate a new .cnf instance, and then run the UBCSAT algorithm implementation on that instance.
8. What are the -runs, -cutoff, -timeout and -srestart parameters, and how do they compare to MAX-TRIES, MAX-FLIPS in other algorithms?
In UBCSAT each run is a complete, independent execution of an algorithm on an instance. UBCSAT is designed so that multiple runs can be executed at once for the collection of many useful statistics. A run is ideally terminated after a solution is found, but they can also be terminated after a fixed amount of time (-timeout) or after fixed number of search steps (-cutoff). Within a run, a restart can happen after a specific number of steps (-srestart) or probabilistically (-prestart). Ideally, each run will be successful but depending on the algorithm and the instance that may be infeasible. In conventional notation used in the literature, a restart occurs after MAX-FLIPS, and this is tried MAX-TRIES, so in UBCSAT terms, you should use
-srestart MAX-FLIPS -cutoff (MAX-TRIES * MAX-FLIPS). If you are not as interested in performing multiple runs of such an experiment, and/or you would rather look at the statistics across multiple "tries" instead of runs, you can use-cutoff MAX-FLIPS -runs MAX-TRIES.
9. How to I get started programming within UBCSAT?
We will be adding support web pages to this website to help you. For now, we suggest reviewing our paper, and then exploring the software to see how algorithms such as GWSAT and WalkSAT have been implemented. Next, try looking at ubcsat-globals.h, and ubcsat-triggers.h to get you started.