title: The Resolution of Keller’s Conjecture

text: We consider three graphs, [Formula: see text], [Formula: see text], and [Formula: see text], related to Keller’s conjecture in dimension 7. The conjecture is false for this dimension if and only if at least one of the graphs contains a clique of size [Formula: see text]. We present an automated method to solve this conjecture by encoding the existence of such a clique as a propositional formula. We apply satisfiability solving combined with symmetry-breaking techniques to determine that no such clique exists. This result implies that every unit cube tiling of [Formula: see text] contains a facesharing pair of cubes. Since a faceshare-free unit cube tiling of [Formula: see text] exists (which we also verify), this completely resolves Keller’s conjecture.


title: Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols

text: The word problem for a finite set of ground identities is known to be decidable in polynomial time, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we also assume that certain function symbols f are extensional in the sense that [Formula: see text] implies [Formula: see text]. In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.


title: Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis

text: The abduction problem in logic asks whether there exists a formula that is consistent with a given set of axioms and, together with these axioms, suffices to entail a given goal. We propose an approach for solving this problem that is based on syntax-guided enumeration. For scalability, we use a novel procedure that incrementally constructs a solution in disjunctive normal form that is built from enumerated formulas. The procedure can be configured to generate progressively weaker and simpler solutions over the course of a run of the procedure. Our approach is fully general and can be applied over any background logic that is handled by the underlying SMT solver in our approach. Our experiments show our approach compares favorably with other tools for abductive reasoning.


title: Politeness for the Theory of Algebraic Datatypes

text: Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.


title: Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates

text: We address the problem of proving the satisfiability of Constrained Horn Clauses (CHCs) with Algebraic Data Types (ADTs), such as lists and trees. We propose a new technique for transforming CHCs with ADTs into CHCs where predicates are defined over basic types, such as integers and booleans, only. Thus, our technique avoids the explicit use of inductive proof rules during satisfiability proofs. The main extension over previous techniques for ADT removal is a new transformation rule, called differential replacement, which allows us to introduce auxiliary predicates corresponding to the lemmas used when making inductive proofs. We present an algorithm that applies the new rule, together with the traditional folding/unfolding rules, for the automatic removal of ADTs. We prove that if the set of the transformed clauses is satisfiable, then so is the set of the original clauses. By an experimental evaluation, we show that the use of the new rule significantly improves the effectiveness of ADT removal, and that our approach is competitive with respect to a state-of-the-art tool that extends the CVC4 solver with induction.


title: Solving Bitvectors with MCSAT: Explanations from Bits and Pieces

text: We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results.


title: Formalizing the Face Lattice of Polyhedra

text: Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under sublattices.


title: How QBF Expansion Makes Strategy Extraction Hard

text: In this paper we show that the QBF proof checking format QRAT (Quantified Resolution Asymmetric Tautologies) by Heule, Biere and Seidl cannot have polynomial time strategy extraction unless P=PSPACE. In our proof, the crucial property that makes strategy extraction PSPACE-hard for this proof format is universal expansion, even expansion on a single variable. While expansion reasoning used in other QBF calculi can admit polynomial time strategy extraction, we find this is conditional on a property studied in proof complexity theory. We show that strategy extraction on expansion based systems can only happen when the underlying propositional calculus has the property of feasible interpolation.


title: Verification of Closest Pair of Points Algorithms

text: We verify two related divide-and-conquer algorithms solving one of the fundamental problems in Computational Geometry, the Closest Pair of Points problem. Using the interactive theorem prover Isabelle/HOL, we prove functional correctness and the optimal running time of [Formula: see text] of the algorithms. We generate executable code which is empirically competitive with handwritten reference implementations.


title: Logic-Independent Proof Search in Logical Frameworks: (Short Paper)

text: Logical frameworks like LF allow to specify the syntax and (natural deduction) inference rules for syntax/proof-checking a wide variety of logical systems. A crucial feature that is missing for prototyping logics is a way to specify basic proof automation. We try to alleviate this problem by generating [Formula: see text]Prolog (ELPI) inference predicates from logic specifications and controlling them by logic-independent helper predicates that encapsulate the prover characteristics. We show the feasibility of the approach with three experiments: We directly automate ND calculi, we generate tableau theorem provers and model generators.


title: Layered Clause Selection for Theory Reasoning: (Short Paper)

text: Explicit theory axioms are added by a saturation-based theorem prover as one of the techniques for supporting theory reasoning. While simple and effective, adding theory axioms can also pollute the search space with many irrelevant consequences. As a result, the prover often gets lost in parts of the search space where the chance to find a proof is low. In this paper, we describe a new strategy for controlling the amount of reasoning with explicit theory axioms. The strategy refines a recently proposed two-layer-queue clause selection and combines it with a heuristic measure of the amount of theory reasoning in the derivation of a clause. We implemented the new strategy in the automatic theorem prover Vampire and present an evaluation showing that our work dramatically improves the state-of-the-art clause-selection strategy in the presence of theory axioms.


title: A CTL* Model Checker for Petri Nets

text: This tool paper describes RGMEDD*, a CTL* model checker that computes the set of states (sat-sets) of a Petri net that satisfy a CTL* formula. The tool can be used as a stand-alone program or from the GreatSPN graphical interface. The tool is based on the decision diagram library Meddly, it uses Spot to translate (sub)formulae into Büchi automata and a variation of the Emerson-Lei algorithm to compute the sat-sets. Correctness has been assessed based on the Model Checking Context 2018 results (for LTL and CTL queries), the sat-set computation of GreatSPN (for CTL) and LTSmin (for LTL), and the [Formula: see text]-calculus model checker of LTSmin for proper CTL* formulae (using a translator from CTL* to [Formula: see text]-calculus available in LTSmin). As far as we know, RGMEDD* is the only available Büchi-based CTL* model checker.


title: PSPACE-Completeness of the Soundness Problem of Safe Asymmetric-Choice Workflow Nets

text: Asymmetric-choice workflow nets (ACWF-nets) are an important subclass of workflow nets (WF-nets) that can model and analyse business processes of many systems, especially the interactions among multiple processes. Soundness of WF-nets is a basic property guaranteeing that these business processes are deadlock-/livelock-free and each designed action has a potential chance to be executed. Aalst et al. proved that the soundness problem is decidable for general WF-nets and proposed a polynomial algorithm to check the soundness for free-choice workflow nets (FCWF-nets) that are a special subclass of ACWF-nets. Tiplea et al. proved that for safe acyclic WF-nets the soundness problem is co-NP-complete, and we proved that for safe WF-nets the soundness problem is PSPACE-complete. We also proved that for safe ACWF-nets the soundness problem is co-NP-hard, but this paper sharpens this result by proving that for safe ACWF-nets this problem is PSPACE-complete actually. This paper provides a polynomial-time reduction from the acceptance problem of linear bounded automata (LBA) to the soundness problem of safe ACWF-nets. The kernel of the reduction is to guarantee that an LBA with an input string does not accept the input string if and only if the constructed safe ACWF-net is sound. Based on our reduction, we easily prove that the liveness problem of safe AC-nets is also PSPACE-complete, but the best result on this problem was NP-hardness provided by Ohta and Tsuji. Therefore, we also strengthen their result.


title: Automated Repair of Process Models Using Non-local Constraints

text: State-of-the-art process discovery methods construct free-choice process models from event logs. Hence, the constructed models do not take into account indirect dependencies between events. Whenever the input behavior is not free-choice, these methods fail to provide a precise model. In this paper, we propose a novel approach for the enhancement of free-choice process models, by adding non-free-choice constructs discovered a-posteriori via region-based techniques. This allows us to benefit from both the performance of existing process discovery methods, and the accuracy of the employed fundamental synthesis techniques. We prove that the proposed approach preserves fitness with respect to the event log, while improving the precision when indirect dependencies exist. The approach has been implemented and tested on both synthetic and real-life datasets. The results show its effectiveness in repairing process models discovered from event logs.


title: Automatic Decomposition of Petri Nets into Automata Networks – A Synthetic Account

text: This article revisits the problem of decomposing a Petri net into a network of automata, a problem that has been around since the early 70s. We reformulate this problem as the transformation of an ordinary, one-safe Petri net into a flat, unit-safe NUPN (Nested-Unit Petri Net) and define a quality criterion based on the number of bits required for the structural encoding of markings. We propose various transformation methods, all of which we implemented in a tool chain that combines NUPN tools with third-party software, such as SAT solvers, SMT solvers, and tools for graph colouring and finding maximal cliques. We perform an extensive evaluation of these methods on a collection of more than 12,000 nets from diverse sources, including nets whose marking graph is too large for being explored exhaustively.


title: Piecewise Affine Dynamical Models of Timed Petri Nets – Application to Emergency Call Centers

text: We study timed Petri nets, with preselection and priority routing. We represent the behavior of these systems by piecewise affine dynamical systems. We use tools from the theory of nonexpansive mappings to analyze these systems. We establish an equivalence theorem between priority-free fluid timed Petri nets and semi-Markov decision processes, from which we derive the convergence to a periodic regime and the polynomial-time computability of the throughput. More generally, we develop an approach inspired by tropical geometry, characterizing the congestion phases as the cells of a polyhedral complex. We illustrate these results by a current application to the performance evaluation of emergency call centers in the Paris area.


title: A New Property of Choice-Free Petri Net Systems

text: When a Petri net system of some class is synthesised from a labelled transition system, it may be interesting to derive structural properties of the corresponding reachability graphs and to use them in a pre-synthesis phase in order to quickly reject inadequate transition systems, and provide fruitful error messages. The same is true for simultaneous syntheses problems. This was exploited for the synthesis of choice-free nets for instance, for which several interesting properties have been derived. We exhibit here a new property for this class, and analyse if this gets us closer to a full characterisation of choice-free synthesizable transition systems.


title: Subsumption Demodulation in First-Order Theorem Proving

text: Motivated by applications of first-order theorem proving to software analysis, we introduce a new inference rule, called subsumption demodulation, to improve support for reasoning with conditional equalities in superposition-based theorem proving. We show that subsumption demodulation is a simplification rule that does not require radical changes to the underlying superposition calculus. We implemented subsumption demodulation in the theorem prover Vampire, by extending Vampire with a new clause index and adapting its multi-literal matching component. Our experiments, using the TPTP and SMT-LIB repositories, show that subsumption demodulation in Vampire can solve many new problems that could so far not be solved by state-of-the-art reasoners.


title: Dynamic Recursive Petri Nets

text: In the early two-thousands, Recursive Petri nets (RPN) have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. While having a great expressive power, RPN suffer two limitations: (1) they do not include more general features for transitions like reset arcs, transfer arcs, etc. (2) the initial marking associated with the recursive “call” only depends on the calling transition and not on the current marking of the caller. Here we introduce Dynamic Recursive Petri nets (DRPN) which address these issues. We show that the standard extensions of Petri nets for which decidability of the coverability problem is preserved are particular cases of DPRN. Then we establish that w.r.t. coverability languages, DRPN are strictly more expressive than RPN. Finally we prove that the coverability problem is still decidable for DRPN.


title: SGGS Decision Procedures

text: SGGS (Semantically-Guided Goal-Sensitive reasoning) is a conflict-driven first-order theorem-proving method which is refutationally complete and model complete in the limit. These features make it attractive as a basis for decision procedures. In this paper we show that SGGS decides the stratified fragment which generalizes EPR, the PVD fragment, and a new fragment that we dub restrained. The new class has the small model property, as the size of SGGS-generated models can be upper-bounded, and is also decided by hyperresolution and ordered resolution. We report on experiments with a termination tool implementing a restrainedness test, and with an SGGS prototype named Koala.


title: A Combinator-Based Superposition Calculus for Higher-Order Logic

text: We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.


title: Synthesis for Multi-weighted Games with Branching-Time Winning Conditions

text: We investigate the synthesis problem in a quantitative game-theoretic setting with branching-time objectives. The objectives are given in a recursive modal logic with semantics defined over a multi-weighted extension of a Kripke structure where each transition is annotated with multiple nonnegative weights representing quantitative resources such as discrete time, energy and cost. The objectives may express bounds on the accumulation of each resource both in a global scope and in a local scope (on subformulae) utilizing a reset operator. We show that both the model checking problem as well as the synthesis problem are decidable and that the model checking problem is EXPTIME-complete, while the synthesis problem is in 2-EXPTIME and is NEXPTIME-hard. Furthermore, we encode both problems to the calculation of maximal fixed points on dependency graphs, thus achieving on-the-fly algorithms with the possibility of early termination.


title: Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams

text: We consider coloured Petri nets, qualitative and quantitative ones alike, as supported by our PetriNuts tool family, comprising, among others, Snoopy, Marcie and Spike. Currently, most analysis and simulation techniques require to unfold the given coloured Petri net into its corresponding plain, uncoloured Petri net representation. This unfolding step is rather straightforward for finite discrete colour sets, but tends to be time-consuming due to the potentially huge number of possible transition bindings. We present an unfolding approach building on a special type of symbolic data structures, called Interval Decision Diagram, and compare its runtime performance with an unfolding engine employing an off-the-shelf library to solve constraint satisfaction problems. For this comparison we use the 22 scalable coloured models from the MCC benchmark suite, complemented by a few from our own collection.


title: Formalizing a Seligman-Style Tableau System for Hybrid Logic: (Short Paper)

text: Hybrid logic is modal logic enriched with names for worlds. We formalize soundness and completeness proofs for a Seligman-style tableau system for hybrid logic in the proof assistant Isabelle/HOL. The formalization shows how to lift certain rule restrictions, thereby simplifying the original un-formalized proof. Moreover, the completeness proof we formalize is synthetic which suggests we can extend this work to prove a wider range of results about hybrid logic.


title: The Information Systems Modeling Suite: Modeling the Interplay Between Information and Processes

text: According to our recent proposal, an information system is a combination of a process model captured as a Petri Net with Identifiers, an information model specified in the first-order logic over finite sets with equality, and a specification of how the transitions in the net manipulate information facts. The Information Systems Modeling (ISM) Suite is an integrated environment for developing, simulating, and analyzing models of information systems, released under an open-source license. This paper presents the basic features of the ISM Suite.


title: A Knuth-Bendix-Like Ordering for Orienting Combinator Equations

text: We extend the graceful higher-order basic Knuth-Bendix order (KBO) of Becker et al. to an ordering that orients combinator equations left-to-right. The resultant ordering is highly suited to parameterising the first-order superposition calculus when dealing with the theory of higher-order logic, as it prevents inferences between the combinator axioms. We prove a number of desirable properties about the ordering including it having the subterm property for ground terms, being transitive and being well-founded. The ordering fails to be a reduction ordering as it lacks compatibility with certain contexts. We provide an intuition of why this need not be an obstacle when using it to parameterise superposition.


title: MCC: A Tool for Unfolding Colored Petri Nets in PNML Format

text: MCC is a tool designed for a very specific task: to transform the models of High-Level Petri nets, given in the PNML syntax, into equivalent Place/Transition nets. The name of the tool derives from the annual Model-Checking Contest, a competition of model-checking tools that provides a large and diverse collection of PNML models. This choice in naming serves to underline the main focus of the tool, which is to provide an open and efficient solution that lowers the access cost for developers wanting to engage in this competition. We describe the architecture and functionalities of our tool and show how it compares with other existing solutions. Despite the fact that the problem we target is abundantly covered in the literature, we show that it is still possible to innovate. To substantiate this assertion, we put a particular emphasis on two distinctive features of MCC that have proved useful when dealing with some of the most challenging colored models in the contest.


title: Visualizing Token Flows Using Interactive Performance Spectra

text: Process mining techniques can be used to discover process models from event data and project performance and conformance related diagnostics on such models. For example, it is possible to automatically discover Petri nets showing the bottlenecks in production, administration, transport, and financial processes. Also basic statistics (frequencies, average delays, standard deviations, etc.) can be projected on the places and transitions of such nets to reveal performance and compliance problems. However, real-life phenomena such as overtaking, batching, queueing, concept drift, and partial blocking of multiple cases remain invisible when considering basic statistics. This paper presents an approach combining Petri-net-based discovery techniques and so-called performance spectra based on token flows. Token production and consumption are visualized such that the true dynamics of the process are revealed. Our ProM implementation supports a range of visual-analytics features allowing the user to interact with the underlying event data and Petri net. Event data related to the handling of orders are used to demonstrate the functionality of our tool.


title: Cycl[Formula: see text]n – A Tool for Determining Stop-Transitions of Petri Nets

text: This paper introduces the tool Cycl[Formula: see text]n . The core functionality of Cycl[Formula: see text]n is to determine for a transition t of an unbounded Petri net whether or not t stops the net. A transition t stops the net (and is called a stop-transition) if each reachable marking of the net enables only finite occurrence sequences without occurrences of t. Cycl[Formula: see text]n provides a graphical user interface which also illustrates the graph structures leading to the computed result. This way, results are explained in a comprehensible manner, and the user gets a visual explanation of the cyclic behavior of the net causing these results.


title: Structural Reductions Revisited

text: Structural reductions are a powerful class of techniques that reason on a specification with the goal to reduce it before attempting to explore its behaviors. In this paper we present new structural reduction rules for verification of deadlock freedom and safety properties of Petri nets. These new rules are presented together with a large body of rules found in diverse literature. For some rules we leverage an SMT solver to compute if application conditions are met. We use a CEGAR approach based on progressively refining the classical state equation with new constraints, and memory-less exploration to confirm counter-examples. Extensive experimentation demonstrates the usefulness of this structural verification approach.


title: SNexpression: A Symbolic Calculator for Symmetric Net Expressions

text: The paper presents SNexpression: a tool for the symbolic structural analysis of Symmetric Nets (SN). It can operate at a low level, handling expressions required to compute the structural properties of interest, but features also a net-based way of interaction allowing to submit commands referring directly to the net structure avoiding error prone input of low level expressions. The User Interface implements a command line interpreter and provides also a multi-page notebook to keep track of the submitted commands and their result.


title: Data Centric Workflows for Crowdsourcing

text: Crowdsourcing consists in hiring workers on internet to perform large amounts of simple, independent and replicated work units, before assembling the returned results. A challenge to solve intricate problems is to define orchestrations of tasks, and allow higher-order answers where workers can suggest a process to obtain data rather than a plain answer. Another challenge is to guarantee that an orchestration with correct input data terminates, and produces correct output data. This work proposes complex workflows, a data-centric model for crowdsourcing based on orchestration of concurrent tasks and higher order schemes. We consider termination (whether some/all runs of a complex workflow terminate) and correctness (whether some/all runs of a workflow terminate with data satisfying FO requirements). We show that existential termination/correctness are undecidable in general excepted for specifications with bounded recursion. However, universal termination/correctness are decidable when constraints on inputs are specified in a decidable fragment of FO, and are at least in [Formula: see text].


title: Integrating Induction and Coinduction via Closure Operators and Proof Cycles

text: Coinductive reasoning about infinitary data structures has many applications in computer science. Nonetheless developing natural proof systems (especially ones amenable to automation) for reasoning about coinductive data remains a challenge. This paper presents a minimal, generic formal framework that uniformly captures applicable (i.e. finitary) forms of inductive and coinductive reasoning in an intuitive manner. The logic extends transitive closure logic, a general purpose logic for inductive reasoning based on the transitive closure operator, with a dual ‘co-closure’ operator that similarly captures applicable coinductive reasoning in a natural, effective manner. We develop a sound and complete non-well-founded proof system for the extended logic, whose cyclic subsystem provides the basis for an effective system for automated inductive and coinductive reasoning. To demonstrate the adequacy of the framework we show that it captures the canonical coinductive data type: streams.


title: A Study on Team Bisimulations for BPP Nets

text: BPP nets, a subclass of finite P/T nets, were equipped in [13] with an efficiently decidable, truly concurrent, behavioral equivalence, called team bisi-milarity. This equivalence is a very intuitive extension of classic bisimulation equivalence (over labeled transition systems) to BPP nets and it is checked in a distributed manner, without building a global model of the overall behavior of the marked BPP net. This paper has three goals. First, we provide BPP nets with various causality-based equivalences, notably a novel one, called causal-net bisimilarity, and (a version of) fully-concurrent bisimilarity [3]. Then, we define a variant equivalence, h-team bisimilarity, coarser than team bisimilarity. Then, we complete the study by comparing them with the causality-based semantics we have introduced: the main results are that team bisimilarity coincides with causal-net bisimilarity, while h-team bisimilarity with fully-concurrent bisimilarity.


title: Description Logics with Concrete Domains and General Concept Inclusions Revisited

text: Concrete domains have been introduced in the area of Description Logic to enable reference to concrete objects (such as numbers) and predefined predicates on these objects (such as numerical comparisons) when defining concepts. Unfortunately, in the presence of general concept inclusions (GCIs), which are supported by all modern DL systems, adding concrete domains may easily lead to undecidability. One contribution of this paper is to strengthen the existing undecidability results further by showing that concrete domains even weaker than the ones considered in the previous proofs may cause undecidability. To regain decidability in the presence of GCIs, quite strong restrictions, in sum called [Formula: see text]-admissibility, need to be imposed on the concrete domain. On the one hand, we generalize the notion of [Formula: see text]-admissibility from concrete domains with only binary predicates to concrete domains with predicates of arbitrary arity. On the other hand, we relate [Formula: see text]-admissibility to well-known notions from model theory. In particular, we show that finitely bounded, homogeneous structures yield [Formula: see text]-admissible concrete domains. This allows us to show [Formula: see text]-admissibility of concrete domains using existing results from model theory.


title: Soft Subexponentials and Multiplexing

text: Linear logic and its refinements have been used as a specification language for a number of deductive systems. This has been accomplished by carefully studying the structural restrictions of linear logic modalities. Examples of such refinements are subexponentials, light linear logic, and soft linear logic. We bring together these refinements of linear logic in a non-commutative setting. We introduce a non-commutative substructural system with subexponential modalities controlled by a minimalistic set of rules. Namely, we disallow the contraction and weakening rules for the exponential modality and introduce two primitive subexponentials. One of the subexponentials allows the multiplexing rule in the style of soft linear logic and light linear logic. The second subexponential provides the exchange rule. For this system, we construct a sequent calculus, establish cut elimination, and also provide a complete focused proof system. We illustrate the expressive power of this system by simulating Turing computations and categorial grammar parsing for compound sentences. Using the former, we prove undecidability results. The new system employs Lambek’s non-emptiness restriction, which is incompatible with the standard (sub)exponential setting. Lambek’s restriction is crucial for applications in linguistics: without this restriction, categorial grammars incorrectly mark some ungrammatical phrases as being correct.


title: On the High Complexity of Petri Nets [Formula: see text]-Languages

text: We prove that [Formula: see text]-languages of (non-deterministic) Petri nets and [Formula: see text]-languages of (non-deterministic) Turing machines have the same topological complexity: the Borel and Wadge hierarchies of the class of [Formula: see text]-languages of (non-deterministic) Petri nets are equal to the Borel and Wadge hierarchies of the class of [Formula: see text]-languages of (non-deterministic) Turing machines. We also show that it is highly undecidable to determine the topological complexity of a Petri net [Formula: see text]-language. Moreover, we infer from the proofs of the above results that the equivalence and the inclusion problems for [Formula: see text]-languages of Petri nets are [Formula: see text]-complete, hence also highly undecidable.


title: Circular Traffic Queues and Petri’s Cycloids

text: Two sorts of circular traffic systems are defined and their minimal length of recurrent transition sequences is computed. The result is used for finding cycloids that have an isomorphic reachability graph. Cycloids are particular Petri nets for modelling processes of actions or events, belonging to the fundaments of Petri’s general systems theory. They have very different interpretations, ranging from Einstein’s relativity theory to elementary information processing gates. The cycloid representation of circular traffic systems allows to identify basic synchronisation mechanisms and leads to a structure theory of such systems.


title: On-the-Fly Synthesis for Strictly Alternating Games

text: We study two-player zero-sum infinite reachability games with strictly alternating moves of the players allowing us to model a race between the two opponents. We develop an algorithm for deciding the winner of the game and suggest a notion of alternating simulation in order to speed up the computation of the winning strategy. The theory is applied to Petri net games, where the strictly alternating games are in general undecidable. We consider soft bounds on Petri net places in order to achieve decidability and implement the algorithms in our prototype tool. Finally, we compare the performance of our approach with an algorithm proposed in the seminal work by Liu and Smolka for calculating the minimum fixed points on dependency graphs. The results show that using alternating simulation almost always improves the performance in time and space and with exponential gain in some examples. Moreover, we show that there are Petri net games where our algorithm with alternating simulation terminates, whereas the algorithm without the alternating simulation loops for any possible search order.


title: Petri Nets Validation of Markovian Models of Emergency Department Arrivals

text: Modeling of hospital’s Emergency Departments (ED) is vital for optimisation of health services offered to patients that shows up at an ED requiring treatments with different level of emergency. In this paper we present a modeling study whose contribution is twofold: first, based on a dataset relative to the ED of an Italian hospital, we derive different kinds of Markovian models capable to reproduce, at different extents, the statistical character of dataset arrivals; second, we validate the derived arrivals model by interfacing it with a Petri net model of the services an ED patient undergoes. The empirical assessment of a few key performance indicators allowed us to validate some of the derived arrival process model, thus confirming that they can be used for predicting the performance of an ED.


title: Repairing Event Logs with Missing Events to Support Performance Analysis of Systems with Shared Resources

text: To identify the causes of performance problems or to predict process behavior, it is essential to have correct and complete event data. This is particularly important for distributed systems with shared resources, e.g., one case can block another case competing for the same machine, leading to inter-case dependencies in performance. However, due to a variety of reasons, real-life systems often record only a subset of all events taking place. For example, to reduce costs, the number of sensors is minimized or parts of the system are not connected. To understand and analyze the behavior of processes with shared resources, we aim to reconstruct bounds for timestamps of events that must have happened but were not recorded. We present a novel approach that decomposes system runs into token trajectories of cases and resources that may need to synchronize in the presence of many-to-many relationships. Such relationships occur, for example, in warehouses where packages for N incoming orders are not handled in a single delivery but in M different deliveries. We use linear programming over token trajectories to derive the timestamps of unobserved events in an efficient manner. This helps to complete the event logs and facilitates analysis. We focus on material handling systems like baggage handling systems in airports to illustrate our approach. However, the approach can be applied to other settings where recording is incomplete. The ideas have been implemented in ProM and were evaluated using both synthetic and real-life event logs.


title: NP Reasoning in the Monotone [Formula: see text]-Calculus

text: Satisfiability checking for monotone modal logic is known to be (only) NP-complete. We show that this remains true when the logic is extended with alternation-free fixpoint operators as well as the universal modality; the resulting logic – the alternation-free monotone [Formula: see text]-calculus with the universal modality – contains both concurrent propositional dynamic logic (CPDL) and the alternation-free fragment of game logic as fragments. We obtain our result from a characterization of satisfiability by means of Büchi games with polynomially many Eloise nodes.


title: Interleaving vs True Concurrency: Some Instructive Security Examples

text: Information flow security properties were defined some years ago in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems [17, 26]), and interleaving behavioral equivalences (e.g., bisimulation equivalence [27]). More recently, the distributed model of Petri nets has been used to study non-interference in [1, 5, 6], but also in these papers an interleaving semantics was used. By exploiting a simple process algebra, called CFM [18] and equipped with a Petri net semantics, we provide some examples showing that team equivalence, a truly-concurrent behavioral equivalence proposed in [19, 20], is much more suitable to define information flow security properties. The distributed non-interference property we propose, called DNI, is very easily checkable on CFM processes, as it is compositional, so that it does not suffer from the state-space explosion problem. Moreover, DNI is characterized syntactically on CFM by means of a type system.


title: A Comprehensive Framework for Saturation Theorem Proving

text: We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus, for instance within an Otter or [Image: see text] loop. Our framework is mechanized in Isabelle/ [Image: see text] .


title: Possible Models Computation and Revision – A Practical Approach

text: This paper describes a method of computing plausible states of a system as a logical model. The problem of analyzing state-based systems as they evolve over time has been studied widely in the automated reasoning community (and others). This paper proposes a specific approach, one that is tailored to situational awareness applications. The main contribution is a calculus for a novel specification language that is built around disjunctive logic programming under a possible models semantics, stratification in terms of event times, default negation, and a model revision operator for dealing with incomplete or erroneous events – a typical problem in realistic applications. The paper proves the calculus correct wrt. a formal semantics of the specification language and it describes the calculus’ implementation via embedding in Scala. This enables immediate access to rich data structures and external systems, which is important in practice.


title: Constructive Hybrid Games

text: Hybrid games combine discrete, continuous, and adversarial dynamics. Differential game logic ([Image: see text]) enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This constitutes the logical foundation for synthesis of correct control and monitoring code for safety-critical cyber-physical systems. Our contributions include novel semantics as well as soundness and consistency.


title: Mechanised Modal Model Theory

text: In this paper, we discuss the mechanisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in mechanisations of modal logic have centered on proof systems and applications in model-checking. We have mechanised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al. [1]). Among others, one important result, the Van Benthem characterisation theorem, characterises the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters.


title: A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic

text: Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.


title: Simulation as a Tool to Illustrate Clinical Pharmacology Concepts to Healthcare Program Learners

text: PURPOSE OF REVIEW: This article provides an overview of simulation as an effective and evolving tool for teaching clinical pharmacology within the health professions. Further, opportunities for positioning this methodology to meet current educational challenges are presented. RECENT FINDINGS: Clinical pharmacology is an essential core competency for all health professionals, correlating with ability to appropriately and safely prescribe, administer, or optimize medication regimens. Computer-assisted learning became the earliest form of simulation applied to pharmacology teaching, arising from increasing pressure to deviate from animal and tissue experiments in undergraduate education in the 1990s. In the last decade, high fidelity patient simulation, using manikin technology, has demonstrated benefit in building connectivity between knowledge and clinical application within patient care. Serious games, or computer-based educational games, provide an alternative method for creating context, with potential realized for newer technologies like augmented reality. These tools, while beneficial, are not applied in a uniform manner across programs. We advocate for routine incorporation of these tools as they offer significant opportunities to address the challenges faced in today’s healthcare education, particularly with the need for continued social distancing and limitations on in-person educational engagement during coronavirus. Partnership with faculty utilizing simulation in other areas of the curriculum will assist in overcoming potential barriers to implementation. SUMMARY: Simulation provides various methods that have significant potential to address the challenges in today’s provision of clinical pharmacology education, especially with new directives for social distancing and limitations for in-person educational engagement.


Internationale Aufmerksamkeit für das Corona-Taxi


title: Recent Trends and Future Directions in Research Regarding Parents with Intellectual and Developmental Disabilities

text: PURPOSE OF REVIEW: This report updates research on parents with IDD and their children published since 2014. RECENT FINDINGS: Since 2014, a plethora of studies using large administrative databases in different countries support a contextual approach to understand why parents with IDD and their children may have worse outcomes than other families. In most studies, increased risk of ill health in women with IDD and health and developmental problems in their children were fully or partially accounted for by socioeconomic and psychosocial hardships. New research has found that pregnant women with IDD tend to have risk factors for pregnancy, birth, and postpartum complications that may contribute to adverse child outcomes. Intervention research is gradually becoming more contextualized. SUMMARY: More studies are needed on multicultural aspects of parenting, programs that could help parents with IDD overcome social and health disadvantages, comprehensive and coordinated service models that start during pregnancy, innovative parent support arrangements, parenting education for teens and young adults with IDD, use of technology, and dissemination and implementation of evidence-based programs.


COVID-19 in five neighbouring limited resources countries: A financial and health threats


Retraction of studies on potential drug therapies for COVID-19: A call for reliability and scientific integrity


Endometrial Susceptibility to SARS COV-2: Explained by Gene Expression across the Menstrual Cycle?


Familial clusters of the 2019 novel coronavirus diseases in Taiwan


Mayo Clinic Strategies for COVID-19:Community-Based Drive-Through and Walk-Through Testing Centers


The Era of Point-of-Care Ultrasound Has Arrived; Are Cardiologists Ready?


Challenges and management options of tubo-ovarian cancer during the SARS-CoV-2 pandemic


Personal protective equipment, airway management and systematic reviews. Comment on Br J Anaesth 2020


Heart Failure Collaboratory Statement on Heart Failure Remote Monitoring in the Landscape of COVID-19 and Social Distancing


Editorial: The Immunology of Sepsis—Understanding Host Susceptibility, Pathogenesis of Disease, and Avenues for Future Treatment


Spasticity Treatment During COVID-19 Pandemic: Clinical Recommendations


Vitamin D Supplementation: A Potential Approach for Coronavirus/COVID-19 Therapeutics?


Nanobodies: Prospects of Expanding the Gamut of Neutralizing Antibodies Against the Novel Coronavirus, SARS-CoV-2


title: Epidemiology of sepsis and septic shock in intensive care units between sepsis-2 and sepsis-3 populations: sepsis prognostication in intensive care unit and emergency room (SPICE-ICU)

text: BACKGROUND: Diagnosing sepsis remains difficult because it is not a single disease but a syndrome with various pathogen- and host factor-associated symptoms. Sepsis-3 was established to improve risk stratification among patients with infection based on organ failures, but it has been still controversial compared with previous definitions. Therefore, we aimed to describe characteristics of patients who met sepsis-2 (severe sepsis) and sepsis-3 definitions. METHODS: This was a multicenter, prospective cohort study conducted by 22 intensive care units (ICUs) in Japan. Adult patients (≥ 16 years) with newly suspected infection from December 2017 to May 2018 were included. Those without infection at final diagnosis were excluded. Patient’s characteristics and outcomes were described according to whether they met each definition or not. RESULTS: In total, 618 patients with suspected infection were admitted to 22 ICUs during the study, of whom 530 (85.8%) met the sepsis-2 definition and 569 (92.1%) met the sepsis-3 definition. The two groups comprised different individuals, and 501 (81.1%) patients met both definitions. In-hospital mortality of study population was 19.1%. In-hospital mortality among patients with sepsis-2 and sepsis-3 patients was comparable (21.7% and 19.8%, respectively). Patients exclusively identified with sepsis-2 or sepsis-3 had a lower mortality (17.2% vs. 4.4%, respectively). No patients died if they did not meet any definitions. Patients who met sepsis-3 shock definition had higher in-hospital mortality than those who met sepsis-2 shock definition. CONCLUSIONS: Most patients with infection admitted to ICU meet sepsis-2 and sepsis-3 criteria. However, in-hospital mortality did not occur if patients did not meet any criteria. Better criteria might be developed by better selection and combination of elements in both definitions. TRIAL REGISTRATION: UMIN000027452


Editorial Desk


Stand for black lives matter: Association for the Psychoanalysis of Culture & Society


Impact of SARS-CoV-2 (Coronavirus) Pandemic on Public Mental Health


title: Occupational Exposure to Biological Agents

text: Biological risks were mentioned by the “European Agency for Safety and Health, at Work’s Expert Forecast on Emerging Biological Risks related to Occupational Safety and Health”, the second most important emerging risk. In an era when the “one health approach” is considered the right way to address public health issues occupational safety continues to look at biological agents as a minor issue compared to other agents. The food industry is known to be very committed to food safety assurance but less concerned with the safety of food operators unless they may compromise the quality of the food product. However, the focus on biological agents is essential not only due to air spread or contact with organic dust but we must not overlook another crucial aspect which is the antimicrobial resistance that may be associated with biological agents, nowadays one of the biggest threats to global health, food security and development.


title: Work in the Future: A Summary and Conclusion

text: As we conclude this book, the world is beset by a crisis of historic proportions. COVID-19, the disease caused by the SARS-CoV-2 virus, has rapidly spread throughout the globe, leaving death, sorrow, and economic hardship in its wake. Medical professionals and scientists the world over are trying to use their expertise to help monitor, make sense of, diagnose, prevent, and treat this infection.


Sommaire


Look for the helpers


title: History of heart transplantation, the resurgence of DCD heart donations and outcomes following transplantation; the Royal Papworth Experience

text: Human heart transplantation started more than half a century ago. The Royal Papworth Hospital, in Cambridgeshire, United Kingdom, where this procedure has been performed for more than four decades, has pioneered the resurgence of Donor Circulatory Death (DCD) heart transplantation, acknowledging the fact that the first transplant performed by Dr. Christian Barnard was from a DCD donor. The history of this procedure, the work carried out towards establishing a robust and successful DCD heart transplant program and the outcomes of the first fifty DCD heart transplants are described and discussed.


title: Project 6: The R Personal Assistant

text: If you are like me, you probably have a morning routine that involves information. Perhaps before you even get out of bed, you grab your phone or tablet and hit your “cycle” of apps: email, news, social media, and perhaps company reports and analytics. Sometimes it seems like you spend more of your time cycling through things than actually reading them. Wouldn’t it be nice to tie all of that together? In this chapter, we’ll do exactly that by having R build a daily briefing for us, and we’ll discuss ways to get it to us in the morning (or anytime we need it) as quickly and easily!


title: Retrospective Analysis of 2019-nCov-Infected Cases in Dongyang, Southeastern China

text: The 2019 novel coronavirus (2019-nCov) has caused increasing number of infected cases globally. This study was performed to analyze information regarding the transmission route and presence of viral nucleic acids on several clinical samples. Confirmed 2019-nCov-infected cases were identified in Dongyang and were treated according to guidelines for the diagnosis of 2019-nCov infection released by the National Health Commission. Information regarding the contacts that the infected people had was collected to determine whether it caused clustered cases. A series of successive nucleic acid examination of feces, oropharyngeal swabs, and sputum was also performed, and the results were analyzed. A total of 19 confirmed cases of 2019-nCov infection were identified in Dongyang, Zhejiang Province, China. Five cases showed severe symptoms, and the remaining ones showed mild manifestations. Ten cases infected from two asymptomatic individuals were clustered into two groups. Among 14 cases with consecutive nucleic acid test results, four patients showed positive results in feces after their negative conversion in oropharyngeal swabs. Asymptomatic individuals with the virus could cause 2019-nCov clustered cases, and the clustered cases may differ from sporadic cases on age and length of hospitalization. In addition, nucleic acids in feces last longer than those in oropharyngeal swabs.


title: Learn on the Fly

text: In this study, we explore the biologically-inspired Learn-On-The-Fly (LOTF) method that actively learns and discovers patterns with improvisation and sensory intelligence, including pheromone trails, structure from motion, sensory fusion, sensory inhibition, and spontaneous alternation. LOTF is related to classic online modeling and adaptive modeling methods. However, it aims to solve more comprehensive, ill-structured problems such as human activity recognition from a drone video in a disastrous environment. It helps to build explainable AI models that enable human-machine teaming with visual representation, visual reasoning, and machine vision. It is anticipated that LOTF would have an impact on Artificial Intelligence, video analytics for searching and tracking survivors’ activities for humanitarian assistance and disaster relief (HADR), field augmented reality, and field robotic swarms.


Regarding “Serial Quantitative Chest CT Assessment of COVID-19: Deep-Learning Approach”


title: COVID-19: A Multimodality Review of Radiologic Techniques, Clinical Utility, and Imaging Features

text: In this article we will review the imaging features of COVID-19 across multiple modalities, including radiography, computed tomography (CT), magnetic resonance imaging (MRI), positron emission tomography/computed tomography (PET/CT), and ultrasonography (US). Given that COVID-19 primarily affects the lung parenchyma by causing pneumonia, our directive is to focus on thoracic findings associated with COVID-19. We aim to enhance radiologists’ understanding of this disease in order to help guide diagnosis and management.


Accuracy of Low-Dose Chest CT Scan in Detection of COVID-19


title: Reliability in Extreme Isolation: A Natural Language Processing Tool for Stress Self-assessment

text: Life in isolation is a condition that affects more people every day. From isolation of people in case of an epidemic (Ebola, Coronavirus, ..) to mineworkers or scientist in the Antarctic environment, it is currently well established that extreme isolation is a stressor element which negatively affects human creating stress and social conflict. Living in outer space is one of the most extreme forms of isolation that can be used as a test bench for isolation research. Crews in space are expected to be able to manage independently stress and social conflict problems to be highly reliable and autonomous. Human natural language (NL) has the potential of being a valuable source of information on crew-members stress and reliability in isolation. Based on the use of NL, the PSI (Performance and Stress in Isolation) research group is developing an Artificial Intelligent tool for the autonomous monitoring of stress and reliability. In order to develop this tool, the first step (here presented) is to investigate the correlation of NL with stress and reliability within the PSI experiment. The experiment consisted of three tasks to be performed periodically during the isolation: 1. Analysis of free written communication (NL); 2. Short self-reference questionnaire; and 3. Detection of heart rate and blood pressure values. In this paper we present the preliminary data collected from 29 participants (17 males and 12 females) to 6 space analogue missions accomplished in Europe, the USA and Israel in the 2016 – 2019 time frames. That is, so far, the largest database ever analyzed of this kind. The results are coherent with what is described in the literature about NLP content and style analysis, with the novelty of the correlations found with the cardiovascular parameters, thus reinforcing the perspective of applying a NLP AI system for supporting stress management in extreme isolation contexts from Space to Earth spin off.


Re: “International Expert Consensus Statement on Chest Imaging in Pediatric COVID-19 Patient Management: Imaging Findings, Imaging Study Reporting and Imaging Study Recommendations”


title: Urbanicity mental costs valuation: a review and urban-societal planning consideration

text: Living in cities has numerous comparative advantages than living in the countryside or in small villages and towns, most notably better access to education, services and jobs. However, it is also associated with a roughly twofold increase in some mental disorders rate incidence compared with living in rural areas. Economic assessments reported a forecasted loss of more than 19 trillion dollars in global GDP between 2011 and 2030 and of around 7 trillion for the year 2030 alone when measured by the human capital method. If we exclude self-selection processes and make the hypothesis to be able to level down the mental illness rate incidence in urban areas to these of the rural by better urban-societal planning, around € 1.2 trillion could be saved yearly worldwide. Even a reduction of only 20% in urban mental illness rate would save around 250 billion dollars yearly.


title: A metabolic handbook for the COVID-19 pandemic

text: For infectious-disease outbreaks, clinical solutions typically focus on efficient pathogen destruction. However, the COVID-19 pandemic provides a reminder that infectious diseases are complex, multisystem conditions, and a holistic understanding will be necessary to maximize survival. For COVID-19 and all other infectious diseases, metabolic processes are intimately connected to the mechanisms of disease pathogenesis and the resulting pathology and pathophysiology, as well as the host defence response to the infection. Here, I examine the relationship between metabolism and COVID-19. I discuss why preexisting metabolic abnormalities, such as type 2 diabetes and hypertension, may be important risk factors for severe and critical cases of infection, highlighting parallels between the pathophysiology of these metabolic abnormalities and the disease course of COVID-19. I also discuss how metabolism at the cellular, tissue and organ levels might be harnessed to promote defence against the infection, with a focus on disease-tolerance mechanisms, and speculate on the long-term metabolic consequences for survivors of COVID-19.


The new normal


Infektiologische Notfälle und Sepsis


Overview


Pädiatrische Notfälle


title: Can We Improve the Monitoring of People With Multiple Sclerosis Using Simple Tools, Data Sharing, and Patient Engagement?

text: Technological innovation is transforming traditional clinical practice, enabling people with multiple sclerosis (pwMS) to contribute health care outcome data remotely between clinic visits. In both relapsing and progressive forms of multiple sclerosis (MS), patients may experience variable disability accrual and symptoms throughout their disease course. The potential impact on the quality of life (QoL) in pwMS and their families and carers is profound. The introduction of treatment targets, such as NEDA (no evidence of disease activity) and NEPAD (no evidence of progression or active disease), that guide clinical decision-making, highlight the importance of utilizing sensitive instruments to measure and track disease activity and progression. However, the gold standard neurological disability tool—expanded disability severity scale (EDSS)—has universally recognized limitations. With strides made in our understanding of MS pathophysiology and DMT responsiveness, maintaining the status quo of measuring disability progression is no longer the recommended option. Outside the clinical trial setting, a comprehensive monitoring system has not been robustly established for pwMS. A 21st-century approach is required to integrate clinical, paraclinical, and patient-reported outcome (PRO) data from electronic health records, local databases, and patient registries. Patient and public involvement (PPI) is critical in the design and implementation of this workflow. To take full advantage of the potential of digital technology in the monitoring and care and QoL of pwMS will require iterative feedback between pwMS, health care professionals (HCPs), scientists, and digital experts.


title: A Critical Blimp-1-Dependent IL-10 Regulatory Pathway in T Cells Protects From a Lethal Pro-inflammatory Cytokine Storm During Acute Experimental Trypanosoma brucei Infection

text: In many infectious diseases, the immune response operates as a double-edged sword. While required for protective immunity, infection-induced inflammation can be detrimental if it is not properly controlled, causing collateral body damage and potentially leading to death. It is in this context that the potent anti-inflammatory cytokine interleukin-10 (IL-10) is required to dampen the pro-inflammatory immune response that hallmarks trypanosomosis. Effective control of this infection requires not just the action of antibodies specific for the parasite's variable surface glycoprotein (VSG) coat antigens, but also a pro-inflammatory immune response mediated mainly by IFNγ, TNF, and NO. However, strict control of inflammation is mandatory, as IL-10-deficient mice succumb from an unrestrained cytokine storm within 10 days of a Trypanosome brucei infection. The relevant cellular source of IL-10 and the associated molecular mechanisms implicated in its trypanosomosis associated production are poorly understood. Using an IL-10 reporter mouse strain (Vert-X), we demonstrate here that NK cells, CD8(+) T cells and CD4(+) T cells as well as B cells and plasma cells constitute potential cellular sources of IL-10 within the spleen and liver during acute infection. The IL-10 wave follows peak pro-inflammatory cytokine production, which accompanied the control of peak parasitemia. Similar results were observed following conventional experimental needle infection and physiological infections via T. brucei-infected tsetse flies. Our results show that conditional T cell-specific ablation of the IL-10 regulating Prdm1 gene (encoding for the Blimp-1 transcription factor), leads to an uncontrolled trypanosome-induced pro-inflammatory syndrome like the one observed in infected IL-10-deficient mice. This result indicates that the biological role of IL-10-derived from non-T cells, including NK cells, is of minor importance when considering host survival. The cytokine IL-27 that is also considered to be an IL-10 regulator, did not affect IL-10 production during infection. Together, these data suggest that T. brucei activates a Blimp-1-dependent IL-10 regulatory pathway in T cells that acts as a critical anti-inflammatory rheostat, mandatory for host survival during the acute phase of parasitemia.


title: The Modulation of Mucosal Antiviral Immunity by Immunobiotics: Could They Offer Any Benefit in the SARS-CoV-2 Pandemic?

text: Viral respiratory infections are of major importance because of their capacity to cause of a high degree of morbidity and mortality in high-risk populations, and to rapidly spread between countries. Perhaps the best example of this global threat is the infectious disease caused by the new SARS-CoV-2 virus, which has infected more than 4 million people worldwide, causing the death of 287,000 persons according to the WHO's situation report on May 13, 2020. The availability of therapeutic tools that would be used massively to prevent or mitigate the detrimental effects of emerging respiratory viruses on human health is therefore mandatory. In this regard, research from the last decade has reported the impact of the intestinal microbiota on the respiratory immunity. It was conclusively demonstrated how the variations in the intestinal microbiota affect the responses of respiratory epithelial cells and antigen presenting cells against respiratory virus attack. Moreover, the selection of specific microbial strains (immunobiotics) with the ability to modulate immunity in distal mucosal sites made possible the generation of nutritional interventions to strengthen respiratory antiviral defenses. In this article, the most important characteristics of the limited information available regarding the immune response against SARS-CoV-2 virus are revised briefly. In addition, this review summarizes the knowledge on the cellular and molecular mechanisms involved in the improvement of respiratory antiviral defenses by beneficial immunobiotic microorganisms such as Lactobacillus rhamnosus CRL1505. The ability of beneficial microorganisms to enhance type I interferons and antiviral factors in the respiratory tract, stimulate Th1 response and antibodies production, and regulate inflammation and coagulation activation during the course of viral infections reducing tissue damage and preserving lung functionally, clearly indicate the potential of immunobiotics to favorably influence the immune response against SARS-CoV-2 virus.


title: Antibodies and Immunity During Kawasaki Disease

text: The cause of Kawasaki disease (KD), the leading cause of acquired heart disease in children, is currently unknown. Epidemiology studies support that an infectious disease is involved in at least starting the inflammatory cascade set off during KD. Clues from epidemiology support that humoral immunity can have a protective effect. However, the role of the immune system, particularly of B cells and antibodies, in pathogenesis of KD is still unclear. Intravenous immunoglobulin (IVIG) and other therapies targeted at modulating inflammation can prevent development of coronary aneurysms. A number of autoantibody responses have been reported in children with KD and antibodies have been generated from aneurysmal plasma cell infiltrates. Recent reports show that children with KD have similar plasmablast responses as other children with infectious diseases, further supporting an infectious starting point. As ongoing studies are attempting to identify the etiology of KD through study of antibody responses, we sought to review the role of humoral immunity in KD pathogenesis, treatment, and recovery.


title: Meningoencephalomyelitis of Unknown Origin in Cats: A Case Series Describing Clinical and Pathological Findings

text: Meningoencephalomyelitis of unknown origin (MUO) is an umbrella term describing inflammatory changes of the central nervous system (CNS) with suspected non-infectious etiology. Diagnosis of MUO mostly remains presumed in a clinical setting. Histopathological and immunohistochemical examination of CNS tissue represent additional tools for detection of inflammation and the exclusion of specific infectious agents. While MUO is well-described in canine patients, only little is known about MUO in cats. Previous reports of feline MUO involve either clinical findings or histopathological examination but not both. The present case series is the first report describing both clinical and histopathological findings of feline MUO: Four cats (age: 1.7–17.8 years) showed acute to chronic progressive neurological signs of encephalopathy or myelopathy. Three cats had extraneural signs (hyperthermia, weight loss, hyporexia, leukocytosis). Magnetic resonance imaging (MRI) showed multifocal intraparenchymal lesions in forebrain, brainstem or spinal cord with homogenous contrast enhancement (2/2). Cerebrospinal fluid (CSF) examination was normal or displayed albuminocytologic dissociation. Histopathology revealed a multifocal, lympho-histiocytic meningoencephalitis in three cases and a lympho-histiocytic myelitis in one case. Immunohistochemistry for feline parvovirus, feline coronavirus, feline herpesvirus, tick borne encephalitis virus, Borna disease virus, morbillivirus, rabies virus, suid herpesvirus-1, and Toxoplasma gondii were negative in all cases. ONE SENTENCE SUMMARY: This case series is the first one reporting both clinical and histopathological findings in cats with MUO. Feline MUO incorporates heterogeneous subtypes of sterile CNS inflammation.


title: Co-circulation of both low and highly pathogenic avian influenza H5 viruses in current poultry epidemics in Taiwan

text: Highly pathogenic avian influenza (HPAI) A(H5) viruses belonging to clade 2.3.4.4c of the A/goose/Guangdong/1/96-like (Gs/GD) lineage caused severe global outbreaks in domestic birds from 2014 to 2015, that also represented the first incursions of Gs/GD viruses into Taiwan and the USA. However, few studies have investigated the circulation of clade 2.3.4.4c viruses after 2015. Here, we describe Gs/GD clade 2.3.4.4c and Mexican-like H5N2 viruses that were isolated in Taiwan during active surveillance conducted in chicken farms from February to March 2019. Phylogenetic analysis demonstrated two distinct genome constellations of the clade 2.3.4.4c H5 viruses, with the internal genes of one of the new genotypes closely related to a virus isolated from a pintail (Anas acuta) in Taiwan, providing the first direct evidence that migratory birds play a role in importing viruses into Taiwan. Our study also confirmed the co-circulation of Gs/GD clade 2.3.4.4c and Mexican-like H5 lineage viruses in Taiwan, presenting a rare case where Gs/GD viruses developed sustained transmission alongside another enzootic H5 lineage, raising the possibility that homosubtypic immunity may mask virus transmission, potentially frustrating detection, and the implementation of appropriate control measures. To eradicate H5 viruses from poultry in Taiwan, further studies on the effect of co-circulation in poultry of low pathogenic avian influenza and HPAI viruses are needed. Furthermore, only with continued surveillance efforts globally can we fully discern dispersal patterns and risk factors of virus transmission both to and within Taiwan.


PPE Supply Chain Needs Data Transparency and Stress Testing


title: Propofol Safety in Anticoagulated and Nonanticoagulated Patients During Extracorporeal Membrane Oxygenation

text: Sedation management during extracorporeal membrane oxygenation(ECMO) is a common challenge encountered by treating intensivists. Data about the safety of propofol use during ECMO has been contradictory. We aimed to investigate associated risks of propofol use on oxygenator lifespan and to explore the effect of propofol use on oxygenator membranes when therapeutic anticoagulation was omitted. Adult respiratory ECMO patients who received propofol were retrospectively compared with those who did not, and outcomes were assessed by means of duration of oxygenator functionality before requiring an exchange, and number of exchanges during propofol use and/or ECMO support. Out of the 63patients included in the analysis, 46%received propofol during ECMO as part of sedation regimen. The use of propofol was not found to be associated with an increased incidence of oxygenator failure when compared with cohorts who did not receive propofol (21% propofol arm vs. 6% control, p = 0.13). When analyzed for anticoagulation omission effects, propofol did not increase the risk of oxygenator failure (p = 0.63). The only predictor that statistically predicted the risk of oxygenator failure was development of heparin-induced thrombocytopenia (HIT) during ECMO. The results of this study further support the previously reported safety of propofol utilization during respiratory ECMO even in the absence of anticoagulation.


title: Total Artificial Heart as Bridge to Cardiac Retransplantation

text: Mechanical circulatory support has been performed as a bridge to cardiac retransplantation in selected patients with graft failure. However, there is limited published experience on the use and potential benefit of the total artificial heart (TAH) as a bridge to cardiac retransplantation. We report on our institutional experience with 3 patients that received TAH as a bridge to retransplant, with 1 patient surviving post-retransplantation. This case series demonstrates the high-risk nature of this undertaking in cardiac retransplant candidates and highlights the issue of sensitization portending greater risk for poor outcomes after TAH as bridge to retransplantation.


title: Pandemic Guidance for Stroke Centers Aiding COVID-19 Treatment Teams

text: The coronavirus disease 2019 (COVID-19) pandemic has in some regions overwhelmed the capacity and staffing needs of healthcare systems, necessitating the provision of resources and staff from different disciplines to aid COVID treatment teams. Stroke centers have multidisciplinary clinical and procedural expertise to support COVID treatment teams. Staff safety and patient safety are essential, as are open lines of communication between stroke center leaders and hospital leadership in a pandemic where policies and procedures can change or evolve rapidly. Support needs to be allocated in a way that allows for the continued operation of a fully capable stroke center, with the ability to adjust if stroke center volume or staff attrition requires.


National Institutes of Health StrokeNet During the Time of COVID-19 and Beyond


Education: a neglected social determinant of health


Cover Illustration: “Frontline” mural, Ashton Lane, Glasgow, by the.rebel.bearBack from the Frontline


The state of English prisons and the urgent need for reform


title: Stigma, Acceptance and Belonging for People with IDD Across Cultures

text: PURPOSE OF REVIEW: This review explores recent literature (from 2017 onwards) to identify current developments related to reducing stigma and increasing acceptance for people with Intellectual and Developmental Disabilities (IDD) in their communities across diverse cultures. RECENT FINDINGS: We identified literature related to experiences of stigma for people with IDD and their families across diverse cultures, as well as current and potential interventions and approaches for promoting acceptance. SUMMARY: Although the literature confirms that stigma is still a major barrier to acceptance and inclusion for people with IDD regardless of culture, there appears to be progress in terms of using diverse approaches to support acceptance and belonging. Researchers are also increasingly acknowledging the importance of culture and context in the experience and mitigation of stigma. There remains a need for researchers and practitioners to include people with IDD in identifying and prioritising interventions that promote belonging within their communities.


The Juxtaposition of Caring


Lessons from clinical practice during COVID-19 pandemic()


Letter from the Guest Editor


Cannabis research: Risks of recreational use and potential medical applications


The Heterogeneity of Grief in India during Coronavirus disease 2019 (COVID-19) and the National Lockdown


title: Remote but not isolated

text: I helped organized an online seminar series for 1500 people by with no planning. Here is are some thoughts on how it went, what we learned, and how it might shape in person meetings in the future.


The Importance of the Clinical Internship for the Radiologist


Perspective from a Patient Partner


title: Designing New Phase Selection Heuristics

text: CDCL-based SAT solvers have transformed the field of automated reasoning owing to their demonstrated efficiency at handling problems arising from diverse domains. The success of CDCL solvers is owed to the design of clever heuristics that enable the tight coupling of different components. One of the core components is phase selection, wherein the solver, during branching, decides the polarity of the branch to be explored for a given variable. Most of the state-of-the-art CDCL SAT solvers employ phase-saving as a phase selection heuristic, which was proposed to address the potential inefficiencies arising from far-backtracking. In light of the emergence of chronological backtracking in CDCL solvers, we re-examine the efficiency of phase saving. Our empirical evaluation leads to a surprising conclusion: The usage of saved phase and random selection of polarity for decisions following a chronological backtracking leads to an indistinguishable runtime performance in terms of instances solved and PAR-2 score. We introduce Decaying Polarity Score (DPS) to capture the trend of the polarities attained by the variable, and upon observing lack of performance improvement due to DPS, we turn to a more sophisticated heuristic seeking to capture the activity of literals and the trend of polarities: Literal State Independent Decaying Sum (LSIDS). We find the 2019 winning SAT solver, Maple_LCM_Dist_ChronoBTv3, augmented with LSIDS solves 6 more instances while achieving a reduction of over 125 seconds in PAR-2 score, a significant improvement in the context of the SAT competition.


title: Community and LBD-Based Clause Sharing Policy for Parallel SAT Solving

text: Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses”. These clauses, when shared between the worker nodes of parallel solvers, should lead to better performance. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study. Some of the more well-known metrics to identify high-quality clauses for sharing include clause length, literal block distance (LBD), and clause usage in propagation. In this paper, we propose a new metric aimed at identifying high-quality learnt clauses and a concomitant clause-sharing policy based on a combination of LBD and community structure of Boolean formulas. The concept of community structure has been proposed as a possible explanation for the extraordinary performance of SAT solvers in industrial instances. Hence, it is a natural candidate as a basis for a metric to identify high-quality clauses. To be more precise, our metric identifies clauses that have low LBD and low community number as ones that are high-quality for applications such as verification and testing. The community number of a clause C measures the number of different communities of a formula that the variables in C span. We perform extensive empirical analysis of our metric and clause-sharing policy, and show that our method significantly outperforms state-of-the-art techniques on the benchmark from the parallel track of the last four SAT competitions.


title: Trail Saving on Backtrack

text: A CDCL SAT solver can backtrack a large distance when it learns a new clause, e.g, when the new learnt clause is a unit clause the solver has to backtrack to level zero. When the length of the backtrack is large, the solver can end up reproducing many of the same decisions and propagations when it redescends the search tree. Different techniques have been proposed to reduce this potential redundancy, e.g., partial/chronological backtracking and trail saving on restarts. In this paper we present a new trail saving technique that is not restricted to restarts, unlike prior trail saving methods. Our technique makes a copy of the part of the trail that is backtracked over. This saved copy can then be used to improve the efficiency of the solver’s subsequent redescent. Furthermore, the saved trail also provides the solver with the ability to look ahead along the previous trail which can be exploited to improve its efficiency. Our new trail saving technique offers different tradeoffs in comparison with chronological backtracking and often yields superior performance. We also show that our technique is able to improve the performance of state-of-the-art solvers.


title: Clause Size Reduction with all-UIP Learning

text: Almost all CDCL SAT solvers use the 1-UIP clause learning scheme for learning new clauses from conflicts, and our current understanding of SAT solving provides good reasons for using that scheme. In particular, the 1-UIP scheme yields asserting clauses, and these asserting clauses have minimum LBD among all possible asserting clauses. As a result of these advantages, other clause learning schemes, like i-UIP and all-UIP, that were proposed in early work are not used in modern solvers. In this paper, we propose a new technique for exploiting the all-UIP clause learning scheme. Our technique is to employ all-UIP learning under the constraint that the learnt clause’s LBD does not increase (over the minimum established by the 1-UIP clause). Our method can learn clauses that are significantly smaller than the 1-UIP clause while preserving the minimum LBD. Unlike previous clause minimization methods, our technique is not limited to learning a sub-clause of the 1-UIP clause. We show empirically that our method can improve the performance of state of the art solvers.


title: Sorting Parity Encodings by Reusing Variables

text: Parity reasoning is challenging for CDCL solvers: Refuting a formula consisting of two contradictory, differently ordered parity constraints of modest size is hard. Two alternative methods can solve these reordered parity formulas efficiently: binary decision diagrams and Gaussian Elimination (which requires detection of the parity constraints). Yet, implementations of these techniques either lack support of proof logging or introduce many extension variables. The compact, commonly-used encoding of parity constraints uses Tseitin variables. We present a technique for short clausal proofs that exploits these Tseitin variables to reorder the constraints within the DRAT system. The size of our refutations of reordered parity formulas is [Formula: see text].


title: Four Flavors of Entailment

text: We present a novel approach for enumerating partial models of a propositional formula, inspired by how theory solvers and the SAT solver interact in lazy SMT. Using various forms of dual reasoning allows our CDCL-based algorithm to enumerate partial models with no need for exploring and shrinking full models. Our focus is on model enumeration without repetition, with potential applications in weighted model counting and weighted model integration for probabilistic inference over Boolean and hybrid domains. Chronological backtracking renders the use of blocking clauses obsolete. We provide a formalization and examples. We further discuss important design choices for a future implementation related to the strength of dual reasoning, including unit propagation, using SAT or QBF oracles.


title: Hemodynamic and Systemic Effects of Albumin in Patients with Advanced Liver Disease

text: PURPOSE OF REVIEW: Albumin administration is recommended to prevent or treat specific complications of decompensated cirrhosis based on its capacity to expand plasma volume. However, the molecule also has many other biological properties that are unrelated to the oncotic activity. The purpose of this review is to examine the hemodynamic and systemic effects of albumin administration in patients with decompensated cirrhosis. RECENT FINDINGS: Besides plasma expansion, albumin appears to act against inflammation, facilitate immunocompetence, and improve cardiac and endothelial function, thus antagonizing critical steps in the pathophysiological cascade underlying decompensated cirrhosis. SUMMARY: Increasing knowledge of the pathophysiological mechanisms of the disease, as well the pleiotropic properties of the molecule, provides the rationale for considering albumin as a multi-target disease-modifying agent in decompensated cirrhosis. Both oncotic and non-oncotic properties likely concur with the clinical benefits of long-term albumin administration recently demonstrated in these patients.


title: German hospital capacities for prolonged mechanical ventilator weaning in neurorehabilitation – results of a representative survey

text: A brief survey among members of the German Neurorehabilitation Society aimed to document the hospital capacities (“beds”) for prolonged weaning from a mechanical ventilator for patients with neuro-disabilities that require simultaneous multi-professional neurorehabilitation treatment. Sixty-eight institutions declared to have capacities with a broad distribution across Germany and its federal states. Overall, 1094 “beds” for prolonged weaning (and neurorehabilitation) were reported, 871 together with further information regarding their identification and hence regional location. These units had on average 16.1 beds for prolonged weaning (95% confidence interval 12.6 to 19.6) with a range from 2 to 68 beds per organization. The data indicate substantial capacities for the combined prolonged weaning and neurorehabilitation treatment in Germany. For most “beds” included in this analysis a basic validation was possible. While a reasonable coverage of these specialized service capacities by the survey is likely, the number reported could still be biased by underreporting by non-response. Both the broad variation of number of “beds” for prolonged weaning per unit and their unequal geographical distribution across federal states (per capita rate) warrant a more refined follow-up survey that will provide insights into reasons for the observed pattern of variation for these specialized hospital capacities.


title: Distributed Cube and Conquer with Paracooba

text: Cube and conquer is currently the most effective approach to solve hard combinatorial problems in parallel. It organizes the search in two phases. First, a look-ahead solver splits the problem into many sub-problems, called cubes, which are then solved in parallel by incremental CDCL solvers. In this tool paper we present the first fully integrated and automatic distributed cube-and-conquer solver Paracooba targeting cluster and cloud computing. Previous work was limited to multi-core parallelism or relied on manual orchestration of the solving process. Our approach uses one master per problem to initialize the solving process and automatically discovers and releases compute nodes through elastic resource usage. Multiple problems can be solved in parallel on shared compute nodes, controlled by a custom peer-to-peer based load-balancing protocol. Experiments show the scalability of our approach.


title: Improving Implementation of SAT Competitions 2017–2019 Winners

text: The results of annual SAT competitions are often viewed as the milestones showcasing the progress in SAT solvers. However, their competitive nature leads to the situation when the majority of this year’s solvers are based on previous year’s winner. And since the main focus is always on novelty, it means that there are times when some implementation details have a potential for improvement, but they are just inherited from solver to solver for several years in a row. In this study we propose small modifications of implementations of existing heuristics in several related SAT solvers. These modifications mostly consist in employing a deterministic strategy for switching between branching heuristics and in augmentations of the treatment of Tier2 and Core clauses. In our experiments we show that the proposed changes have a positive effect on solvers’ performance both individually and in combination with each other.


title: Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits

text: Approximate circuits that trade the chip area or power consumption for the precision of the computation play a key role in development of energy-aware systems. Designing complex approximate circuits is, however, very difficult, especially, when a given approximation error has to be guaranteed. Evolutionary search algorithms together with SAT-based error evaluation currently represent one of the most successful approaches for automated circuit approximation. In this paper, we apply satisfiability solving not only for circuit evaluation but also for its minimisation. We consider and evaluate several approaches to this task, both inspired by existing works as well as novel ones. Our experiments show that a combined strategy, integrating evolutionary search and SMT-based sub-circuit minimisation (using quantified theory of arrays) that we propose, is able to find complex approximate circuits (e.g. 16-bit multipliers) with considerably better trade-offs between the circuit precision and size than existing approaches.


title: SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing

text: In Wire Arc Additive Manufactoring (WAAM), an object is welded from scratch. Finding feasible welding paths that make use of the potential of the technology is a computationally complex problem as it requires planning paths in 3D. All parts of the object to be manufactured have to be visited in few welding paths. The search for such welding paths in 3D can be mapped to searching for a fragmented Hamiltonian path in a mathematical graph. We propose a SAT-based approach to finding such fragmented Hamiltonian paths that is suitable for planning WAAM paths. We show how to encode the search for such paths as a mix of SAT clauses and one non-clausal constraint that can be integrated into the SAT solver itself. The reasoning power of the solver enables us to impose additional constraints coming from the application domain on the planned paths, and we show experimentally that in this way, we can find welding paths for relatively complex object geometries.


title: On the Effect of Learned Clauses on Stochastic Local Search

text: There are two competing paradigms in successful SAT solvers: Conflict-driven clause learning (CDCL) and stochastic local search (SLS). CDCL uses systematic exploration of the search space and has the ability to learn new clauses. SLS examines the neighborhood of the current complete assignment. Unlike CDCL, it lacks the ability to learn from its mistakes. This work revolves around the question whether it is beneficial for SLS to add new clauses to the original formula. We experimentally demonstrate that clauses with a large number of correct literals w. r. t. a fixed solution are beneficial to the runtime of SLS. We call such clauses high-quality clauses. Empirical evaluations show that short clauses learned by CDCL possess the high-quality attribute. We study several domains of randomly generated instances and deduce the most beneficial strategies to add high-quality clauses as a preprocessing step. The strategies are implemented in an SLS solver, and it is shown that this considerably improves the state-of-the-art on randomly generated instances. The results are statistically significant.


title: Reproducible Efficient Parallel SAT Solving

text: In this paper, we propose a new reproducible and efficient parallel SAT solving algorithm. Unlike sequential SAT solvers, most parallel solvers do not guarantee reproducible behavior due to maximizing the performance. The unstable and non-deterministic behavior of parallel SAT solvers hinders a wider adoption of parallel solvers to the practical applications. In order to achieve robust and efficient parallel SAT solving, we propose two techniques to significantly reduce idle time in deterministic parallel SAT solving: delayed clause exchange and accurate estimation of execution time of clause exchange interval between solvers. The experimental results show that our reproducible parallel SAT solver has comparable performance to non-deterministic parallel SAT solvers even in a many-core environment.


title: On Weakening Strategies for PB Solvers

text: Current pseudo-Boolean solvers implement different variants of the cutting planes proof system to infer new constraints during conflict analysis. One of these variants is generalized resolution, which allows to infer strong constraints, but suffers from the growth of coefficients it generates while combining pseudo-Boolean constraints. Another variant consists in using weakening and division, which is more efficient in practice but may infer weaker constraints. In both cases, weakening is mandatory to derive conflicting constraints. However, its impact on the performance of pseudo-Boolean solvers has not been assessed so far. In this paper, new application strategies for this rule are studied, aiming to infer strong constraints with small coefficients. We implemented them in Sat4j and observed that each of them improves the runtime of the solver. While none of them performs better than the others on all benchmarks, applying weakening on the conflict side has surprising good performance, whereas applying partial weakening and division on both the conflict and the reason sides provides the best results overall.


title: Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles

text: Cohn and Umans proposed a framework for developing fast matrix multiplication algorithms based on the embedding computation in certain groups algebras [9]. In subsequent work with Kleinberg and Szegedy, they connected this to the search for combinatorial objects called strong uniquely solvable puzzles (strong USPs) [8]. We begin a systematic computer-aided search for these objects. We develop and implement algorithms based on reductions to [Formula: see text] and [Formula: see text] to verify that puzzles are strong USPs and to search for large strong USPs. We produce tight bounds on the maximum size of a strong USP for width [Formula: see text], and construct puzzles of small width that are larger than previous work. Although our work only deals with puzzles of small-constant width and does not produce a new, faster matrix multiplication algorithm, we provide evidence that there exist families of strong USPs that imply matrix multiplication algorithms that are more efficient than those currently known.


title: Strong (D)QBF Dependency Schemes via Tautology-Free Resolution Paths

text: We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency scheme. We establish soundness of the tautology-free scheme, implying that it can be used in any DQBF proof system. We further explore the power of DQBF resolution systems parameterised by dependency schemes and show that our new scheme results in exponentially shorter proofs in comparison to the reflexive resolution path dependency scheme when used in the expansion DQBF system [Formula: see text]. On QBFs, we demonstrate that our new scheme is exponentially stronger than the reflexive resolution path dependency scheme when used in Q-resolution, thus resulting in the strongest QBF dependency scheme known to date.


title: SAT Heritage: A Community-Driven Effort for Archiving, Building and Running More Than Thousand SAT Solvers

text: SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. Moreover, there has been more than a thousand solvers published so far, some of them released in the early 90’s. If the SAT community wants to archive and be able to keep track of all the solvers that made its history, it urgently needs to deploy an important effort. We propose to initiate a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far. We rely on the best tools for archiving and building binaries (thanks to Docker, GitHub and Zenodo) and provide a consistent and easy way for this. Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.


title: Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator Networks

text: Incremental techniques have been widely used in solving problems reducible to SAT and MaxSAT instances. When an algorithm requires making subsequent runs of a SAT-solver on a slightly changing input formula, it is usually beneficial to change the strategy, so that the algorithm only operates on a single instance of a SAT-solver. One way to do this is via a mechanism called assumptions, which allows to accumulate and reuse knowledge from one iteration to the next and, in consequence, the provided input formula need not to be rebuilt during computation. In this paper we propose an encoding of a Pseudo-Boolean goal function that is based on sorting networks and can be provided to a SAT-solver only once. Then, during an optimization process, different bounds on the value of the function can be given to the solver by appropriate sets of assumptions. The experimental results show that the proposed technique is sound, that is, it increases the number of solved instances and reduces the average time and memory used by the solver on solved instances.