-
Quantum Graph-State Synthesis with SAT
Authors:
Sebastiaan Brand,
Tim Coopmans,
Alfons Laarman
Abstract:
In quantum computing and quantum information processing, graph states are a specific type of quantum states which are commonly used in quantum networking and quantum error correction. A recurring problem is finding a transformation from a given source graph state to a desired target graph state using only local operations. Recently it has been shown that deciding transformability is already NP-har…
▽ More
In quantum computing and quantum information processing, graph states are a specific type of quantum states which are commonly used in quantum networking and quantum error correction. A recurring problem is finding a transformation from a given source graph state to a desired target graph state using only local operations. Recently it has been shown that deciding transformability is already NP-hard. In this paper, we present a CNF encoding for both local and non-local graph state operations, corresponding to one- and two-qubit Clifford gates and single-qubit Pauli measurements. We use this encoding in a bounded-model-checking set-up to synthesize the desired transformation. For a completeness threshold, we provide an upper bound on the length of the transformation if it exists. We evaluate the approach in two settings: the first is the synthesis of the ubiquitous GHZ state from a random graph state where we can vary the number of qubits, while the second is based on a proposed 14 node quantum network. We find that the approach is able to synthesize transformations for graphs up to 17 qubits in under 30 minutes.
△ Less
Submitted 7 September, 2023;
originally announced September 2023.
-
A Decision Diagram Operation for Reachability
Authors:
Sebastiaan Brand,
Thomas Bäck,
Alfons Laarman
Abstract:
Saturation is considered the state-of-the-art method for computing fixpoints with decision diagrams. We present a relatively simple decision diagram operation called REACH that also computes fixpoints. In contrast to saturation, it does not require a partitioning of the transition relation. We give sequential algorithms implementing the new operation for both binary and multi-valued decision diagr…
▽ More
Saturation is considered the state-of-the-art method for computing fixpoints with decision diagrams. We present a relatively simple decision diagram operation called REACH that also computes fixpoints. In contrast to saturation, it does not require a partitioning of the transition relation. We give sequential algorithms implementing the new operation for both binary and multi-valued decision diagrams, and moreover provide parallel counterparts. We implement these algorithms and experimentally compare their performance against saturation on 692 model checking benchmarks in different languages. The results show that the REACH operation often outperforms saturation, especially on transition relations with low locality. In a comparison between parallelized versions of REACH and saturation we find that REACH obtains comparable speedups up to 16 cores, although falls behind saturation at 64 cores. Finally, in a comparison with the state-of-the-art model checking tool ITS-tools we find that REACH outperforms ITS-tools on 29% of models, suggesting that REACH can be useful as a complementary method in an ensemble tool.
△ Less
Submitted 7 December, 2022;
originally announced December 2022.
-
A computational framework for modelling infectious disease policy based on age and household structure with applications to the COVID-19 pandemic
Authors:
Joe Hilton,
Heather Riley,
Lorenzo Pellis,
Rabia Aziza,
Samuel P. C. Brand,
Ivy K. Kombe,
John Ojal,
Andrea Parisi,
Matt J. Keeling,
D. James Nokes,
Robert Manson-Sawko,
Thomas House
Abstract:
The widespread, and in many countries unprecedented, use of non-pharmaceutical interventions (NPIs) during the COVID-19 pandemic has highlighted the need for mathematical models which can estimate the impact of these measures while accounting for the highly heterogeneous risk profile of COVID-19. Models accounting either for age structure or the household structure necessary to explicitly model ma…
▽ More
The widespread, and in many countries unprecedented, use of non-pharmaceutical interventions (NPIs) during the COVID-19 pandemic has highlighted the need for mathematical models which can estimate the impact of these measures while accounting for the highly heterogeneous risk profile of COVID-19. Models accounting either for age structure or the household structure necessary to explicitly model many NPIs are commonly used in infectious disease modelling, but models incorporating both levels of structure present substantial computational and mathematical challenges due to their high dimensionality. Here we present a modelling framework for the spread of an epidemic that includes explicit representation of age structure and household structure. Our model is formulated in terms of tractable systems of ordinary differential equations for which we provide an open-source Python implementation. Such tractability leads to significant benefits for model calibration, exhaustive evaluation of possible parameter values, and interpretability of results. We demonstrate the flexibility of our model through four policy case studies, where we quantify the likely benefits of the following measures which were either considered or implemented in the UK during the current COVID-19 pandemic: control of within- and between-household mixing through NPIs; formation of support bubbles during lockdown periods; out-of-household isolation (OOHI); and temporary relaxation of NPIs during holiday periods. Our ordinary differential equation formulation and associated analysis demonstrate that multiple dimensions of risk stratification and social structure can be incorporated into infectious disease models without sacrificing mathematical tractability. This model and its software implementation expand the range of tools available to infectious disease policy analysts.
△ Less
Submitted 1 September, 2022; v1 submitted 14 January, 2022;
originally announced January 2022.
-
Improved analytical bounds on delivery times of long-distance entanglement
Authors:
Tim Coopmans,
Sebastiaan Brand,
David Elkouss
Abstract:
The ability to distribute high-quality entanglement between remote parties is a necessary primitive for many quantum communication applications. A large range of schemes for realizing the long-distance delivery of remote entanglement has been proposed, both for bipartite and multipartite entanglement. For assessing the viability of these schemes, knowledge of the time at which entanglement is deli…
▽ More
The ability to distribute high-quality entanglement between remote parties is a necessary primitive for many quantum communication applications. A large range of schemes for realizing the long-distance delivery of remote entanglement has been proposed, both for bipartite and multipartite entanglement. For assessing the viability of these schemes, knowledge of the time at which entanglement is delivered is crucial. Specifically, if the communication task requires multiple remote-entangled quantum states and these states are generated at different times by the scheme, the earlier states will need to wait and thus their quality will decrease while being stored in an (imperfect) memory. For the remote-entanglement delivery schemes which are closest to experimental reach, this time assessment is challenging, as they consist of nondeterministic components such as probabilistic entanglement swaps. For many such protocols even the average time at which entanglement can be distributed is not known exactly, in particular when they consist of feedback loops and forced restarts. In this work, we provide improved analytical bounds on the average and on the quantiles of the completion time of entanglement distribution protocols in the case that all network components have success probabilities lower bounded by a constant. A canonical example of such a protocol is a nested quantum repeater scheme which consists of heralded entanglement generation and entanglement swaps. For this scheme specifically, our results imply that a common approximation to the mean entanglement distribution time, the 3-over-2 formula, is in essence an upper bound to the real time. Our results rely on a novel connection with reliability theory.
△ Less
Submitted 8 February, 2022; v1 submitted 21 March, 2021;
originally announced March 2021.
-
Hybrid divide-and-conquer approach for tree search algorithms
Authors:
Mathys Rennela,
Sebastiaan Brand,
Alfons Laarman,
Vedran Dunjko
Abstract:
One of the challenges of quantum computers in the near- and mid- term is the limited number of qubits we can use for computations. Finding methods that achieve useful quantum improvements under size limitations is thus a key question in the field. In this vein, it was recently shown that a hybrid classical-quantum method can help provide polynomial speed-ups to classical divide-and-conquer algorit…
▽ More
One of the challenges of quantum computers in the near- and mid- term is the limited number of qubits we can use for computations. Finding methods that achieve useful quantum improvements under size limitations is thus a key question in the field. In this vein, it was recently shown that a hybrid classical-quantum method can help provide polynomial speed-ups to classical divide-and-conquer algorithms, even when only given access to a quantum computer much smaller than the problem itself. In this work, we study the hybrid divide-and-conquer method in the context of tree search algorithms, and extend it by including quantum backtracking, which allows better results than previous Grover-based methods. Further, we provide general criteria for polynomial speed-ups in the tree search context, and provide a number of examples where polynomial speed ups, using arbitrarily smaller quantum computers, can be obtained. We provide conditions for speedups for the well known algorithm of DPLL, and we prove threshold-free speed-ups for the PPSZ algorithm (the core of the fastest exact Boolean satisfiability solver) for well-behaved classes of formulas. We also provide a simple example where speed-ups can be obtained in an algorithm-independent fashion, under certain well-studied complexity-theoretical assumptions. Finally, we briefly discuss the fundamental limitations of hybrid methods in providing speed-ups for larger problems.
△ Less
Submitted 20 March, 2023; v1 submitted 14 July, 2020;
originally announced July 2020.
-
Efficient computation of the waiting time and fidelity in quantum repeater chains
Authors:
Sebastiaan Brand,
Tim Coopmans,
David Elkouss
Abstract:
Quantum communication enables a host of applications that cannot be achieved by classical communication means, with provably secure communication as one of the prime examples. The distance that quantum communication schemes can cover via direct communication is fundamentally limited by losses on the communication channel. By means of quantum repeaters, the reach of these schemes can be extended an…
▽ More
Quantum communication enables a host of applications that cannot be achieved by classical communication means, with provably secure communication as one of the prime examples. The distance that quantum communication schemes can cover via direct communication is fundamentally limited by losses on the communication channel. By means of quantum repeaters, the reach of these schemes can be extended and chains of quantum repeaters could in principle cover arbitrarily long distances. In this work, we provide two efficient algorithms for determining the generation time and fidelity of the first generated entangled pair between the end nodes of a quantum repeater chain. The runtime of the algorithms increases polynomially with the number of segments of the chain, which improves upon the exponential runtime of existing algorithms. Our first algorithm is probabilistic and can analyze refined versions of repeater chain protocols which include intermediate entanglement distillation. Our second algorithm computes the waiting time distribution up to a pre-specified truncation time, has faster runtime than the first one and is moreover exact up to machine precision. Using our proof-of-principle implementation, we are able to analyze repeater chains of thousands of segments for some parameter regimes. The algorithms thus serve as useful tools for the analysis of large quantum repeater chain protocols and topologies of the future quantum internet.
△ Less
Submitted 16 December, 2019;
originally announced December 2019.
-
Relation Variables in Qualitative Spatial Reasoning
Authors:
Sebastian Brand
Abstract:
We study an alternative to the prevailing approach to modelling qualitative spatial reasoning (QSR) problems as constraint satisfaction problems. In the standard approach, a relation between objects is a constraint whereas in the alternative approach it is a variable. The relation-variable approach greatly simplifies integration and implementation of QSR. To substantiate this point, we discuss s…
▽ More
We study an alternative to the prevailing approach to modelling qualitative spatial reasoning (QSR) problems as constraint satisfaction problems. In the standard approach, a relation between objects is a constraint whereas in the alternative approach it is a variable. The relation-variable approach greatly simplifies integration and implementation of QSR. To substantiate this point, we discuss several QSR algorithms from the literature which in the relation-variable approach reduce to the customary constraint propagation algorithm enforcing generalised arc-consistency.
△ Less
Submitted 2 August, 2006;
originally announced August 2006.
-
Infinite Qualitative Simulations by Means of Constraint Programming
Authors:
Krzysztof R. Apt,
Sebastian Brand
Abstract:
We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define the simulations, we combine constraints that formalize the background knowledge concerned with qualitative reasoning with appropriate inter-state constraints that are formulated usin…
▽ More
We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define the simulations, we combine constraints that formalize the background knowledge concerned with qualitative reasoning with appropriate inter-state constraints that are formulated using linear temporal logic. We implemented this approach in a constraint programming system by drawing on ideas from bounded model checking. The resulting system allows us to test and modify the problem specifications in a straightforward way and to combine various knowledge aspects.
△ Less
Submitted 2 August, 2006;
originally announced August 2006.
-
ACD Term Rewriting
Authors:
Gregory J. Duck,
Peter J. Stuckey,
Sebastian Brand
Abstract:
We introduce Associative Commutative Distributive Term Rewriting (ACDTR), a rewriting language for rewriting logical formulae. ACDTR extends AC term rewriting by adding distribution of conjunction over other operators. Conjunction is vital for expressive term rewriting systems since it allows us to require that multiple conditions hold for a term rewriting rule to be used. ACDTR uses the notion…
▽ More
We introduce Associative Commutative Distributive Term Rewriting (ACDTR), a rewriting language for rewriting logical formulae. ACDTR extends AC term rewriting by adding distribution of conjunction over other operators. Conjunction is vital for expressive term rewriting systems since it allows us to require that multiple conditions hold for a term rewriting rule to be used. ACDTR uses the notion of a "conjunctive context", which is the conjunction of constraints that must hold in the context of a term, to enable the programmer to write very expressive and targeted rewriting rules. ACDTR can be seen as a general logic programming language that extends Constraint Handling Rules and AC term rewriting. In this paper we define the semantics of ACDTR and describe our prototype implementation.
△ Less
Submitted 2 August, 2006;
originally announced August 2006.
-
Towards "Propagation = Logic + Control"
Authors:
Sebastian Brand,
Roland H. C. Yap
Abstract:
Constraint propagation algorithms implement logical inference. For efficiency, it is essential to control whether and in what order basic inference steps are taken. We provide a high-level framework that clearly differentiates between information needed for controlling propagation versus that needed for the logical semantics of complex constraints composed from primitive ones. We argue for the a…
▽ More
Constraint propagation algorithms implement logical inference. For efficiency, it is essential to control whether and in what order basic inference steps are taken. We provide a high-level framework that clearly differentiates between information needed for controlling propagation versus that needed for the logical semantics of complex constraints composed from primitive ones. We argue for the appropriateness of our controlled propagation framework by showing that it captures the underlying principles of manually designed propagation algorithms, such as literal watching for unit clause propagation and the lexicographic ordering constraint. We provide an implementation and benchmark results that demonstrate the practicality and efficiency of our framework.
△ Less
Submitted 2 August, 2006;
originally announced August 2006.
-
Constraint-Based Qualitative Simulation
Authors:
Krzysztof R. Apt,
Sebastian Brand
Abstract:
We consider qualitative simulation involving a finite set of qualitative relations in presence of complete knowledge about their interrelationship. We show how it can be naturally captured by means of constraints expressed in temporal logic and constraint satisfaction problems. The constraints relate at each stage the 'past' of a simulation with its 'future'. The benefit of this approach is that…
▽ More
We consider qualitative simulation involving a finite set of qualitative relations in presence of complete knowledge about their interrelationship. We show how it can be naturally captured by means of constraints expressed in temporal logic and constraint satisfaction problems. The constraints relate at each stage the 'past' of a simulation with its 'future'. The benefit of this approach is that it readily leads to an implementation based on constraint technology that can be used to generate simulations and to answer queries about them.
△ Less
Submitted 7 April, 2005;
originally announced April 2005.
-
Schedulers and Redundancy for a Class of Constraint Propagation Rules
Authors:
Sebastian Brand,
Krzysztof R. Apt
Abstract:
We study here schedulers for a class of rules that naturally arise in the context of rule-based constraint programming. We systematically derive a scheduler for them from a generic iteration algorithm of [Apt 2000]. We apply this study to so-called membership rules of [Apt and Monfroy 2001]. This leads to an implementation that yields a considerably better performance for these rules than their…
▽ More
We study here schedulers for a class of rules that naturally arise in the context of rule-based constraint programming. We systematically derive a scheduler for them from a generic iteration algorithm of [Apt 2000]. We apply this study to so-called membership rules of [Apt and Monfroy 2001]. This leads to an implementation that yields a considerably better performance for these rules than their execution as standard CHR rules. Finally, we show how redundant rules can be identified and how appropriately reduced sets of rules can be computed.
△ Less
Submitted 2 November, 2004; v1 submitted 23 March, 2004;
originally announced March 2004.
-
Schedulers for Rule-based Constraint Programming
Authors:
Krzysztof R. Apt,
Sebastian Brand
Abstract:
We study here schedulers for a class of rules that naturally arise in the context of rule-based constraint programming. We systematically derive a scheduler for them from a generic iteration algorithm of Apt [2000]. We apply this study to so-called membership rules of Apt and Monfroy [2001]. This leads to an implementation that yields for these rules a considerably better performance than their…
▽ More
We study here schedulers for a class of rules that naturally arise in the context of rule-based constraint programming. We systematically derive a scheduler for them from a generic iteration algorithm of Apt [2000]. We apply this study to so-called membership rules of Apt and Monfroy [2001]. This leads to an implementation that yields for these rules a considerably better performance than their execution as standard CHR rules.
△ Less
Submitted 15 November, 2002;
originally announced November 2002.
-
Proceedings of the 6th Annual Workshop of the ERCIM Working Group on Constraints
Authors:
Krzysztof R. Apt,
Roman Bartak,
Eric Monfroy,
Francesca Rossi,
Sebastian Brand
Abstract:
Homepage of the workshop proceedings, with links to all individually archived papers
Homepage of the workshop proceedings, with links to all individually archived papers
△ Less
Submitted 3 October, 2001;
originally announced October 2001.
-
Constraint Propagation in Presence of Arrays
Authors:
Sebastian Brand
Abstract:
We describe the use of array expressions as constraints, which represents a consequent generalisation of the "element" constraint. Constraint propagation for array constraints is studied theoretically, and for a set of domain reduction rules the local consistency they enforce, arc-consistency, is proved. An efficient algorithm is described that encapsulates the rule set and so inherits the capab…
▽ More
We describe the use of array expressions as constraints, which represents a consequent generalisation of the "element" constraint. Constraint propagation for array constraints is studied theoretically, and for a set of domain reduction rules the local consistency they enforce, arc-consistency, is proved. An efficient algorithm is described that encapsulates the rule set and so inherits the capability to enforce arc-consistency from the rules.
△ Less
Submitted 14 May, 2001;
originally announced May 2001.