zbMATH — the first resource for mathematics

UBCSAT: An implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. (English) Zbl 1122.68620
Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 306-320 (2005).
Summary: In this paper we introduce UBCSAT, a new implementation and experimentation environment for Stochastic Local Search (SLS) algorithms for SAT and MAX-SAT. Based on a novel triggered procedure architecture, UBCSAT provides implementations of numerous well-known and widely used SLS algorithms for SAT and MAX-SAT, including GSAT, WalkSAT, and SAPS; these implementations generally match or exceed the efficiency of the respective original reference implementations. Through numerous reporting and statistical features, including the measurement of run-time distributions, UBCSAT facilitates the advanced empirical analysis of these algorithms. New algorithm variants, SLS algorithms, and reporting features can be added to UBCSAT in a straightforward and efficient way. UBCSAT is implemented in $$C$$ and runs on numerous platforms and operating systems; it is publicly and freely available at http://www.satlib.org/ubcsat.
For the entire collection see [Zbl 1075.68002].

MSC:
 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
MersenneTwister; SATLIB; UBCSAT; Walksat
Full Text: