On the Exact Complexity of Evaluating Quantified k -CNF

We relate the exponential complexities 2 ^s(k)n of $\textsc {$k$-sat}$ and the exponential complexity $2^{s(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf}))n}$ of $\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})$ (the problem of evaluating quantified formulas of the form $\forall\vec{x} \exists\vec{y} \textsc {F}(\vec {x},\vec{y})$ where F is a 3-cnf in $\vec{x}$ variables and $\vec{y}$ variables) and show that s(∞) (the limit of s(k) as k→∞) is at most $s(\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf}))$ . Therefore, if we assume the Strong Exponential-Time Hypothesis, then there is no algorithm for $\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})$ running in time 2 ^cn with c<1. On the other hand, a nontrivial exponential-time algorithm for $\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})$ would provide a $\textsc {$k$-sat}$ solver with better exponent than all current algorithms for sufficiently large k. We also show several syntactic restrictions of the evaluation problem $\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})$ have nontrivial algorithms, and provide strong evidence that the hardest cases of $\textsc {eval}(\mathrm {\varPi }_{2} 3\textsc {-cnf})$ must have a mixture of clauses of two types: one universally quantified literal and two existentially quantified literals, or only existentially quantified literals. Moreover, the hardest cases must have at least n?o(n) universally quantified variables, and hence only o(n) existentially quantified variables. Our proofs involve the construction of efficient minimally unsatisfiable $\textsc {$k$-cnf}$ s and the application of the Sparsification lemma.     

On matrices, automata, and double counting in constraint programming

Matrix models are ubiquitous for constraint problems. Many such problems have a matrix of variables $\mathcal{M}$ , with the same constraint C defined by a finite-state automaton $\mathcal{A}$ on each row of $\mathcal{M}$ and a global cardinality constraint $\mathit{gcc}$ on each column of $\mathcal{M}$ . We give two methods for deriving, by double counting, necessary conditions on the cardinality variables of the $\mathit{gcc}$ constraints from the automaton $\mathcal{A}$ . The first method yields linear necessary conditions and simple arithmetic constraints. The second method introduces the cardinality automaton, which abstracts the overall behaviour of all the row automata and can be encoded by a set of linear constraints. We also provide a domain consistency filtering algorithm for the conjunction of lexicographic ordering constraints between adjacent rows of $\mathcal{M}$ and (possibly different) automaton constraints on the rows. We evaluate the impact of our methods in terms of runtime and search effort on a large set of nurse rostering problem instances.     

Arithmetizing Classes Around \textsf{NC} 1 and \textsf{L}

The parallel complexity class $\textsf{NC}$ ¹ has many equivalent models such as polynomial size formulae and bounded width branching programs. Caussinus et al. (J. Comput. Syst. Sci. 57:200–212, 1992) considered arithmetizations of two of these classes, $\textsf{\#NC}$ ¹ and $\textsf{\#BWBP}$ . We further this study to include arithmetization of other classes. In particular, we show that counting paths in branching programs over visibly pushdown automata is in $\textsf{FLogDCFL}$ , while counting proof-trees in logarithmic width formulae has the same power as $\textsf{\#NC}$ ¹. We also consider polynomial-degree restrictions of $\textsf{SC}$ ⁱ , denoted $\textsf{sSC}$ ⁱ , and show that the Boolean class $\textsf{sSC}$ ¹ is sandwiched between $\textsf{NC}$ ¹ and $\textsf{L}$ , whereas $\textsf{sSC}$ ⁰ equals $\textsf{NC}$ ¹. On the other hand, the arithmetic class $\textsf{\#sSC}$ ⁰ contains $\textsf{\#BWBP}$ and is contained in $\textsf{FL}$ , and $\textsf{\#sSC}$ ¹ contains $\textsf{\#NC}$ ¹ and is in $\textsf{SC}$ ². We also investigate some closure properties of the newly defined arithmetic classes.     

Rounds in Combinatorial Search

A set system $\mathcal{H} \subseteq2^{[m]}$ is said to be separating if for every pair of distinct elements x,y∈[m] there exists a set $H\in\mathcal{H}$ such that H contains exactly one of them. The search complexity of a separating system $\mathcal{H} \subseteq 2^{[m]}$ is the minimum number of questions of type “x∈H?” (where $H \in\mathcal{H}$ ) needed in the worst case to determine a hidden element x∈[m]. If we receive the answer before asking a new question then we speak of the adaptive complexity, denoted by $\mathrm{c} (\mathcal{H})$ ; if the questions are all fixed beforehand then we speak of the non-adaptive complexity, denoted by $\mathrm{c}_{na} (\mathcal{H})$ . If we are allowed to ask the questions in at most k rounds then we speak of the k-round complexity of $\mathcal{H}$ , denoted by $\mathrm{c}_{k} (\mathcal{H})$ . It is clear that $|\mathcal{H}| \geq\mathrm{c}_{na} (\mathcal{H}) = \mathrm{c}_{1} (\mathcal{H}) \geq\mathrm{c}_{2} (\mathcal{H}) \geq\cdots\geq\mathrm{c}_{m} (\mathcal{H}) = \mathrm{c} (\mathcal{H})$ . A group of problems raised by G.O.H. Katona is to characterize those separating systems for which some of these inequalities are tight. In this paper we are discussing set systems $\mathcal{H}$ with the property $|\mathcal{H}| = \mathrm{c}_{k} (\mathcal{H}) $ for any k≥3. We give a necessary condition for this property by proving a theorem about traces of hypergraphs which also has its own interest.     

On reducing factorization to the discrete logarithm problem modulo a composite

The discrete logarithm problem modulo a composite??abbreviate it as DLPC??is the following: given a (possibly) composite integer n??? 1 and elements ${a, b \in \mathbb{Z}_n^*}$ , determine an ${x \in \mathbb{N}}$ satisfying a ^x ?=?b if one exists. The question whether integer factoring can be reduced in deterministic polynomial time to the DLPC remains open. In this paper we consider the problem ${{\rm DLPC}_\varepsilon}$ obtained by adding in the DLPC the constraint ${x\le (1-\varepsilon)n}$ , where ${\varepsilon}$ is an arbitrary fixed number, ${0 < \varepsilon\le\frac{1}{2}}$ . We prove that factoring n reduces in deterministic subexponential time to the ${{\rm DLPC}_\varepsilon}$ with ${O_\varepsilon((\ln n)^2)}$ queries for moduli less or equal to n.     

The Rank-Width of Edge-Coloured Graphs

A C-coloured graph is a graph, that is possibly directed, where the edges are coloured with colours from the set C. Clique-width is a complexity measure for C-coloured graphs, for finite sets C. Rank-width is an equivalent complexity measure for undirected graphs and has good algorithmic and structural properties. It is in particular related to the vertex-minor relation. We discuss some possible extensions of the notion of rank-width to C-coloured graphs. There is not a unique natural notion of rank-width for C-coloured graphs. We define two notions of rank-width for them, both based on a coding of C-coloured graphs by ${\mathbb{F}}^{*}$ -graphs— $\mathbb {F}$ -coloured graphs where each edge has exactly one colour from $\mathbb{F}\setminus \{0\},\ \mathbb{F}$ a field—and named respectively $\mathbb{F}$ -rank-width and $\mathbb {F}$ -bi-rank-width. The two notions are equivalent to clique-width. We then present a notion of vertex-minor for $\mathbb{F}^{*}$ -graphs and prove that $\mathbb{F}^{*}$ -graphs of bounded $\mathbb{F}$ -rank-width are characterised by a list of $\mathbb{F}^{*}$ -graphs to exclude as vertex-minors (this list is finite if $\mathbb{F}$ is finite). An algorithm that decides in time O(n ³) whether an $\mathbb{F}^{*}$ -graph with n vertices has $\mathbb{F}$ -rank-width (resp. $\mathbb{F}$ -bi-rank-width) at most k, for fixed k and fixed finite field $\mathbb{F}$ , is also given. Graph operations to check MSOL-definable properties on $\mathbb{F}^{*}$ -graphs of bounded $\mathbb{F}$ -rank-width (resp. $\mathbb{F}$ -bi-rank-width) are presented. A specialisation of all these notions to graphs without edge colours is presented, which shows that our results generalise the ones in undirected graphs.     

A note on reverse scheduling with maximum lateness objective

The inverse and reverse counterparts of the single-machine scheduling problem $1||L_{\max }$ are studied in [2], in which the complexity classification is provided for various combinations of adjustable parameters (due dates and processing times) and for five different types of norm: $\ell _{1},\ell _{2},\ell _{\infty },\ell _{H}^{\Sigma } $ , and $\ell _{H}^{\max }$ . It appears that the $O(n^{2})$ -time algorithm for the reverse problem with adjustable due dates contains a flaw. In this note, we present the structural properties of the reverse model, establishing a link with the forward scheduling problem with due dates and deadlines. For the four norms $\ell _{1},\ell _{\infty },\ell _{H}^{\Sigma }$ , and $ \ell _{H}^{\max }$ , the complexity results are derived based on the properties of the corresponding forward problems, while the case of the norm $\ell _{2}$ is treated separately. As a by-product, we resolve an open question on the complexity of problem $1||\sum \alpha _{j}T_{j}^{2}$ .     

Numerical solutions of AXB = C for mirrorsymmetric matrix X under a specified submatrix constraint

Mirrorsymmetric matrices, which are the iteraction matrices of mirrorsymmetric structures, have important application in studying odd/even-mode decomposition of symmetric multiconductor transmission lines (MTL). In this paper we present an efficient algorithm for minimizing ${\|AXB-C\|}$ where ${\|\cdot\|}$ is the Frobenius norm, ${A\in \mathbb{R}^{m\times n}}$ , ${B\in \mathbb{R}^{n\times s}}$ , ${C\in \mathbb{R}^{m\times s}}$ and ${X\in \mathbb{R}^{n\times n}}$ is mirrorsymmetric with a specified central submatrix [x _ij ] _{r≤i, j≤n-r} . Our algorithm produces a suitable X such that AXB = C in finitely many steps, if such an X exists. We show that the algorithm is stable any case, and we give results of numerical experiments that support this claim.     

Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis

Most state-of-the-art approaches for Satisfiability Modulo Theories $(SMT(\mathcal{T}))$ rely on the integration between a SAT solver and a decision procedure for sets of literals in the background theory $\mathcal{T} (\mathcal{T}{\text {-}}solver)$ . Often $\mathcal{T}$ is the combination $\mathcal{T}_1 \cup \mathcal{T}_2$ of two (or more) simpler theories $(SMT(\mathcal{T}_1 \cup \mathcal{T}_2))$ , s.t. the specific ${\mathcal{T}_i}{\text {-}}solvers$ must be combined. Up to a few years ago, the standard approach to $SMT(\mathcal{T}_1 \cup \mathcal{T}_2)$ was to integrate the SAT solver with one combined $\mathcal{T}_1 \cup \mathcal{T}_2{\text {-}}solver$ , obtained from two distinct ${\mathcal{T}_i}{\text {-}}solvers$ by means of evolutions of Nelson and Oppen’s (NO) combination procedure, in which the ${\mathcal{T}_i}{\text {-}}solvers$ deduce and exchange interface equalities. Nowadays many state-of-the-art SMT solvers use evolutions of a more recent $SMT(\mathcal{T}_1 \cup \mathcal{T}_2)$ procedure called Delayed Theory Combination (DTC), in which each ${\mathcal{T}_i}{\text {-}}solver$ interacts directly and only with the SAT solver, in such a way that part or all of the (possibly very expensive) reasoning effort on interface equalities is delegated to the SAT solver itself. In this paper we present a comparative analysis of DTC vs. NO for $SMT(\mathcal{T}_1 \cup \mathcal{T}_2)$ . On the one hand, we explain the advantages of DTC in exploiting the power of modern SAT solvers to reduce the search. On the other hand, we show that the extra amount of Boolean search required to the SAT solver can be controlled. In fact, we prove two novel theoretical results, for both convex and non-convex theories and for different deduction capabilities of the ${\mathcal{T}_i}{\text {-}}solvers$ , which relate the amount of extra Boolean search required to the SAT solver by DTC with the number of deductions and case-splits required to the ${\mathcal{T}_i}{\text {-}}solvers$ by NO in order to perform the same tasks: (i) under the same hypotheses of deduction capabilities of the ${\mathcal{T}_i}{\text {-}}solvers$ required by NO, DTC causes no extra Boolean search; (ii) using ${\mathcal{T}_i}{\text {-}}solvers$ with limited or no deduction capabilities, the extra Boolean search required can be reduced down to a negligible amount by controlling the quality of the $\mathcal{T}$ -conflict sets returned by the ${\mathcal{T}_i}{\text {-}}solvers$ .     

Branching Time Logics \mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha } with Operations Until and Since Based on Bundles of Integer Numbers, Logical Consecutions, Deciding Algorithms

This paper is intended as an attempt to describe logical consequence in branching time logics. We study temporal branching time logics $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ which use the standard operations Until and Next and dual operations Since and Previous (LTL, as standard, uses only Until and Next). Temporal logics $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ are generated by semantics based on Kripke/Hinttikka structures with linear frames of integer numbers $\mathcal {Z}$ with a single node (glued zeros). For $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ , the permissible branching of the node is limited by α (where 1≤α≤ω). We prove that any logic $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ is decidable w.r.t. admissible consecutions (inference rules), i.e. we find an algorithm recognizing consecutions admissible in $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ . As a consequence, it implies that $\mathcal {BTL}^{\mathrm {U,S}}_{\mathrm {N},\mathrm {N}^{-1}}(\mathcal {Z})_{\alpha }$ itself is decidable and solves the satisfiability problem.     

Validating the Knuth-Morris-Pratt Failure Function,Fast and Online

Let $\pi'_{w}$ denote the failure function of the Knuth-Morris-Pratt algorithm for a word w. In this paper we study the following problem: given an integer array $A'[1 \mathinner {\ldotp \ldotp }n]$ , is there a word w over an arbitrary alphabet Σ such that $A'[i]=\pi'_{w}[i]$ for all i? Moreover, what is the minimum cardinality of Σ required? We give an elementary and self-contained $\mathcal{O}(n\log n)$ time algorithm for this problem, thus improving the previously known solution (Duval et al. in Conference in honor of Donald E. Knuth, 2007), which had no polynomial time bound. Using both deeper combinatorial insight into the structure of π′ and advanced algorithmic tools, we further improve the running time to $\mathcal{O}(n)$ .     

Self-Referential Justifications in Epistemic Logic

This paper is devoted to the study of self-referential proofs and/or justifications, i.e., valid proofs that prove statements about these same proofs. The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as  $\mathsf{S4}$ . We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and that the language of justification logic can serve as an adequate refinement. We consider well-known modal logics of knowledge/belief and show, using explicit justifications, that $\mathsf{S4}$ , $\mathsf{D4}$ , $\mathsf{K4}$ , and  $\mathsf{T}$ with their respective justification counterparts  $\mathsf{LP}$ , $\mathsf{JD4}$ , $\mathsf{J4}$ , and  $\mathsf{JT}$ describe knowledge that is self-referential in some strong sense. We also demonstrate that self-referentiality can be avoided for  $\mathsf{K}$ and  $\mathsf{D}$ . In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics. We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics. We also discuss difficulties that result from an introduction of negative introspection.     

Quantum discord in spin systems with dipole–dipole interaction

The behavior of total quantum correlations (discord) in dimers consisting of dipolar-coupled spins 1/2 are studied. We found that the discord $Q=0$ at absolute zero temperature. As the temperature $T$ increases, the quantum correlations in the system increase at first from zero to its maximum and then decrease to zero according to the asymptotic law $T^{-2}$ . It is also shown that in absence of external magnetic field $B$ , the classical correlations $C$ at $T\rightarrow 0$ are, vice versa, maximal. Our calculations predict that in crystalline gypsum $\hbox {CaSO}_{4}\cdot \hbox {2H}_{2}{\hbox {O}}$ the value of natural $(B=0)$ quantum discord between nuclear spins of hydrogen atoms is maximal at the temperature of 0.644  $\upmu $ K, and for 1,2-dichloroethane $\hbox {H}_{2}$ ClC– $\hbox {CH}_{2}{\hbox {Cl}}$ the discord achieves the largest value at $T=0.517~\upmu $ K. In both cases, the discord equals $Q\approx 0.083$  bit/dimer what is $8.3\,\%$ of its upper limit in two-qubit systems. We estimate also that for gypsum at room temperature $Q\sim 10^{-18}$  bit/dimer, and for 1,2-dichloroethane at $T=90$  K the discord is $Q\sim 10^{-17}$  bit per a dimer.     

Tight Bounds for Distributed Minimum-Weight Spanning Tree Verification

This paper introduces the notion of distributed verification without preprocessing. It focuses on the Minimum-weight Spanning Tree (MST) verification problem and establishes tight upper and lower bounds for the time and message complexities of this problem. Specifically, we provide an MST verification algorithm that achieves simultaneously $\tilde{O}(m)$ messages and $\tilde{O}(\sqrt{n} + D)$ time, where m is the number of edges in the given graph G, n is the number of nodes, and D is G’s diameter. On the other hand, we show that any MST verification algorithm must send $\tilde{\varOmega}(m)$ messages and incur $\tilde{\varOmega}(\sqrt{n} + D)$ time in worst case. Our upper bound result appears to indicate that the verification of an MST may be easier than its construction, since for MST construction, both lower bounds of $\tilde{\varOmega}(m)$ messages and $\tilde{\varOmega}(\sqrt{n} + D)$ time hold, but at the moment there is no known distributed algorithm that constructs an MST and achieves simultaneously $\tilde{O}(m)$ messages and $\tilde{O}(\sqrt{n} + D)$ time. Specifically, the best known time-optimal algorithm (using ${\tilde{O}}(\sqrt {n} + D)$ time) requires O(m+n ^3/2) messages, and the best known message-optimal algorithm (using ${\tilde{O}}(m)$ messages) requires O(n) time. On the other hand, our lower bound results indicate that the verification of an MST is not significantly easier than its construction.     

Polyadic tense \theta-valued \Lukasiewicz–Moisil algebras

In this paper we introduce the polyadic tense $\theta$ -valued $\L$ ukasiewicz–Moisil algebras (=polyadic tense $\hbox{LM}_{\theta}$ -algebras), as a common generalization of polyadic tense Boolean algebras and polyadic $\hbox{LM}_{\theta}$ -algebras. Our main result is a representation theorem for polyadic tense $\hbox{LM}_{\theta}$ -algebras.     

Completions of cut systems in Q-sets

Let $ Q$ be a complete residuated lattice. Let $\text {SetR}(Q)$ be the category of sets with similarity relations with values in $ Q$ (called $ Q$ -sets), which is an analogy of the category of classical sets with relations as morphisms. A cut in an $ Q$ -set $(A,\delta )$ is a system $(C_{\alpha })_{\alpha \in Q}$ , where $C_{\alpha }$ are subsets of $A\times Q$ . It is well known that in the category $\text {SetR}(Q)$ , there is a close relation between special cuts (called f-cuts) in an $ Q$ -set on one hand and fuzzy sets in the same $ Q$ -set, on the other hand. Moreover, there exists a completion procedure according to which any cut $(C_{\alpha })_{\alpha }$ can be extended onto an f-cut $(\overline{C_{\alpha }})_{\alpha }$ . In the paper, we prove that the completion procedure is, in some sense, the best possible. This will be expressed by the theorem which states that the category of f-cuts is a full reflective subcategory in the category of cuts.     

Near-Linear Approximation Algorithms for Geometric Hitting Sets

Given a range space $(X,\mathcal{R})$ , where $\mathcal{R}\subset2^{X}$ , the hitting set problem is to find a smallest-cardinality subset H?X that intersects each set in $\mathcal{R}$ . We present near-linear-time approximation algorithms for the hitting set problem in the following geometric settings: (i)? $\mathcal{R}$ is a set of planar regions with small union complexity. (ii)? $\mathcal{R}$ is a set of axis-parallel d-dimensional boxes in ? ^d . In both cases X is either the entire ? ^d , or a finite set of points in ? ^d . The approximation factors yielded by the algorithm are small; they are either the same as, or within very small factors off the best factors known to be computable in polynomial time.     

Topology-Preserving Conditions for 2D Digital Images Under Rigid Transformations

In the continuous domain $\mathbb{R}^{n}$ , rigid transformations are topology-preserving operations. Due to digitization, this is not the case when considering digital images, i.e., images defined on $\mathbb{Z}^{n}$ . In this article, we begin to investigate this problem by studying conditions for digital images to preserve their topological properties under all rigid transformations on $\mathbb{Z}^{2}$ . Based on (i) the recently introduced notion of DRT graph, and (ii) the notion of simple point, we propose an algorithm for evaluating digital images topological invariance.