scholarly journals A Logic of Directions

Author(s):  
Heshan Du ◽  
Natasha Alechina ◽  
Anthony G. Cohn

We propose a logic of directions for points (LD) over 2D Euclidean space, which formalises primary direction relations east (E), west (W), and indeterminate east/west (Iew), north (N), south (S) and indeterminate north/south (Ins). We provide a sound and complete axiomatisation of it, and prove that its satisfiability problem is NP-complete.

1997 ◽  
Vol 6 ◽  
pp. 211-221 ◽  
Author(s):  
T. Drakengren ◽  
P. Jonsson

We investigate the computational properties of the spatial algebra RCC-5 which is a restricted version of the RCC framework for spatial reasoning. The satisfiability problem for RCC-5 is known to be NP-complete but not much is known about its approximately four billion subclasses. We provide a complete classification of satisfiability for all these subclasses into polynomial and NP-complete respectively. In the process, we identify all maximal tractable subalgebras which are four in total.


2019 ◽  
Vol 29 (8) ◽  
pp. 1139-1184 ◽  
Author(s):  
Stéphane Demri ◽  
Raul Fervari

Abstract We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, obtaining surprising results by design of proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with $\Diamond $, the difference modality $\langle \neq \rangle $ and separating conjunction $\ast $ is shown Tower-complete whereas the restriction either to $\Diamond $ and $\ast $ or to $\langle \neq \rangle $ and $\ast $ is only NP-complete. We establish that the full logic MSL admits an undecidable satisfiability problem. Furthermore, we investigate variants of MSL with alternative semantics and we build bridges with interval temporal logics and with logics equipped with sabotage operators.


2000 ◽  
Vol 11 (01) ◽  
pp. 29-63
Author(s):  
MARTIN MÜLLER ◽  
SUSUMU NISHIMURA

We present a constraint system, OF, of feature trees that is appropriate to specify and implement type inference for first-class messages. OF extends traditional systems of feature constraints by a selection constraint x <y> z, "by first-class feature tree" y, which is in contrast to the standard selection constraint x[f]y, "by fixed feature" f. We investigate the satisfiability problem of OF and show that it can be solved in polynomial time, and even in quadratic time if the number of features is bounded. We compare OF with Treinen's system EF of feature constraints with first-class features, which has an NP-complete satisfiability problem. This comparison yields that the satisfiability problem for OF with negation is NP-hard. Further we obtain NP-completeness, for a specific subclass of OF with negation that is useful for a related type inference problem. Based on OF we give a simple account of type inference for first-class messages in the spirit of Nishimura's recent proposal, and we show that it has polynomial time complexity: We also highlight an immediate extension of this type system that appears to be desirable but makes type inference NP-complete.


2002 ◽  
Vol 09 (02) ◽  
pp. 115-123
Author(s):  
Miroljub Dugić

We analyze the Ohya-Masuda quantum algorithm that solves the so-called “satisfiability” problem, which is an NP-complete problem of the complexity theory. We distinguish three steps in the algorithm, and analyze the second step, in which a coherent superposition of states (a “pure” state) transforms into an “incoherent” mixture presented by a density matrix. We show that, if “nonideal” (in analogy with “nonideal” quantum measurement), this transformation can make the algorithm to fail in some cases. On this basis we give some general notions on the physical implementation of the Ohya-Masuda algorithm.


2008 ◽  
Vol 14 (1) ◽  
pp. 1-28 ◽  
Author(s):  
Ian Pratt-Hartmann

AbstractThe numerically definite syllogistic is the fragment of English obtained by extending the language of the classical syllogism with numerical quantifiers. The numerically definite relational syllogistic is the fragment of English obtained by extending the numerically definite syllogistic with predicates involving transitive verbs. This paper investigates the computational complexity of the satisfiability problem for these fragments. We show that the satisfiability problem (= finite satisfiability problem) for the numerically definite syllogistic is strongly NP-complete, and that the satisfiability problem (= finite satisfiability problem) for the numerically definite relational syllogistic is NEXPTIME-complete, but perhaps not strongly so. We discuss the related problem of probabilistic (propositional) satisfiability, and thereby demonstrate the incompleteness of some proof-systems that have been proposed for the numerically definite syllogistic.


2016 ◽  
Vol 56 ◽  
pp. 403-428 ◽  
Author(s):  
Xiaowang Zhang ◽  
Jan Van den Bussche ◽  
François Picalausa

The satisfiability problem for SPARQL 1.0 patterns is undecidable in general, since the relational algebra can be emulated using such patterns. The goal of this paper is to delineate the boundary of decidability of satisfiability in terms of the constraints allowed in filter conditions. The classes of constraints considered are bound-constraints, negated bound- constraints, equalities, nonequalities, constant-equalities, and constant-nonequalities. The main result of the paper can be summarized by saying that, as soon as inconsistent filter conditions can be formed, satisfiability is undecidable. The key insight in each case is to find a way to emulate the set difference operation. Undecidability can then be obtained from a known undecidability result for the algebra of binary relations with union, composition, and set difference. When no inconsistent filter conditions can be formed, satisfiability is decidable by syntactic checks on bound variables and on the use of literals. Although the problem is shown to be NP-complete, it is experimentally shown that the checks can be implemented efficiently in practice. The paper also points out that satisfiability for the so-called ‘well-designed’ patterns can be decided by a check on bound variables and a check for inconsistent filter conditions.


Author(s):  
Zhixiang Yin ◽  
Jing Yang ◽  
Qiang Zhang ◽  
Zhen Tang ◽  
Guoqiang Wang ◽  
...  

Satisfiability problem is a famous nondeterministic polynomial-time complete (NP-complete) problem, which has always been a hotspot in artificial intelligence. In this paper, by combining the advantages of DNA origami with hybridization chain reaction, a computing model was proposed to solve the satisfiability problem. For each clause in the given formula, a DNA origami device was devised. The device corresponding to the clause was capable of searching for assignments that satisfied the clause. When all devices completed the search in parallel, the intersection of these satisfying assignments found must satisfy all the clauses. Therefore, whether the given formula is satisfiable or not was decided. The simulation results demonstrated that the proposed computing model was feasible. Our work showed the capability of DNA origami in architecting automatic computing device. The paper proposed a novel method for designing functional nanoscale devices based on DNA origami.


1982 ◽  
Vol 34 (3) ◽  
pp. 519-524 ◽  
Author(s):  
Svatopluk Poljak ◽  
Daniel Turzík

Let G be a symmetric connected graph without loops. Denote by b(G) the maximum number of edges in a bipartite subgraph of G. Determination of b(G) is polynomial for planar graphs ([6], [8]); in general it is an NP-complete problem ([5]). Edwards in [1], [2] found some estimates of b(G) which give, in particular,for a connected graph G of n vertices and m edges, whereand ﹛x﹜ denotes the smallest integer ≧ x.We give an 0(V3) algorithm which for a given graph constructs a bipartite subgraph B with at least f(m, n) edges, yielding a short proof of Edwards’ result.Further, we consider similar methods for obtaining some estimates for a particular case of the satisfiability problem. Let Φ be a Boolean formula of variables x1, …, xn.


2013 ◽  
Vol 683 ◽  
pp. 909-912 ◽  
Author(s):  
Anna Gorbenko ◽  
Vladimir Popov

In this paper, we propose a system of scenarios creation for self-learning of intelligent mobile robots. This model is based on the model of Hamiltonian path with fixed number of color repetitions for c-arc-colored digraphs. We show that the problem of Hamiltonian path with fixed number of color repetitions for c-arc-colored digraphs is NP-complete. We consider an approach to solve the problem. This approach is based on an explicit reduction from the problem to the satisfiability problem.


1984 ◽  
Vol 8 (1) ◽  
pp. 85-89 ◽  
Author(s):  
Craig A. Tovey

Sign in / Sign up

Export Citation Format

Share Document