arXiv subjects

Xishun Zhao

Publications and source records attributed to Xishun Zhao.

12 recordsLinked to original sources

arXiv2023

Capturing the polynomial hierarchy by second-order revised Krom logic

We study the expressive power and complexity of second-order revised Krom logic (SO-KROM$^{r}$). On ordered finite structures, we show that its existential fragment $Σ^1_1$-KROM$^r$ equals $Σ^1_1$-KROM, and captures NL. On all finite structures, for $k\geq 1$, we show that $Σ^1_{k}$ equals $Σ^1_{k+1}$-KROM$^r$ if $k$ is even, and $Π^1_{k}$ equals $Π^1_{k+1}$-KROM$^r$ if $k$ is odd. The result gives an alternative logic to capture the polynomial hierarchy. We also introduce an extended version of second-order Krom logic (SO-EKROM). On ordered finite structures, we prove that SO-EKROM collapses to $Π^{1}_{2}$-EKROM and equals $Π^1_1$. Both SO-EKROM and $Π^{1}_{2}$-EKROM capture co-NP on ordered finite structures.

cs.LO↗

arXiv2022

The Complexity and Expressive Power of Second-Order Extended Logic

We study the expressive powers of SO-HORN$^{*}$, SO-HORN$^{r}$ and SO-HORN$^{*r}$ on all finite structures. We show that SO-HORN$^{r}$, SO-HORN$^{*r}$, FO(LFP) coincide with each other and SO-HORN$^{*}$ is proper sublogic of SO-HORN$^{r}$. To prove this result, we introduce the notions of DATALOG$^{*}$ program, DATALOG$^{r}$ program and their stratified versions, S-DATALOG$^{*}$ program and S-DATALOG$^{r}$ program. It is shown that, on all structures, DATALOG$^{r}$ and S-DATALOG$^{r}$ are equivalent and DATALOG$^{*}$ is a proper sublogic of DATALOG$^{r}$. SO-HORN$^{*}$ and SO-HORN$^{r}$ can be treated as the negations of DATALOG$^{*}$ and DATALOG$^{r}$, respectively. We also show that SO-EHORN$^{r}$ logic which is an extended version of SO-HORN captures co-NP on all finite structures.

cs.LO↗

arXiv2022

A Logic that Captures $β$P on Ordered Structures

We extend the inflationary fixed-point logic, IFP, with a new kind of second-order quantifiers which have (poly-)logarithmic bounds. We prove that on ordered structures the new logic $\exists^{\log^ω}\text{IFP}$ captures the limited nondeterminism class $β\text{P}$. In order to study its expressive power, we also design a new version of Ehrenfeucht-Fraïssé game for this logic and show that our capturing result will not hold on the general case, i.e. on all the finite structures.

cs.LO↗

arXiv2018

Quantum-enhanced Logic-based Blockchain I: Quantum Honest-success Byzantine Agreement and Qulogicoin

We proposed a framework of quantum-enhanced logic-based blockchain, which improves the efficiency and power of quantum-secured blockchain. The efficiency is improved by using a new quantum honest-success Byzantine agreement protocol to replace the classical Byzantine agreement protocol, while the power is improved by incorporating quantum protection and quantum certificate into the syntax of transactions. Our quantum-secured logic-based blockchain can already be implemented by the current technology. The cryptocurrency created and transferred in our blockchain is called qulogicoin. Incorporating quantum protection and quantum certificates into blockchain makes it possible to use blockchain to overcome the limitations of some quantum cryptographic protocols. As an illustration, we show that a significant shortcoming of cheat-sensitive quantum bit commitment protocols can be overcome with the help of our blockchain and qulogicoin.

quant-ph↗

arXiv2017

Bounds for variables with few occurrences in conjunctive normal forms

We investigate connections between SAT (the propositional satisfiability problem) and combinatorics, around the minimum degree (number of occurrences) of variables in various forms of redundancy-free boolean conjunctive normal forms (clause-sets). Lean clause-sets do not have non-trivial autarkies, that is, it is not possible to satisfy some clauses and leave the other clauses untouched. The deficiency of a clause-set is the difference of the number of clauses and the number of variables. We prove a precise upper bound on the minimum variable degree of lean clause-sets in dependency on the deficiency. If a clause-set does not fulfil this upper bound, then it must have a non-trivial autarky; we show that the autarky-reduction (elimination of affected clauses) can be done in polynomial time, while it is open to find the autarky itself in polynomial time. Then we investigate this upper bound for the special case of minimally unsatisfiable clause-sets. We show that the bound can be improved here, introducing a general method to improve the underlying recurrence. We consider precise relations, and thus the investigations have a number-theoretical flavour. We try to build a bridge from logic to combinatorics (especially to hypergraph colouring), and we discuss thoroughly the background and open problems, and provide many examples and explanations.

math.CO↗

arXiv2016

Unsatisfiable hitting clause-sets with three more clauses than variables

The topic of this paper is the Finiteness Conjecture for minimally unsatisfiable clause-sets (MUs), stating that for each fixed deficiency (number of clauses minus number of variables) there are only finitely many patterns, given a certain basic reduction (generalising unit-clause propagation). We focus our attention on hitting clause-sets (every two clauses have at least one clash), where the conjecture says that there are only finitely many isomorphism types. The Finiteness Conjecture is here known to hold for deficiency at most 2, and we now prove it for deficiency 3. An important tool is the notion of "(ir)reducible clause-sets": we show how to reduce the general question to the irreducible case, and then solve this case (for deficiency 3). This notion comes from number theory (Korec 1984, Berger et al 1990), and we rediscovered it in our studies.

cs.DM↗

arXiv2015

Parameters for minimal unsatisfiability: Smarandache primitive numbers and full clauses

We establish a new bridge between propositional logic and elementary number theory. The main objects are "minimally unsatisfiable clause-sets", short "MUs", unsatisfiable conjunctive normal forms rendered satisfiable by elimination of any clause. In other words, irredundant coverings of the boolean hypercube by subcubes. The main parameter for MUs is the "deficiency" k, the difference between the number of clauses and the number of variables (the difference between the number of elements in the covering and the dimension of the hypercube), and the fundamental fact is that k >= 1 holds. A "full clause" in an MU contains all variables (corresponding to a singleton in the covering). We show the lower bound S_2(k) <= FCM(k), where FCM(k) is the maximal number of full clauses in MUs of deficiency k, while S_2(k) is the smallest n such that 2^k divides n!. The proof rests on two methods: On the logic-combinatorial side, applying subsumption resolution and its inverse, a fundamental method since Boole in 1854 introduced the "expansion method". On the arithmetical side, analysing certain recursions, combining an application-specific recursion with a recursion from the field of meta-Fibonacci sequences (indeed S_2 equals twice the Conolly sequence). A further tool is the consideration of unsatisfiable "hitting clause-sets" (UHITs), special cases of MUs, which correspond to the partitions of the boolean hypercube by subcubes; they are also known as orthogonal or disjoint DNF tautologies. We actually show the sharper lower bound S_2(k) <= FCH(k), where FCH(k) is the maximal number of full clauses in UHITs of deficiency k. We conjecture that for all k holds S_2(k) = FCH(k), which would establish a surprising connection between the extremal combinatorics of (un)satisfiability and elementary number theory. We apply the lower bound to analyse the structure of MUs and UHITs.

cs.DM↗

arXiv2015

Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas

\emph{Canonical (logic) programs} (CP) refer to normal logic programs augmented with connective $not\ not$. In this paper we address the question of whether CP are \emph{succinctly incomparable} with \emph{propositional formulas} (PF). Our main result shows that the PARITY problem, which can be polynomially represented in PF but \emph{only} has exponential representations in CP. In other words, PARITY \emph{separates} PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable when translating a set of formulas in PF into an equivalent program in CP (without introducing new variables). Furthermore, since it has been shown by Lifschitz and Razborov that there is also a problem that separates CP from PF (assuming $\mathsf{P}\nsubseteq \mathsf{NC^1/poly}$), it follows that CP and PF are indeed succinctly incomparable. From the view of the theory of computation, the above result may also be considered as the separation of two \emph{models of computation}, i.e., we identify a language in $\mathsf{NC^1/poly}$ which is not in the set of languages computable by polynomial size CP programs.

cs.LO↗

arXiv2012

On Davis-Putnam reductions for minimally unsatisfiable clause-sets

For investigations into the structure of MU, i.e., minimally unsatisfiable clause-sets or conjunctive normal forms, singular DP-reduction is a fundamental tool, applying DP-reduction F -> DP_v(F) in case variable v occurs in one polarity only once. Recall, in general DP_v(F) replaces all clauses containing variable v by their resolvents on v (another name is "variable elimination"). We consider sDP(F), the set of all results of applying singular DP-reduction to F in MU as long as possible, obtaining non-singular F' in MU with the same deficiency, i.e., delta(F') = delta(F). (In general, delta(F) is the difference c(F) - n(F) of the number of clauses and the number of variables.) Our main results are: 1. For all F', F" in sDP(F) we have n(F') = n(F"). 2. If F is saturated (F in SMU), then we have |sDP(F)| = 1. 3. If F is "eventually saturated", that is, sDP(F) <= SMU, then for F', F" in sDP(F) we have F' isomorphic F" (establishing "confluence modulo isomorphism"). The results are obtained by a detailed analysis of singular DP-reduction for F in MU. As an application we obtain that singular DP-reduction for F in MU(2) (i.e., delta(F) = 2) is confluent modulo isomorphism (using the fundamental characterisation of MU(2) by Kleine Buening). The background for these considerations is the general project of the classification of MU in terms of the deficiency.

cs.DM↗

arXiv2011

Proof System for Plan Verification under 0-Approximation Semantics

In this paper a proof system is developed for plan verification problems $\{X\}c\{Y\}$ and $\{X\}c\{KW p\}$ under 0-approximation semantics for ${\mathcal A}_K$. Here, for a plan $c$, two sets $X,Y$ of fluent literals, and a literal $p$, $\{X\}c\{Y\}$ (resp. $\{X\}c\{KW p\}$) means that all literals of $Y$ become true (resp. $p$ becomes known) after executing $c$ in any initial state in which all literals in $X$ are true.Then, soundness and completeness are proved. The proof system allows verifying plans and generating plans as well.

cs.AI↗

arXiv2011

On variables with few occurrences in conjunctive normal forms

We consider the question of the existence of variables with few occurrences in boolean conjunctive normal forms (clause-sets). Let mvd(F) for a clause-set F denote the minimal variable-degree, the minimum of the number of occurrences of variables. Our main result is an upper bound mvd(F) <= nM(surp(F)) <= surp(F) + 1 + log_2(surp(F)) for lean clause-sets F in dependency on the surplus surp(F). - Lean clause-sets, defined as having no non-trivial autarkies, generalise minimally unsatisfiable clause-sets. - For the surplus we have surp(F) <= delta(F) = c(F) - n(F), using the deficiency delta(F) of clause-sets, the difference between the number of clauses and the number of variables. - nM(k) is the k-th "non-Mersenne" number, skipping in the sequence of natural numbers all numbers of the form 2^n - 1. We conjecture that this bound is nearly precise for minimally unsatisfiable clause-sets. As an application of the upper bound we obtain that (arbitrary!) clause-sets F with mvd(F) > nM(surp(F)) must have a non-trivial autarky (so clauses can be removed satisfiability-equivalently by an assignment satisfying some clauses and not touching the other clauses). It is open whether such an autarky can be found in polynomial time. As a future application we discuss the classification of minimally unsatisfiable clause-sets depending on the deficiency.

cs.DM↗

arXiv2010

NP-Logic Systems and Model-Equivalence Reductions

In this paper we investigate the existence of model-equivalence reduction between NP-logic systems which are logic systems with model existence problem in NP. It is shown that among all NP-systems with model checking problem in NP, the existentially quantified propositional logic (\exists PF) is maximal with respect to poly-time model-equivalent reduction. However, \exists PF seems not a maximal NP-system in general because there exits a NP-system with model checking problem D^P-complete.

cs.LO↗