faq

Which version of UBCSAT should I use?
1. If you want the latest features & algorithms, and aren't afraid of a possible bug or two, then use the latest beta release. If you want publish results on an established algorithm, use a major release. See the branches page for more information.
What algorithms does UBCSAT support?

1. If you're interested in it, we might be too! email us at ubcsat@googlegroups.com.

1. a) UBCSAT currently supports the DIMACS CNF file format which was described in here. The SAT competitions also describe the format.
2. b) UBCSAT can also read from weighted WCNF files, where the first parameter for each clause is a weight (see the MAX-SAT competition for a description). There is a sample .cnf and .wcnf file provided with the ubcsat distribution.
3. Note: the format for .wcnf files in versions 1.0.0 and 1.1.0 use a real value for the clause weights. Version 1.2 onwards will support the MAX-SAT competition format for 64-bit integer weights.

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

Does the UBCSAT behave the same as the original algorithm (e.g.: WalkSAT, GSAT) implementation?

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

1. 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 parameter: -q)

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

What are the -runs, -cutoff, -timeout and -srestart parameters, and how do they compare to MAX-TRIES, MAX-FLIPS in other algorithms?

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