arXiv subjects

Martin Suda

Publications and source records attributed to Martin Suda.

35 records · Page 2Linked to original sources

arXiv2019

Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements

These are the post-proceedings of the second ARCADE workshop, which took place on the 26th August 2019 in Natal, Brazil, colocated with CADE-27. ARCADE stands for Automated Reasoning: Challenges, Applications, Directions, Exemplary achievements. The goal of this workshop was to bring together key people from various sub-communities of automated reasoning--such as SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for description logic, arithmetic, set theory), interactive theorem proving---to discuss the present, past, and future of the field.

cs.LO↗

arXiv2019

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

We describe an efficient implementation of clause guidance in saturation-based automated theorem provers extending the ENIGMA approach. Unlike in the first ENIGMA implementation where fast linear classifier is trained and used together with manually engineered features, we have started to experiment with more sophisticated state-of-the-art machine learning methods such as gradient boosted trees and recursive neural networks. In particular the latter approach poses challenges in terms of efficiency of clause evaluation, however, we show that deep integration of the neural evaluation with the ATP data-structures can largely amortize this cost and lead to competitive real-time results. Both methods are evaluated on a large dataset of theorem proving problems and compared with the previous approaches. The resulting methods improve on the manually designed clause guidance, providing the first practically convincing application of gradient-boosted and neural clause guidance in saturation-style automated theorem provers.

cs.AI↗

arXiv2019

Dirac monopoles and the importance of the usage of appropriate degrees of freedom

We discuss that the singularities appearing in Dirac's formulation of magnetic monopoles are due to the set of fields which he used and not due to the physical properties of magnetic monopoles. We explain in detail that we can find the same algebraic expressions and singularities for the affine connections on the sphere $S^2$, which Dirac found for the U(1) gauge field of magnetic monopoles. Since spheres have no singularities, it is obvious, that these singularities are due to the set of fields which are used to describe the geometry of $S^2$. As there are descriptions of the geometry of spheres without any singularities, we indicate that it would be preferable to use singularity free descriptions of magnetic and also electric monopoles.

physics.gen-ph↗

arXiv2017

Influence of gravitational waves on circular moving particles

We investigate the influence of a gravitational wave background on particles in circular motion. We are especially interested in waves leading to stationary orbits. This consideration is limited to circular orbits perpendicular to the incidence direction. As a main result of our calculation we obtain in addition to the well-known alteration of the radial distance a time dependent correction term for the phase modifying the circular motion of the particle. A background of gravitational waves creates some kind of uncertainty.

gr-qc↗

arXiv2017

Splitting Proofs for Interpolation

We study interpolant extraction from local first-order refutations. We present a new theoretical perspective on interpolation based on clearly separating the condition on logical strength of the formula from the requirement on the com- mon signature. This allows us to highlight the space of all interpolants that can be extracted from a refutation as a space of simple choices on how to split the refuta- tion into two parts. We use this new insight to develop an algorithm for extracting interpolants which are linear in the size of the input refutation and can be further optimized using metrics such as number of non-logical symbols or quantifiers. We implemented the new algorithm in first-order theorem prover VAMPIRE and evaluated it on a large number of examples coming from the first-order proving community. Our experiments give practical evidence that our work improves the state-of-the-art in first-order interpolation.

cs.LO↗

arXiv2017

Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)

This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover Vampire. We describe the techniques we currently employ to ensure that Vampire is correct and use this to motivate future challenges that need to be addressed to make this process more straightforward and to achieve better correctness guarantees.

cs.LO↗

arXiv2017

Blocked Clauses in First-Order Logic

Blocked clauses provide the basis for powerful reasoning techniques used in SAT, QBF, and DQBF solving. Their definition, which relies on a simple syntactic criterion, guarantees that they are both redundant and easy to find. In this paper, we lift the notion of blocked clauses to first-order logic. We introduce two types of blocked clauses, one for first-order logic with equality and the other for first-order logic without equality, and prove their redundancy. In addition, we give a polynomial algorithm for checking whether a clause is blocked. Based on our new notions of blocking, we implemented a novel first-order preprocessing tool. Our experiments showed that many first-order problems in the TPTP library contain a large number of blocked clauses. Moreover, we observed that their elimination can improve the performance of modern theorem provers, especially on satisfiable problem instances.

cs.LO↗

arXiv2016

Finding Finite Models in Multi-Sorted First Order Logic

This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and encodes the related ground problem as a SAT problem. When moving to the multi-sorted setting each sort may have a different domain size, leading to an explosion in the search space. This paper focusses on methods to tame that search space. The key approach adds additional information to the SAT encoding to suggest which domains should be grown. Evaluation of an implementation of techniques in the Vampire theorem prover shows that they dramatically reduce the search space and that this is an effective approach to find finite models in multi-sorted first order logic.

cs.LO↗

arXiv2016

Selecting the Selection

Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections and term orderings to tame the growth of the search space and help steer proof search. This paper introduces the notion of lookahead selection that estimates (looks ahead) the effect on the search space of selecting a literal. There is also a case made for the use of incomplete selection functions that attempt to restrict the search space instead of satisfying some completeness criteria. Experimental evaluation in the \Vampire\ theorem prover shows that both lookahead selection and incomplete selection significantly contribute to solving hard problems unsolvable by other methods.

cs.AI↗

arXiv2016

Lifting QBF Resolution Calculi to DQBF

We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the strict chain of proof systems Q-Resolution < IR-calc < IRM-calc, the situation is quite different in DQBF. Q-Resolution and likewise universal Resolution are too weak: they are not complete. IR-calc has the right strength: it is sound and complete. IRM-calc is too strong: it is not sound any more, and the same applies to long-distance Resolution. Conceptually, we use the relation of DQBF to EPR and explain our new DQBF calculus based on IR-calc as a subsystem of FO-Resolution.

cs.LO↗

arXiv2013

Variable and clause elimination for LTL satisfiability checking

We study preprocessing techniques for clause normal forms of LTL formulas. Applying the mechanism of labelled clauses enables us to reinterpret LTL satisfiability as a set of purely propositional problems and thus to transfer simplification ideas from SAT to LTL. We demonstrate this by adapting variable and clause elimination, a very effective preprocessing technique used by modern SAT solvers. Our experiments confirm that even in the temporal setting substantial reductions in formula size and subsequent decrease of solver runtime can be achieved.

cs.LO↗

arXiv2013

On the Optimality of Basis Transformations to Secure Entanglement Swapping Based QKD Protocols

In this article, we discuss the optimality of basis transformations as a security measure for quantum key distribution protocols based on entanglement swapping. To estimate the security, we focus on the information an adversary obtains on the raw key bits from a generic version of a collective attack strategy. In the scenario described in this article, the application of general basis transformations serving as a counter measure by one or both legitimate parties is analyzed. In this context, we show that the angles, which describe these basis transformations can be optimized compared to the application of a Hadamard operation, which is the standard basis transformation recurrently found in literature. As a main result, we show that the adversary's information can be reduced to an amount of approximately 0.20752 when using a single basis transformation and to an amount of approximately 0.0548 when combining two different basis transformations. This is less than half the information compared to other protocols using a Hadamard operation and thus represents an advantage regarding the security of entanglement swapping based protocols.

quant-ph↗

arXiv2013

Triggered Clause Pushing for IC3

We propose an improvement of the famous IC3 algorithm for model checking safety properties of finite state systems. We collect models computed by the SAT-solver during the clause propagation phase of the algorithm and use them as witnesses for why the respective clauses could not be pushed forward. It only makes sense to recheck a particular clause for pushing when its witnessing model falsifies a newly added clause. Since this trigger test is both computationally cheap and sufficiently precise, we can afford to keep clauses pushed as far as possible at all times. Experiments indicate that this strategy considerably improves IC3's performance.

cs.LO↗

arXiv2013

Duality in STRIPS planning

We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa. The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

cs.AI↗

arXiv2011

Conjugate Variables as a Resource in Signal and Image Processing

In this paper we develop a new technique to model joint distributions of signals. Our technique is based on quantum mechanical conjugate variables. We show that the transition probability of quantum states leads to a distance function on the signals. This distance function obeys the triangle inequality on all quantum states and becomes a metric on pure quantum states. Treating signals as conjugate variables allows us to create a new approach to segment them. Keywords: Quantum information, transition probability, Euclidean distance, Fubini-study metric, Bhattacharyya coefficients, conjugate variable, signal/sensor fusion, signal and image segmentation.

cs.CV↗

arXiv2011

Quantum Interference between a Single-Photon Fock State and a Coherent State

We derive analytical expressions for the single mode quantum field state at the individual output ports of a beam splitter when a single-photon Fock state and a coherent state are incident on the input ports. The output states turn out to be a statistical mixture between a displaced Fock state and a coherent state. Consequently we are able to find an analytical expression for the corresponding Wigner function. Because of the generality of our calculations the obtained results are valid for all passive and lossless optical four port devices. We show further how the results can be adapted to the case of the Mach-Zehnder interferometer. In addition we consider the case for which the single-photon Fock state is replaced with a general input state: a coherent input state displaces each general quantum state at the output port of a beam splitter with the displacement parameter being the amplitude of the coherent state.

quant-ph↗

arXiv2008

A Novel Attack Strategy on Entanglement Swapping QKD Protocols

Li et al. presented a protocol [Int. Journal of Quantum Information, Vol. 4, No. 6 (2006) 899-906] for quantum key distribution based on entanglement swapping. In this protocol they use random and certain bits to construct a classical key and they claim that this key is secure. In our article we show that the protocol by Li et al. is insecure presenting a new type of attack strategy which gives an adversary full information about the key without being detected. This strategy is based on entanglement swapping, too, and manages to preserve the correlation between the measurement results of the legitimate parties. Further we present a modified version of the protocol and show that it is secure against this new attack strategy.

quant-ph↗