Wyniki wyszukiwania - BazTech

1

Optimal SAT Solver Synthesis of Quantum Circuits Representing Cryptographic Nonlinear Functions

Jagielski Adam

International Journal of Electronics and Telecommunications

|

2023

|

Vol. 69, No. 2

261--267

EN

In this article we present a procedure that allows to synthesize optimal circuit representing any reversible function within reasonable size limits. The procedure allows to choose either the NCT or the MCT gate set and specify any number of ancillary qubits to be used in the circuit. We will explore efficacy of this procedure by synthesizing various sources of nonlinearity used in contemporary symmetric ciphers and draw conclusions about properties of those transformations in quantum setting. In particular we will try to synthesize optimal circuit representing ASCON cipher SBOX which recently won NIST competition for Lightweight Cryptography standard.

2

Parallel Algorithms for Minimal Nondeterministic Finite Automata Inference

Jastrzab Tomasz, Czech Zbigniew J., Wieczorek Wojciech

Fundamenta Informaticae

|

2021

|

Vol. 178, nr 3

203--227

EN

The goal of this paper is to develop the parallel algorithms that, on input of a learning sample, identify a regular language by means of a nondeterministic finite automaton (NFA). A sample is a pair of finite sets containing positive and negative examples. Given a sample, a minimal NFA that represents the target regular language is sought. We define the task of finding an NFA, which accepts all positive examples and rejects all negative ones, as a constraint satisfaction problem, and then propose the parallel algorithms to solve the problem. The results of comprehensive computational experiments on the variety of inference tasks are reported. The question of minimizing an NFA consistent with a learning sample is computationally hard.

3

Complexity Assessments for Decidable Fragments of Set Theory. I : A Taxonomy for the Boolean Case

Cantone Domenico, De Domenico Andrea, Maugeri Pietro, Omodeo Eugenio G.

Fundamenta Informaticae

|

2021

|

Vol. 181, nr 1

37--69

EN

We report on an investigation aimed at identifying small fragments of set theory (typically, sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this paper we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, \, the Boolean relators ⊆, ⊈,=, ≠, and the predicates ‘• = Ø’ and ‘Disj(•, •)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘• ≠ Ø and ‘¬Disj(•, •)’. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

4

Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

Kullmann O.

Fundamenta Informaticae

|

2011

|

Vol. 109, nr 1

27-81

EN

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown "signed literals", corresponding to unary constraints in CSP. However we argue that only the restricted form of "negative monosigned literals" and the resulting generalised clause-sets, corresponding to "sets of no-goods" in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency.

5

The complexity of certain modal formulas on binary ramified subset trees

Heinemann B.

Fundamenta Informaticae

|

1999

|

Vol. 39, Nr 3

259-272

EN

In the present note we determine the complexity of the satisfiability problem of a certain modal logic of subset spaces which was proposed in [6]. The corresponding semantics is defined w.r.t. binary ramified subset trees consisting of a set X and a distinguished set O of subsets of X such that the relation of reverse set inclusion makes O a binary ramified tree. It turns out that the satisfiability problem of the logic is complete in NP.