tts: A SAT-Solver for Small, Difficult Instances

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.

The prevalence of nonadherence in difficult asthma

Rationale: With the advent of new and expensive therapies for severe refractory asthma, targeting the appropriate patients is important. An important issue is identifying nonadherence with current therapies. The extent of nonadherence in a population with difficult asthma has not been previously reported.

Objectives: To examine the prevalence of nonadherence to corticosteroid medication in a population with difficult asthma referred to a Specialist Clinic and to examine the relationship of poor adherence to asthma outcome.

Methods: General practitioner prescription refill records for the previous 6 months for inhaled combination therapy and short-acting ß-agonists were compared with initial prescriptions and expressed as a percentage. Blood plasma prednisolone and cortisol assay levels were used to examine the utility of these measures in assessing adherence to oral prednisolone. Patient demographics, hospital admissions, lung function, oral prednisolone courses, and quality of life data were analyzed to indentify the variables associated with reduced medication adherence.

Measurements and Main Results: A total of 182 patients were assessed. Sixty-three patients (35%) filled 50% or fewer inhaled medication prescriptions; 88% admitted poor adherence with inhaled therapy after initial denial. Twenty-one percent of patients filled more than 100% of presciptions, and 45% of subjects filled between 51 and 100% of prescriptions. Twenty-three of 51 patients (45%) prescribed oral steroids were found to be nonadherent.

Conclusions: A significant proportion of patients with difficult-to-control asthma remained nonadherent to corticosteroid therapy. Objective surrogate and direct measures of adherence should be performed as part of a difficult asthma assessment and are important before prescibing expensive novel biological therapies.

sgen1: A generator of small but difficult satisfiability benchmarks

The satisfiability problem is known to be NP-Complete; therefore, there should be relatively small problem instances that take a very long time to solve. However, most of the smaller benchmarks that were once thought challenging, especially the satisfiable ones, can be processed quickly by modern SAT-solvers. We describe and make available a generator that produces both unsatisfiable and, more significantly, satisfiable formulae that take longer to solve than any others known. At the two most recent international SAT Competitions, the smallest unsolved benchmarks were created by this generator. We analyze the results of all solvers in the most recent competition when applied to these benchmarks and also present our own more focused experiments.