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.

Zero-One Designs Produce Small Hard SAT Instances

Some basics of combinatorial block design are combined with certain constraint satisfaction problems of interest to the satisfiability community. The paper shows how such combinations lead to satisfiability problems, and shows empirically that these are some of the smallest very hard satisfiability problems ever constructed. Partially balanced (0,1) designs (PB01Ds) are introduced as an extension of balanced incomplete block designs (BIBDs) and (0,1) designs. Also, (0,1) difference sets are introduced as an extension of certain cyclical difference sets. Constructions based on (0,1) difference sets enable generation of PB01Ds over a much wider range of parameters than is possible for BIBDs. Building upon previous work of Spence, it is shown how PB01Ds lead to small, very hard, unsatisfiable formulas. A new three-dimensional form of combinatorial block design is introduced, and leads to small, very hard, satisfiable formulas. The methods are validated on solvers that performed well in the SAT 2009 and earlier competitions.

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.

Sequential antimicrobial therapy: treatment of severe lower respiratory tract infections in children

Although there have been a number of studies in adults, to date there has been little research into sequential antimicrobial therapy (SAT) in paediatric populations. The present study evaluates the impact of a SAT protocol for the treatment of severe lower respiratory tract infection in paediatric patients. The study involved 89 paediatric patients (44 control and 45 SAT). The SAT patients had a shorter length of hospital stay (4.0 versus 8.3 days), shorter duration of inpatient antimicrobial therapy (4.0 versus 7.9 days) with the period of iv therapy being reduced from a mean of 5.6 to 1.7 days. The total healthcare costs were reduced by 52%. The resolution of severe lower respiratory tract infection with a short course of iv antimicrobials, followed by conversion to oral therapy yielded clinical outcomes comparable to those achieved using longer term iv therapy. SAT proved to be an important cost-minimizing tool for realizing substantial healthcare costs savings.

THE EFFECTS OF 3 NON-ANTIBIOTIC, ANTIMICROBIAL AGENTS ON THE SURFACE HYDROPHOBICITY OF CERTAIN MICROORGANISMS EVALUATED BY DIFFERENT METHODS

The effects of three non-antibiotic, antimicrobial agents (taurolidine, chlorhexidine acetate and providone-iodine) on the surface hydrophobicity of the clinical strains Escherichia coli, Staphylococcus saprophyticus, Staphylococcus epidermidis and Candida albicans were examined. Three recognized techniques for hydrophobicity measurements, Bacterial Adherence to Hydrocarbons (BATH), the Salt Aggregation Test (SAT) and Hydrophobic Interaction Chromatography (HIC) were compared. At concentrations reported to interfere with microbial-epithelial cell adherence, all three agents altered the cell surface hydrophobicity. However, these effects failed to exhibit a uniform relationship. Generally, taurolidine and povidone-iodine treatments decreased the hydrophobicity of the strains examined whereas chlorhexidine acetate effects depended upon the micro-organism treated. Subsequently, the exact contribution of altered cell surface hydrophobicity to the reported microbial anti-adherence effects is unclear. Comparison of the three techniques revealed a better correlation between the results obtained with the BATH test and HIC than the results obtained with the BATH and SAT or SAT and HIC. However, these differences may be due to the inaccuracy associated with the visual assessment of results employed by the SAT.

‘”Like an Old Cathedral City”: Belfast Welcomes Queen Victoria, August 1849’,

Belfast, with its history of communal violence, is normally seen as lying outside the mainstream of nineteenth-century British urban development. The visit of Queen Victoria in 1849 suggests a more complex, less linear picture. What emerges is an urban identity in transition, in which aspirations to conform to an ideal of civic harmony temporarily overrode acute sectarian and political divisions, where pride in recent economic achievement sat uneasily alongside an awareness of the town’s newcomer status, and where an emerging sense of regional difference competed with a continuing assumption of Irish identity.

Mechanical fatigue and spectrum analysis of small-satellite

Mechanical fatigue due to environmental loads and spectrum analysis due to launch loads of the primary structure of a low cost, low-earth orbit small satellite intended for earth observation missions are presented. The payload of the satellite under consideration is a precise optical unit to image the earth’s surface having a mass of 45 kg. 3-D Finite Element Model for the satellite structure is generated by applying substructure method. Modal analysis is required to determine natural frequencies of the satellite and define its mode shape. Then, ranking of mode shapes according to specific constraint is performed. Harmonic analysis at resonance frequencies with the highest ranking is done and cumulative fatigue damage analysis is performed. Spectrum analysis is performed for Small Sat structure to verify the satellite structure reliability under all dynamic random vibration loads applied during transportation and launch cases.

Accounts of debates in the House of Commons, March– April 1731, supplementary to the diary of the first earl of Egmont

John Perceval (1685–1748), 1st Viscount Perceval and (from 1733) 1st Earl of Egmont, was an assiduous recorder of his own life and times. His diaries, published by the Historical Manuscripts Commission from manuscripts in the British Library, are the best source for parliamentary debates at Westminster in the 1730s. For the years 1730-1733, when Perceval sat in the Commons (as an Irish peer) they are remarkably full. His practice seems to have been to prepare two versions (presumably on the basis of notes taken in the House), the first attributing speeches to individuals, and the second, entered up in the diary, which listed speakers and summarized all arguments on each side. His letterbooks for 1731 contain accounts of five debates that embody his first editing process, with speeches attributed to individuals. They were sent to an Irish correspondent, Marmaduke Coghill, and largely omitted from the diary because Perceval had already transcribed them elsewhere. They are new to historians and cast light on two main issues: the unsuccessful attempts by Perceval and the ‘Irish lobby’ to persuade the British parliament to settle the Irish woollen trade, a question bedevilling Anglo-Irish relations in this period; and an attempt by the opposition to stir up anger against perceived Spanish aggression against Gibraltar. One of the most interesting features is the insight afforded into the Commons performances of Sir Robert Walpole: his management of debates, his own style of speaking, and his sharp exchanges with opponents like William Pulteney.

Magnetic and electronic structure of TICo2S2

An extensive investigation of the ferromagnetic compound TlCo2S2 has resulted in new information on the electronic and magnetic structure. Electronic structure calculations showed that magnetic ordering is energetically favorable with a clear driving force for ferromagnetic coupling within the cobalt layers. TlCo2S2 is metallic and the conductivity is due to holes in the valence band. XPS single crystal measurements did not show evidence of mixed oxidation states of cobalt. Neutron powder diffraction resulted in a ferromagnetic structure with the magnetic moment in the ab-plane. The derived magnetic moment of the cobalt atom is 0.65(2) mu(B) at 10 K and is in very good agreement with the value, mu(sat) = 0.65(1) mu(B) at 10 K, inferred from the magnetic hysteresis curve. (C) 2004 Elsevier Inc. All rights reserved.

Weakening Cardinality Constraints Creates Harder Satisfiability Benchmarks

For some time, the satisfiability formulae that have been the most difficult to solve for their size have been crafted to be unsatisfiable by the use of cardinality constraints. Recent solvers have introduced explicit checking of such constraints, rendering previously difficult formulae trivial to solve. A family of unsatisfiable formulae is described that is derived from the sgen4 family but cannot be solved using cardinality constraints detection and reasoning alone. These formulae were found to be the most difficult during the SAT2014 competition by a significant margin and include the shortest unsolved benchmark in the competition, sgen6-1200-5-1.cnf.

The Effect of Seat Location in Lecture Theatres on Academic Performance

The purpose of this research study was to investigate and identify possible patterns relating to academic performance on the effects of university students self-selecting where to sit in a lecture theatre.
The key research questions are:
1. Does seating position affect student performance?
2. Do the most academically able and engaged students regularly sit at the front of lecture theatres?
Academic achievement
Preliminary results suggest significant assessment score differences between those that sit at the front and those that sit further the back. Of those that received a grade of 75%+ (Grade A) 6.67% regularly sat at the back. With the same group 46.67% regularly sat at the front. Of the group that scored less than 50% (Grade D) 0% of students regularly sat at the front. 12.50% regularly sat in the middle zones with 37.50% sitting at the back. It was also observed that the remaining numbers did not consistently sit in the same zone.

Temporal movement
There is little evidence of movement between seating zones of the Grade A group throughout the 24 week period. However there was considerable movement with the Grade D group. Although still under analysis there appears be a pattern of students in this group graduating towards the back seating positions over the course of the programme.

Engagement
The frequency of completed entries on PinPoint was also used as an indicator of engagement. With the Grade A group 75% of them regularly completed an entry whereas in the Grade D group this drops to less than 50%.
Further analysis on the attitudinal factors in relational to seating position and performance are ongoing, but preliminary results suggest that those students that scored highly in attitude tended to sit at the front and middle sections.
It would indeed appear that the more highly engaged and academically capable students voluntarily sit at the front for most lectures. Interestingly as the course progresses those who had lesser engagement and below average midterm results tend to began to sit progressively toward the back. If this is a repeatable pattern then a linear regression analysis of the seating positions and midterm results could help predict students in danger of failing.