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.

The Utility of Cardiopulmonary Exercise Testing in Difficult Asthma

Background: Unexplained persistent breathlessness in patients with difficult asthma despite multiple treatments is a common clinical problem. Cardiopulmonary exercise testing (CPX) may help identify the mechanism causing these symptoms, allowing appropriate management.

Methods: This was a retrospective analysis of patients attending a specialist-provided service for difficult asthma who proceeded to CPX as part of our evaluation protocol. Patient demographics, lung function, and use of health care and rescue medication were compared with those in patients with refractory asthma. Medication use 6 months following CPX was compared with treatment during CPX.

Results: Of 302 sequential referrals, 39 patients underwent CPX. A single explanatory feature was identified in 30 patients and two features in nine patients: hyperventilation (n = 14), exercise-induced bronchoconstriction (n = 8), submaximal test (n = 8), normal test (n = 8), ventilatory limitation (n = 7), deconditioning (n = 2), cardiac ischemia (n = 1). Compared with patients with refractory asthma, patients without “pulmonary limitation” on CPX were prescribed similar doses of inhaled corticosteroid (ICS) (median, 1,300 µg [interquartile range (IQR), 800-2,000 µg] vs 1,800 µg [IQR, 1,000-2,000 µg]) and rescue oral steroid courses in the previous year (median, 5 [1-6] vs 5 [1-6]). In this group 6 months post-CPX, ICS doses were reduced (median, 1,300 µg [IQR, 800-2,000 µg] to 800 µg [IQR, 400-1,000 µg]; P < .001) and additional medication treatment was withdrawn (n = 7). Patients with pulmonary limitation had unchanged ICS doses post CPX and additional therapies were introduced.

Conclusions: In difficult asthma, CPX can confirm that persistent exertional breathlessness is due to asthma but can also identify other contributing factors. Patients with nonpulmonary limitation are prescribed inappropriately high doses of steroid therapy, and CPX can identify the primary mechanism of breathlessness, facilitating steroid reduction.