Heat stress adaptation induces cross-protection against lethal acid stress conditions in Arcobacter butzleri but not in Campylobacter jejuni

The ability of many bacteria to adapt to stressful conditions may later protect them against the same type of stress (specific adaptive response) or different types of stresses (multiple adaptive response, also termed cross-protection). Arcobacter butzleri and Campylobacter jejuni are close phylogenetic relatives that occur in many foods of animal origin and have been linked with human illness (mainly diarrhoea). In the present study, sublethal stress adaptation temperatures (48 °C and 10 °C) and mild and lethal acid conditions (pH 5.0 and pH 4.0) were determined for A. butzleri and C. jejuni. In addition, it was evaluated whether these sublethal stress adaptations cause specific adaptive responses or cross-protection against subsequent mild or lethal acid stresses in these bacteria. The studies were conducted in broth adjusted to the different conditions and the results were determined by the dilution series plating method. It was shown that heat stress adapted A. butzleri (incubated for 2 h at 48 °C) were significantly more resistant to subsequent lethal acid stress (pH 4.0) than non-adapted cells at the 1 h time-point (p < 0.01 in Wilcoxon rank sum test). No specific adaptive responses against the stresses in A. butzleri or C. jejuni and no cross-protection in C. jejuni were found. The ability of heat stressed A. butzleri to tolerate later lethal acid conditions should be taken into account when designing new food decontamination and processing strategies.     

Unrestricted vs restricted cut in a tableau method for Boolean circuits

This paper studies the relative efficiency of variations of a tableau method for Boolean circuit satisfiability checking. The considered method is a nonclausal generalisation of the Davis–Putnam–Logemann–Loveland (DPLL) procedure to Boolean circuits. The variations are obtained by restricting the use of the cut (splitting) rule in several natural ways. It is shown that the more restricted variations cannot polynomially simulate the less restricted ones. For each pair of methods T, T′, an infinite family of circuits is devised for which T has polynomial size proofs while in T′ the minimal proofs are of exponential size w.r.t. n, implying exponential separation of T and T′ w.r.t. n. The results also apply to DPLL for formulas in conjunctive normal form obtained from Boolean circuits by using Tseitin’s translation. Thus DPLL with the considered cut restrictions, such as allowing splitting only on the variables corresponding to the input gates, cannot polynomially simulate DPLL with unrestricted splitting.AMS subject classification 03B70, 03F20, 68T15, 68T20The financial support from Academy of Finland (project #53695) is gratefully acknowledged.Tommi Junttila: This work was partially done while visiting ITC-IRST (Trento, Italy), and has been sponsored by the CALCULEMUS! IHP-RTN EC project, contract code HPRN-CT-2000-00102.     

MathSAT: Tight Integration of SAT and Mathematical Decision Procedures

Recent improvements in propositional satisfiability techniques (SAT) made it possible to tackle successfully some hard real-world problems (e.g., model-checking, circuit testing, propositional planning) by encoding into SAT. However, a purely Boolean representation is not expressive enough for many other real-world applications, including the verification of timed and hybrid systems, of proof obligations in software, and of circuit design at RTL level. These problems can be naturally modeled as satisfiability in linear arithmetic logic (LAL), that is, the Boolean combination of propositional variables and linear constraints over numerical variables. In this paper we present MathSAT, a new, SAT-based decision procedure for LAL, based on the (known approach) of integrating a state-of-the-art SAT solver with a dedicated mathematical solver for LAL. We improve MathSAT in two different directions. First, the top‐level line procedure is enhanced and now features a tighter integration between the Boolean search and the mathematical solver. In particular, we allow for theory-driven backjumping and learning, and theory-driven deduction; we use static learning in order to reduce the number of Boolean models that are mathematically inconsistent; we exploit problem clustering in order to partition mathematical reasoning; and we define a stack-based interface that allows us to implement mathematical reasoning in an incremental and backtrackable way. Second, the mathematical solver is based on layering; that is, the consistency of (partial) assignments is checked in theories of increasing strength (equality and uninterpreted functions, linear arithmetic over the reals, linear arithmetic over the integers). For each of these layers, a dedicated (sub)solver is used. Cheaper solvers are called first, and detection of inconsistency makes call of the subsequent solvers superfluous. We provide a through experimental evaluation of our approach, by taking into account a large set of previously proposed benchmarks. We first investigate the relative benefits and drawbacks of each proposed technique by comparison with respect to a reference option setting. We then demonstrate the global effectiveness of our approach by a comparison with several state-of-the-art decision procedures. We show that the behavior of MathSAT is often superior to its competitors, both on LAL and in the subclass of difference logic. This work has been partly supported by ISAAC, a European-sponsored project, contract no. AST3-CT-2003-501848; by ORCHID, a project sponsored by Provincia Autonoma di Trento; and by a grant from Intel Corporation. The work of T. Junttila has also been supported by the Academy of Finland, project 53695. S. Schulz has also been supported by a grant of the Italian Ministero dell'Istruzione, dell'Università e della Ricerca and the University of Verona.     

Recent advances in Apertium,a free/open-source rule-based machine translation platform for low-resource languages

This paper presents an overview of Apertium, a free and open-source rule-based machine translation platform. Translation in Apertium happens through a pipeline of modular tools, and the platform continues to be improved as more language pairs are added. Several advances have been implemented since the last publication, including some new optional modules: a module that allows rules to process recursive structures at the structural transfer stage, a module that deals with contiguous and discontiguous multi-word expressions, and a module that resolves anaphora to aid translation. Also highlighted is the hybridisation of Apertium through statistical modules that augment the pipeline, and statistical methods that augment existing modules. This includes morphological disambiguation, weighted structural transfer, and lexical selection modules that learn from limited data. The paper also discusses how a platform like Apertium can be a critical part of access to language technology for so-called low-resource languages, which might be ignored or deemed unapproachable by popular corpus-based translation technologies. Finally, the paper presents some of the released and unreleased language pairs, concluding with a brief look at some supplementary Apertium tools that prove valuable to users as well as language developers. All Apertium-related code, including language data, is free/open-source and available at https://github.com/apertium.

     

Experimental and Numerical Atomistic Investigation of the Third Body Formation Process in Dry Tungsten/Tungsten-Carbide Tribo Couples

The third body in tungsten/tungsten-carbide sliding systems is studied using a combination of experiments and atomistic simulations. Ex situ X-ray photoelectron spectroscopy and focused ion beam analysis of the structural and chemical changes near the surfaces reveals that sliding of tungsten against tungsten-carbide results in plastic deformation of the W surface, leading to grain refinement, and the formation of a mechanically mixed amorphous layer on the WC counter body. Molecular dynamics simulations of W/WC sliding couples exhibit the formation of a nanoscale amorphous W/WC interface. The infrequent occurrence of atomic jamming events in the interface resulted in the emission of dislocations into the W bulk and the generation of amorphous shear bands in the WC counter body in agreement with the different third bodies observed in W and WC after the experiments.