The Ternary Tree Solver (tts)

The Ternary Tree Solver was developed to solve the propositional satisfiability problem. Specifically, it was written to be be entered in the annual SAT Competition and satisfies the input/output requirements of that competition. Version 4-0 participated in the SAT2007 Competition and won the silver medal for the "Crafted" category, UNSAT specialisation. The solver is written to target in particular small, difficult benchmarks. A short description is available.

The system is available for downloading. Both full source and statically-linked linux executable versions are available.

The author Ivor Spence can be contacted at i.spence@qub.ac.uk.

Ternary "tree" from nt-trimmed_3.cnf