tts: A SAT-Solver for Small, Difficult Instances


Autoria(s): Spence, Ivor
Data(s)

2008

Resumo

The Ternary Tree Solver (tts) is a complete solver for propositional satisfiability which was designed to have good performance on the most difficult small instances. It uses a static ternary tree data structure to represent the simplified proposition under all permissible partial assignments and maintains a database of derived propositions known to be unsatisfiable. In the SAT2007 competition version 4.0 won the silver medal for the category handmade, speciality UNSAT solvers and was the top qualifier for the second stage for handmade benchmarks, solving 11 benchmarks which were not solved by any other entrant. We describe the methods used by the solver and analyse the competition Phase 1 results on small benchmarks. We propose a first version of a comprehensive suite of small difficult satisfiability benchmarks (sdsb) and compare the worst-case performance of the competition medallists on these benchmarks.

Formato

application/pdf

Identificador

http://pure.qub.ac.uk/portal/en/publications/tts-a-satsolver-for-small-difficult-instances(e5c3b087-3205-408e-b257-1d6901424967).html

http://pure.qub.ac.uk/ws/files/564906/JSAT4_9_Spence.pdf

Idioma(s)

eng

Direitos

info:eu-repo/semantics/restrictedAccess

Fonte

Spence , I 2008 , ' tts: A SAT-Solver for Small, Difficult Instances ' Journal on Satisfiability, Boolean Modeling and Computation , vol 4 , no. null , pp. 173-190 .

Tipo

article