This paper presents a novel approach to distributed constraint satisfaction (CS) algorithms by leveraging blockchain technology for verification. The core challenge in distributed CS lies in ensuring the correctness and reliability of the algorithms across multiple nodes. Existing solutions often rely on centralized trust models, which are vulnerable to manipulation and single points of failure. Our proposed system addresses this by employing a decentralized architecture where each node executes a CS algorithm, and the resulting solutions are cryptographically verified through a blockchain. This creates an immutable audit trail, guaranteeing the integrity of the process and fostering trust among participants. The system uses a distributed consensus mechanism to maintain the blockchain and ensures that any deviation from the expected solution will be flagged. This approach significantly enhances the security, reliability, and transparency of distributed CS, opening possibilities for applications in areas like smart grids, supply chain management, and decentralized autonomous organizations (DAOs). The key innovation resides in the combination of distributed computation with verifiable blockchain records, offering a robust and trustworthy solution for complex problem-solving scenarios.
For most distributed financial systems, the constraints imposed by the CAP (Consistency, Availability, Partition Tolerance) theorem must be reconciled against the ordering constraints needed to satisfy regulatory requirements and meet the performance requirements of real-time transaction processing. This paper presents the Temporal Sequence Barrier consistency model for asynchronous high-throughput ledger systems. Combining logical vector clocks with epoch-based orchestration patterns imposes a strict causal ordering of events across multiple geographic regions without sacrificing availability. Its database-centric architecture allows stateful routing and selective replication of entities in order to achieve linearizability of causally related transactions while allowing independent sets of entities to be processed in parallel. We provide a detailed evaluation that shows that we can provide causal consistency at latency bounds equal to or better than existing systems using clever buffering and adaptive timeouts, while also addressing the classic challenges in distributed transaction management and operator complexity.
Mohammad Rafiqul Islam, Silicon-Saffat TRISDUCTION
The P versus NP problem, formalized by Cook (1971) and designated a Clay Millennium Prize Problem in 2000, asks whether every computational problem whose solution can be verified in polynomial time can also be solved in polynomial time. For fifty-five years the problem has resisted all single-axis formal resolution attempts. Three independently proven barrier results have demonstrated that all currently known classes of mathematical proof technique are structurally incapable of settling the question within the formal axis alone. This paper presents a unified geometric determination of both P = NP and P ≠ NP using the Trisduction ENGINE, an epistemic certification architecture operating across three orthogonal warrant-vectors: Formal (V_F), Empirical (V_E), and Phenomenological (V_P). Version 10.0 introduces two architectural upgrades over prior versions: Rule 9 Axiomatic Quarantine, which formally removes the Turing Machine abstraction from the framework's admissible baseline and replaces it with the Tri-Layer Plenum topology; and the Meta-Epistemic Hierarchy (Geometry > Mathematics > Logic), which resolves the recurring drift pattern in which formal demands were treated as epistemically superior to geometric physical measurement. The two audits are presented as a single master document to make the asymmetry between the claims structurally transparent: P = NP carries zero positive warrant across all three axes and is stopped at Gate 2; P ≠ NP passes all twelve gates with three fully independent, orthogonal warrant-vectors. The determination is explicitly non-deductive. It does not constitute a traditional mathematical proof and does not satisfy the Clay Mathematics Institute's criteria. GOL [⟀] is defined as the strongest achievable non-deductive epistemic warrant: the geometric fact that three orthogonal planes exhaust all degrees of freedom in the epistemic space, leaving no room for the alternative claim to occupy. The paper's central phenomenological contribution is the dual anchoring of V_P through the Zero-Knowledge Proof conviction gap and the Frame-Independent Observer actualization boundary. Both sources survive the Linguistic Isolation Test against V_F and V_E vocabulary, the Deletion Test, and four rounds of post-certification stress-testing documented in the appendices. The Convergence Dissolution Test finds irreducible residue in all three vectors under the strongest single-factor account. The Living Verifiable Proof — the Engine's simultaneous perfect verification capacity and structurally total generative incapacity at the Isometric Plenum boundary — provides continuously falsifiable phenomenological evidence that checking does not entail finding.
In this paper, I prove that sublinear regret across the environment Class C requires six functional properties, that these properties are mutually independent, and that they compose into a directed informational chain closing back on itself — a six-link cycle whose final link is grounded in an explicit Doob martingale construction over cycles of play. All six properties are defined functionally — as conditions on the distributions a decision-maker induces over actions and canonical summaries — so the results are invariant under implementation and apply to any decision-making system that can be modelled within the class: a person, an institution, or a machine. Every theorem in this paper, without exception, is checked line by line in the Lean 4 proof assistant against Mathlib: the formalization (~12,700 lines) contains zero `sorry`, zero custom axioms, and zero opaque definitions. Class C is the union of all POMDPs satisfying at least one of six structural properties covering the fundamental qualitative dimensions of adaptive hardness: reward ambiguity (P1), absorbing traps (P2), local optima (P3), deterministic optimality (P4), constrained feasibility (P5), and nonstationarity (P6). * Part I (Necessity). I define six primitives X1–X6 as purely functional properties of decision rules: Objective Tracking, Cross-Context Safety Transfer, Global Attractor Exploration, Policy Simplification, Feasibility Projection, and Feedback Adaptation. For each, I construct an explicit environment in C and prove an unconditional Ω(T) regret lower bound for any decision-maker lacking that primitive.* Part II (Independence). For every ordered pair (i,j) with i≠j, I exhibit an explicit decision rule possessing Xj but lacking Xi that suffers Ω(T) regret on the matching environment. All thirty directed-pair results are shown to follow from one master theorem, verified on a single compound environment with full non-interference analysis.* Part III (Sequential Dependence). Necessity is domain-invariant — a structural failure is a structural failure no matter what "success" means to the decision-maker — which is why Parts I and II hold unconditionally. Sufficiency is not: what counts as success is supplied by the domain, not by the theorem, so a single closed-form sufficiency result covering every domain at once would have to either fix one arbitrary notion of success and stop being general, or say nothing of substance. Part III proves exactly what generalizes. I prove six Information Enhancement Theorems establishing that the six primitives compose into a directed information chain: possessing Xi strictly increases the mutual information available toward any goal variable at Xi+1's task. Each of the six links is established outright — a forward theorem, a reverse theorem, and a non-reversibility result — with the exact point where a domain's own definition of success enters the chain named explicitly, as an Implementation Obligation, rather than assumed away. The closing link, X6→X1, is grounded in an actual Doob martingale construction: given that the cycle-indexed posterior is a martingale, it converges almost surely to the truth across cycles — the precise sense in which the chain accumulates rather than resets. To this paper's knowledge, no prior formalization unifies this many independently-proven-necessary structural properties into a single machine-checked class with proven mutual independence across all of them. All mathematical work is provided in full transparency and independent verification is highly encouraged: the complete Lean formalization, with a passing build and every theorem cross-referenced to its exact identifier, is at github.com/M-Ismail-ZA/IsmailsPrimitives. For any feedback or collaboration, please contact me via the email address listed on the paper. Updated: 3 July 2026 (V6.1).
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo
Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.
Recently, Non-Fungible Tokens (NFTs) have attracted attention as valuable digital assets. However, NFT marketplaces face complex challenges in simultaneously recommending optimal pricing to sellers and desirable NFTs to buyers. Unlike conventional marketplaces that focus only on balancing demand and supply between sellers and buyers, these tasks are complicated by intricate value interdependencies arising from diverse buyer preferences, budgets, trait rarities, and the unprecedented breeding mechanisms. This paper formulates the NFT Project Pricing/Purchasing Recommendation (NP3R) problem, aiming to achieve a competitive equilibrium that concurrently optimizes seller revenue and buyer utility. We introduce BANTER, an iterative algorithm that jointly determines (1) optimal NFT purchases for buyers (via NFT-REC), considering breeding utility and current prices; and (2) optimal pricing for sellers (via PRICEREC), based on aggregated demand from NFT-REC. To efficiently manage the combinatorial complexity of breeding, we devise Optimal Parent Pair Selection (OPPS) and Heterogeneous Parent Set Selection (HPSS) schemes. Theoretical analysis guarantees BANTER to converge to a competitive equilibrium. Experiments on five real-world NFT datasets demonstrate its effectiveness in enhancing both seller revenue and average buyer utility. Source code: https://github.com/jimmy-academia/BANTER
Ethereum block building has traditionally been approached using greedy algorithms that prioritize transactions with the highest fee per unit of gas. This work proposes an alternative that considers semantic interactions among transactions and operational constraints to define the utility of transaction combinations. Through a utility model that assigns bonuses and penalties to pairs and triples of transactions, we design algorithms capable of constructing blocks more valuable than those obtained by traditional methods. In experiments with 1,000 real transactions extracted from the network, two algorithms were implemented and evaluated, both grounded in a formulation inspired by job scheduling theory: a classic greedy baseline and the proposed heuristic. The base heuristic achieved approximately 86 % of the utility of the greedy approach ($6.78 \times 10^{20}$vs.$7.81 \times 10^{20}$) while including only 23 transactions. The extended version with greedy fill reached up to 120 % of the reference utility ($1.73 \times 10^{21}$), incorporating 268 transactions compared to 212 for the greedy, while maintaining execution times below 2 seconds. These preliminary results demonstrate the feasibility of capturing additional semantic value within time windows compatible with Ethereum block-building intervals, based on isolated experiments with bounded transaction sets.
As Distributed Ledger Technologies (DLTs) mature, the inherent performance and scalability shortcomings of linearly structured blockchain designs become better understood. Protocols based on Directed Acyclic Graphs (DAGs) have been proposed to address such shortcomings. DAG-based protocols differ from traditional DLTs in the way they build and represent knowledge about transactions and relations between them. While traditional DLTs have straightforward homogeneous semantic attached to blocks and links between blocks, the semantic of vertices and edges in DAG-based protocols is nuanced and varied. In this work, we identify almost a dozen of knowledge-building dimensions in DAG-based DLTs, none of which have been studied before. Knowledge-building is important in DAG-based DLTs because of its significant impact on the size of the DAG, the pace at which new transactions are added, the finality of transactions, and so on. We analyze 40 DAG-based DLTs from this perspective, summarize our results in a taxonomy, and identify a number of research gaps.
This paper studies the \emph{unimodular isomorphism problem} (UIP) of convex lattice polytopes: given two convex lattice polytopes $P$ and $P'$, decide whether there exists a unimodular affine transformation mapping $P$ to $P'$. We show that UIP is graph isomorphism hard, while the polytope congruence problem and the combinatorial polytope isomorphism problem (Akutsu, 1998; Kaibel, Schwartz, 2003) were shown to be graph isomorphism complete, and both the lattice isomorphism problem ( $\mathrm{Sikiri\acute{c}}$, $\mathrm{Sch\ddot{u}rmann}$, Vallentin, 2009) and the projective/affine polytope isomorphism problem (Kaibel, Schwartz, 2003) were shown to be graph isomorphism hard. Furthermore, inspired by protocols for lattice (non-) isomorphism (Ducas, van Woerden, 2022; Haviv, Regev, 2014), we present a statistical zero-knowledge proof system for unimodular isomorphism of lattice polytopes. Finally, we propose an algorithm that given two lattice polytopes computes all unimodular affine transformations mapping one polytope to another and, in particular, decides UIP.
Bernhard Fisseni, Deniz Sarikaya, Bernhard Schröder
Abstract We discuss conceptual change and progress within mathematics, in particular how tools, structural concepts and representations are transferred between fields that appear to be unconnected or remote from each other. The theoretical background is provided by the frame concept, which is used in linguistics, cognitive science and artificial intelligence to model how explicitly given information is combined with expectations deriving from background knowledge. In mathematical proofs, we distinguish two kinds of frames, namely structural frames and ontological frames. The interaction between both kinds of frames can drive mathematical interpretation. We first discuss two examples where structural frames (formulaic notation) drive ontological development (the discovery or exploration of mathematical objects). The development of Boole’s Boolean algebra may at first appear as a metaphorical treatment of the (then) new area of logic. In the analysis, we discuss how different (aspects of) certain algebraic frames change in the transfer, how arising difficulties are solved and overall argue that Boole uses the numerical algebra frame as a research template for the discovery of a system for calculations in logic. Following Ifrah, we analyse the discovery of zero as an extension to the number ontology as driven by the development of notation. Both structural and ontological frames are extended and simplified as notation progresses. Finally, we discuss two examples from infinite combinatorics, viz. topological graph theory, and one foundational issue. In both examples, the two simultaneous frames about one object are maintained independently. They motivate different research questions, but may also fruitfully interact: shifting between multiple synchronously maintained perspectives acts as a motor of innovation. The analysis shows how a frame-based approach allows to model how different perspectives drive mathematical innovation because they highlight different aspects, questions and heuristics.
Standard probabilistic models face fundamental challenges such as data scarcity, a large hypothesis space, and poor data transparency. To address these challenges, we propose a novel probabilistic model of data-driven temporal propositional reasoning. Unlike conventional probabilistic models where data is a product of domain knowledge encoded in the probabilistic model, we explore the reverse direction where domain knowledge is a product of data encoded in the probabilistic model. This more data-driven perspective suggests no distinction between maximum likelihood parameter learning and temporal propositional reasoning. We show that our probabilistic model is equivalent to a highest-order, i.e., full-memory, Markov chain, and it can also be viewed as a hidden Markov model requiring no distinction between hidden and observable variables. We discuss that limits provide a natural and mathematically rigorous way to handle data scarcity, including the zero-frequency problem. We also discuss that a probability distribution over data generated by our probabilistic model helps data transparency by revealing influential data used in predictions. The reproducibility of this theoretical work is fully demonstrated by the included proofs.
Random algorithms have a unique place in complexity theory as a model of computation that ispotentially more powerful than “normal” algorithms, and is also practical. However, it is still notclear how much more power randomness adds. The primary goal in studying random algorithmsis derandomization – some method to simulate random algorithms without actually using random-ness. While full derandomization is quite difficult, we show some weak derandomization results –one using advice, and one using multi-pseudodeterminism. We show that improving these resultswould have major implications. Finally, we show new containments and oracle separations betweentraditional random classes and zero-knowledge proofs.
Stuart H. Rubin, Thouraya Bouabana‐Tebibel, Yasmine Hoadjli, Kadaouia Habib · 5 authors
The solution of NP-hard problems requires the use of one or more explicit or implicit heuristics as a practical measure. Quantum computers promise to make this practical for O (2n) problems or less, but have yet to deliver a solution to a single NP-hard problem. The question addressed by this paper is whether domain transference and reuse of problem-solving knowledge can be mediated through the reuse of heuristics, and, if so, the extent to which such transference may occur in the solution of NP-hard problems. Neural networks have zero domain transference on account of their inability to represent modus ponens. Similarly, CBR, deep learning, EP, GAs, SVMs, the predicate calculus, learning via conventional expert systems, and all other machine learning technologies are unable to theoretically or practically mediate domain transference because they don't respect randomization as the core underpinning technology. The paper offers a constructive proof of the unbounded density of knowledge in support of the Semantic Randomization Theorem (SRT). It details this result and its potential impact on the machine learning community.
Abstract—Digital signature schemes are a founda-tional cryptographic building block in certification and the projection of trust. Based on a signature scheme on committed graphs, we propose a toolkit of certification and proof methods to sign committed topology graphs and to prove properties of their certificates in zero-knowledge. This toolkit allows an issuer, such as an auditor, to sign the topology repre-sentation of an infrastructure. The prover, such as an infrastructure provider, can then convince a verifier of topology properties, such as partitions, connectivity or isolation, without disclosing the structure of the topol-ogy itself. By that, we can achieve the certification of the structure of critical systems, such as infrastructure clouds or outsourced systems, while still maintaining confidentiality. We offer zero-knowledge proofs of knowledge for a general specification language of security goals for virtualized infrastructures, such that high-level security goals can be proven over the topology certificate. Our method builds upon the Camenisch-Lysyanskaya signature scheme, is based on honest-verifier proofs and the strong RSA assumption. I.
In this article, we introduce a Prover–Verifier model for analysing the computational complexity of a class of constraint satisfaction problems (CSPs) termed boolean binary constraint satisfaction problems (BBCSPs). BBCSPs represent an extremely general class of CSPs and find applications in a wide variety of domains including constraint programming, puzzle solving and program testing. The constraints in a BBCSP permit the combination of multiple theories as opposed to traditional constraint systems in which all constraints belong to the same theory. We establish that each instance of a BBCSP admits a coin-flipping Turing machine that halts in time polynomial in the size of the input. Furthermore, the algorithm is oblivious in that it never sees more than one constraint at a time. The prover, P, in the Prover–Verifier model is endowed with very limited powers. In particular, it has no memory and it can only pose restricted queries to the verifier. The verifier, on the other hand, is both omniscient in that it is cognisant of all the problem details and insincere in that it does not have to decide a priori on the intended proof. However, the verifier must stay consistent in its responses, i.e. it cannot rule out a certain possibility in one response to a query from the prover and then rule in the same possibility in response to a subsequent query. We note that the combination of the resources required by the prover and the type of certificate demanded of the verifier, determine the resources required by an algorithm. Inasmuch as our provers will be memoryless and our verifiers will be asked for extremely simple certificates, our work establishes the existence of a simple, randomised algorithm for BBCSPs. Our model itself serves as a basis for the design of zero-knowledge machine learning algorithms in that the prover ends up learning the proof desired by the verifier. Likewise, our work finds applications in the domain of certifying algorithm design, wherein the goal is to provide a proof of correctness of the algorithm on the input instance by providing an easily checkable certificate.
Many backtracking algorithms exhibit heavy-tailed distributions, in which their running time is often much longer than their median. We analyze the behavior of two natural variants of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm for Graph 3-Coloring on sparse random graphs G(n,p=c/n). Let P_c(b) be the probability that DPLL backtracks b times. First, we calculate analytically the probability P_c(0) that these algorithms find a 3-coloring with no backtracking at all, and show that it goes to zero faster than any analytic function as c \to c^* = 3.847... Then we show that even in the ``easy'' phase 1 < c < c^* where P_c(0) > 0, including just above the emergence of the giant component, the expected number of backtracks is exponentially large with positive probability. To our knowledge this is the first rigorous proof that the running time of a natural backtracking algorithm has a heavy tail for graph coloring. Moreover, our results show that these algorithms take exponential time, not just below the 3-colorability threshold, but just above the degree c=1 at which the giant component first appears. In addition, we give experimental evidence and heuristic arguments that this tail takes the form P_c(b) ~ b^{-1} up to an exponential cutoff.