tts: A SAT-Solver for Small, Difficult Instances

Research output: Contribution to journalArticle

105 Downloads (Pure)

Abstract

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.
Original languageEnglish
Pages (from-to)173-190
Number of pages18
JournalJournal on Satisfiability, Boolean Modeling and Computation
Volume4
Issue numbernull
Publication statusPublished - 2008

Fingerprint Dive into the research topics of 'tts: A SAT-Solver for Small, Difficult Instances'. Together they form a unique fingerprint.

  • Cite this