Artykuły w czasopismach: „Conjunctive normal form”

1

De Ita Luna, Guillermo, J. Raymundo Marcial-Romero i José A. Hernández. "The Incremental Satisfiability Problem for a Two Conjunctive Normal Form". Electronic Notes in Theoretical Computer Science 328 (grudzień 2016): 31–45. http://dx.doi.org/10.1016/j.entcs.2016.11.004.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

2

Vaisman, Radislav, Ofer Strichman i Ilya Gertsbakh. "Model Counting of Monotone Conjunctive Normal Form Formulas with Spectra". INFORMS Journal on Computing 27, nr 2 (kwiecień 2015): 406–15. http://dx.doi.org/10.1287/ijoc.2014.0633.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

3

Warners, Joost P. "A linear-time transformation of linear inequalities into conjunctive normal form". Information Processing Letters 68, nr 2 (październik 1998): 63–69. http://dx.doi.org/10.1016/s0020-0190(98)00144-6.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

4

Losee, Robert M., i Abraham Bookstein. "Integrating Boolean queries in conjunctive normal form with probabilistic retrieval models". Information Processing & Management 24, nr 3 (styczeń 1988): 315–21. http://dx.doi.org/10.1016/0306-4573(88)90097-0.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

5

Bruni, Renato. "On the orthogonalization of arbitrary Boolean formulae". Journal of Applied Mathematics and Decision Sciences 2005, nr 2 (1.01.2005): 61–74. http://dx.doi.org/10.1155/jamds.2005.61.

Pełny tekst źródła

Streszczenie:

The orthogonal conjunctive normal form of a Boolean function is a conjunctive normal form in which any two clauses contain at least a pair of complementary literals. Orthogonal disjunctive normal form is defined similarly. Orthogonalization is the process of transforming the normal form of a Boolean function to orthogonal normal form. The problem is of great relevance in several applications, for example, in the reliability theory. Moreover, such problem is strongly connected with the well-known propositional satisfiability problem. Therefore, important complexity issues are involved. A general procedure for transforming an arbitrary CNF or DNF to an orthogonal one is proposed. Such procedure is tested on randomly generated Boolean formulae.

Style APA, Harvard, Vancouver, ISO itp.

6

Zhang, Zaijun, Daoyun Xu i Jincheng Zhou. "A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form". Entropy 23, nr 3 (4.03.2021): 303. http://dx.doi.org/10.3390/e23030303.

Pełny tekst źródła

Streszczenie:

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.

Style APA, Harvard, Vancouver, ISO itp.

7

Schuler, Rainer. "An algorithm for the satisfiability problem of formulas in conjunctive normal form". Journal of Algorithms 54, nr 1 (styczeń 2005): 40–44. http://dx.doi.org/10.1016/j.jalgor.2004.04.012.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

8

Seth, Abhay Deep, Santosh Biswas i Amit Kumar Dhar. "DADCNF: Diagnoser design for Duplicate Address Detection threat using Conjunctive Normal Form". Computer Networks 222 (luty 2023): 109539. http://dx.doi.org/10.1016/j.comnet.2022.109539.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

9

Gropp, Ursula. "Coinductive formulas and a many-sorted interpolation theorem". Journal of Symbolic Logic 53, nr 3 (wrzesień 1988): 937–60. http://dx.doi.org/10.2307/2274584.

Pełny tekst źródła

Streszczenie:

AbstractWe use connections between conjunctive game formulas and the theory of inductive definitions to define the notions of a coinductive formula and its approximations. Corresponding to the theory of conjunctive game formulas we develop a theory of coinductive formulas, including a covering theorem and a normal form theorem for many sorted languages. Applying both theorems and the results on “model interpolation” obtained in this paper, we prove a many-sorted interpolation theorem for ω1ω-logic, which considers interpolation with respect to the language symbols, the quantifiers, the identity, and countably infinite conjunction and disjunction.

Style APA, Harvard, Vancouver, ISO itp.

10

Wild, Marcel. "The many benefits of putting stack filters into disjunctive or conjunctive normal form". Discrete Applied Mathematics 149, nr 1-3 (sierpień 2005): 174–91. http://dx.doi.org/10.1016/j.dam.2004.06.027.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

11

Gorbenko, Anna, i Vladimir Popov. "On Starting Population Selection for GSAT". Applied Mechanics and Materials 365-366 (sierpień 2013): 190–93. http://dx.doi.org/10.4028/www.scientific.net/amm.365-366.190.

Pełny tekst źródła

Streszczenie:

GSAT is a well-known satisfiability search algorithm for conjunctive normal forms. GSAT uses some random functions. One of such functions is a function of starting population of truth assignments for the variables of conjunctive normal form. In this paper, we consider a method of artificial physics optimization for computing a function of starting population.

Style APA, Harvard, Vancouver, ISO itp.

12

Woodruff, David P. "Technical Perspective". ACM SIGMOD Record 51, nr 1 (31.05.2022): 86. http://dx.doi.org/10.1145/3542700.3542720.

Pełny tekst źródła

Streszczenie:

Model counting is the problem of approximately counting the number |Sol(Φ)| of satisfying assignments to a given model Φ, which could, for example, be a formula in conjunctive normal form (CNF) or a formula in disjunctive normal form (DNF).

Style APA, Harvard, Vancouver, ISO itp.

13

NI, TIAN-JIA, i ZHI-YING WEN. "SELF-SIMILARITY OF SATISFIABLE BOOLEAN EXPRESSIONS DECIPHERED IN TERMS OF GRAPH DIRECTED ITERATED FUNCTION SYSTEMS". Fractals 16, nr 04 (grudzień 2008): 305–15. http://dx.doi.org/10.1142/s0218348x0800406x.

Pełny tekst źródła

Streszczenie:

The decision problem of satisfiability of Boolean expression in k-conjunctive normal form (kSAT) is a typical NP-complete problem. In this paper, by mapping the whole Boolean expressions in k-conjunctive normal form onto a unit hypercube, we visualize the problem space of kSAT. The pattern of kSAT is shown to have self-similarity which can be deciphered in terms of graph directed iterated function system. We provide that the Hausdorff dimension of the pattern of kSAT is equal to the box-counting dimension and increases with k. This suggests that the time complexity of kSAT increases with k.

Style APA, Harvard, Vancouver, ISO itp.

14

WU, WANGMING. "COMMUTATIVE IMPLICATIONS ON COMPLETE LATTICES". International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems 02, nr 03 (wrzesień 1994): 333–41. http://dx.doi.org/10.1142/s0218488594000274.

Pełny tekst źródła

Streszczenie:

This paper is devoted to the investigation of commutative implications on a complete lattice L. It is proved that the disjunctive normal form (DNF) of a linguistic composition * is included in the conjunctive normal form (CNF) of that *, i.e., DNF(*) ≤ CNF(*) holds, for a special family of t-norms, t-conorms and negations induced by commutative implications.

Style APA, Harvard, Vancouver, ISO itp.

15

Cheremisinova, L. D., i D. Ya Novikov. "Formal verification with functional indeterminacy on the basis of satisfiability testing of the conjunctive normal form". Automatic Control and Computer Sciences 44, nr 1 (luty 2010): 1–10. http://dx.doi.org/10.3103/s0146411610010013.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

16

Casillas, Jorge, Pedro Martínez i Alicia D. Benítez. "Learning consistent, complete and compact sets of fuzzy rules in conjunctive normal form for regression problems". Soft Computing 13, nr 5 (2.09.2008): 451–65. http://dx.doi.org/10.1007/s00500-008-0361-5.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

17

López-Medina, Marco A., J. Raymundo Marcial-Romero, Guillermo De Ita Luna i José A. Hernández. "A method for counting models on grid Boolean formulas1". Journal of Intelligent & Fuzzy Systems 42, nr 5 (31.03.2022): 4719–26. http://dx.doi.org/10.3233/jifs-219259.

Pełny tekst źródła

Streszczenie:

We present a novel algorithm based on combinatorial operations on lists for computing the number of models on two conjunctive normal form Boolean formulas whose restricted graph is represented by a grid graph Gm,n. We show that our algorithm is correct and its time complexity is O ( t · 1 . 618 t + 2 + t · 1 . 618 2 t + 4 ) , where t = n · m is the total number of vertices in the graph. For this class of formulas, we show that our proposal improves the asymptotic behavior of the time-complexity with respect of the current leader algorithm for counting models on two conjunctive form formulas of this kind.

Style APA, Harvard, Vancouver, ISO itp.

18

Chen, Wenxiang, Darrell Whitley, Adele Howe i Brian Goldman. "Stochastic Local Search over Minterms on Structured SAT Instances". Proceedings of the International Symposium on Combinatorial Search 7, nr 1 (1.09.2021): 125–26. http://dx.doi.org/10.1609/socs.v7i1.18403.

Pełny tekst źródła

Streszczenie:

We observed that Conjunctive Normal Form (CNF) encodings of structured SAT instances often have a set of consecutive clauses defined over a small number of Boolean variables. To exploit the pattern, we propose a transformation of CNF to an alternative representation, Conjunctive Minterm Canonical Form (CMCF). The transformation is a two-step process: CNF clauses are first partitioned into disjoint subsets such that each subset contains CNF clauses with shared Boolean variables. CNF clauses in each subset are then replaced by Minterm Canonical Form (i.e., partial solutions), which is found by enumeration. We show empirically that a simple Stochastic Local Search (SLS) solver based on CMCF can consistently achieve a higher success rate using fewer evaluations than the SLS solver WalkSAT on two representative classes of structured SAT problems.

Style APA, Harvard, Vancouver, ISO itp.

19

Novikov, D. Ya, i L. D. Cheremisinova. "Analysis of the implementability of descriptions with functional indeterminacy based on the verification of conjunctive normal form satisfiability". Automatic Control and Computer Sciences 45, nr 4 (sierpień 2011): 206–17. http://dx.doi.org/10.3103/s0146411611040055.

Pełny tekst źródła

Style APA, Harvard, Vancouver, ISO itp.

20

SASAKI, KATSUMI. "FORMULAS IN MODAL LOGIC S4". Review of Symbolic Logic 3, nr 4 (13.09.2010): 600–627. http://dx.doi.org/10.1017/s1755020310000043.

Pełny tekst źródła

Streszczenie:

Here, we provide a detailed description of the mutual relation of formulas with finite propositional variables p1, …, pm in modal logic S4. Our description contains more information on S4 than those given in Shehtman (1978) and Moss (2007); however, Shehtman (1978) also treated Grzegorczyk logic and Moss (2007) treated many other normal modal logics. Specifically, we construct normal forms, which behave like the principal conjunctive normal forms in the classical propositional logic. The results include finite and effective methods to find a normal form equivalent to a given formula A by clarifying the behavior of connectives and giving a finite method to list all exact models.

Style APA, Harvard, Vancouver, ISO itp.

21

Selezneva, Svetlana N. "On bijunctive predicates over a finite set". Discrete Mathematics and Applications 29, nr 1 (25.02.2019): 49–58. http://dx.doi.org/10.1515/dma-2019-0006.

Pełny tekst źródła

Streszczenie:

Abstract The paper is concerned with representations of predicates over a finite set in the form of generalized conjunctive normal forms (GCNF). Properties of predicates GCNF are found which are preserved by some majority function. Such predicates are called generalized bijunctive predicates. These properties are used to construct new faster polynomial algorithms for the generalized satisfiability problem in the case when some majority function preserves all the original predicates.

Style APA, Harvard, Vancouver, ISO itp.

22

Selezneva, Svetlana N. "On weak positive predicates over a finite set". Discrete Mathematics and Applications 30, nr 3 (25.06.2020): 203–13. http://dx.doi.org/10.1515/dma-2020-0019.

Pełny tekst źródła

Streszczenie:

AbstractPredicates that are preserved by a semi-lattice function are considered. These predicates are called weak positive. A representation of these predicates are proposed in the form of generalized conjunctive normal forms (GCNFs). Properties of GCNFs of these predicates are obtained. Based on the properties obtained, more efficient polynomial-time algorithms are proposed for solving the generalized satisfiability problem in the case when all initial predicates are preserved by a certain semi-lattice function.

Style APA, Harvard, Vancouver, ISO itp.

23

ARECES, CARLOS, i EZEQUIEL ORBE. "SYMMETRIES IN MODAL LOGICS". Bulletin of Symbolic Logic 21, nr 4 (grudzień 2015): 373–401. http://dx.doi.org/10.1017/bsl.2015.31.

Pełny tekst źródła

Streszczenie:

AbstractIn this paper we develop the theoretical foundations to exploit symmetries in modal logics. We generalize the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas using the framework provided by coinductive modal models introduced in [5]. Hence, the results apply to a wide class of modal logics including, for example, hybrid logics. We present two graph constructions that enable the reduction of symmetry detection in modal formulas to the graph automorphism detection problem, and we evaluate the graph constructions on modal benchmarks.

Style APA, Harvard, Vancouver, ISO itp.

24

Dudek, Jeffrey, Vu Phan i Moshe Vardi. "ADDMC: Weighted Model Counting with Algebraic Decision Diagrams". Proceedings of the AAAI Conference on Artificial Intelligence 34, nr 02 (3.04.2020): 1468–76. http://dx.doi.org/10.1609/aaai.v34i02.5505.

Pełny tekst źródła

Streszczenie:

We present an algorithm to compute exact literal-weighted model counts of Boolean formulas in Conjunctive Normal Form. Our algorithm employs dynamic programming and uses Algebraic Decision Diagrams as the main data structure. We implement this technique in ADDMC, a new model counter. We empirically evaluate various heuristics that can be used with ADDMC. We then compare ADDMC to four state-of-the-art weighted model counters (Cachet, c2d, d4, and miniC2D) on 1914 standard model counting benchmarks and show that ADDMC significantly improves the virtual best solver.

Style APA, Harvard, Vancouver, ISO itp.

25

MONFROGLIO, ANGELO. "NEURAL NETWORKS AND LINEAR PROGRAMMING FOR THE SATISFIABILITY PROBLEM". International Journal of Neural Systems 09, nr 01 (luty 1999): 11–25. http://dx.doi.org/10.1142/s0129065799000034.

Pełny tekst źródła

Streszczenie:

First a Linear Programming formulation is considered for the satisfiability problem, in particular for the satisfaction of a Conjunctive Normal Form in the Propositional Calculus and the Simplex algorithm for solving the optimization problem. The use of Recurrent Neural Networks is then described for choosing the best pivot positions and greatly improving the algorithm performance. The result of hard cases testing is reported and shows that the technique can be useful even if it requires a huge amount of size for the constraint array and Neural Network Data Input.

Style APA, Harvard, Vancouver, ISO itp.

26

Zeng, Wei Peng, Li Sha Cai, Er Min Lin i Guo Huang. "New Methods for Deriving All Minimal Diagnostic Using Satisfiability Algorithms". Applied Mechanics and Materials 543-547 (marzec 2014): 899–903. http://dx.doi.org/10.4028/www.scientific.net/amm.543-547.899.

Pełny tekst źródła

Streszczenie:

In the model-based diagnosis reasoning, diagnosis in two steps,they are generating all minimal conflict sets of conflict identification and Generate all the minimal hitting sets of candidate generation.In this paper, we propose new method based on SAT solver generates all minimal diagnostic.Firstly the normal behavior,system model and obtained observations are described in conjunctive normal form.,then all related clauses of Pending diagnostic system put into SAT solvers. The decision circuit failure problem is converted to satisfiability problem. Hence combine CSSE-tree for solving minimal diagnostic.It can determine the point of failure without first solving the conflict set and then with hitting set algorithm.A method is presented to directly slove the minimum fault sets,which is quite different from the traditional model-based diagnosis.The diagnosis is only finished in one step.

Style APA, Harvard, Vancouver, ISO itp.

27

Heule, Marijn, Matti Järvisalo, Florian Lonsing, Martina Seidl i Armin Biere. "Clause Elimination for SAT and QSAT". Journal of Artificial Intelligence Research 53 (26.06.2015): 127–68. http://dx.doi.org/10.1613/jair.4694.

Pełny tekst źródła

Streszczenie:

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of various computationally hard problems can be efficiently solved. This success has been achieved through several breakthroughs in practical implementations of decision procedures for SAT and QSAT, that is, in SAT and QSAT solvers. Here, simplification techniques for conjunctive normal form (CNF) for SAT and for prenex conjunctive normal form (PCNF) for QSAT---the standard input formats of SAT and QSAT solvers---have recently proven very effective in increasing solver efficiency when applied before (i.e., in preprocessing) or during (i.e., in inprocessing) satisfiability search. In this article, we develop and analyze clause elimination procedures for pre- and inprocessing. Clause elimination procedures form a family of (P)CNF formula simplification techniques which remove clauses that have specific (in practice polynomial-time) redundancy properties while maintaining the satisfiability status of the formulas. Extending known procedures such as tautology, subsumption, and blocked clause elimination, we introduce novel elimination procedures based on asymmetric variants of these techniques, and also develop a novel family of so-called covered clause elimination procedures, as well as natural liftings of the CNF-level procedures to PCNF. We analyze the considered clause elimination procedures from various perspectives. Furthermore, for the variants not preserving logical equivalence under clause elimination, we show how to reconstruct solutions to original CNFs from satisfying assignments to simplified CNFs, which is important for practical applications for the procedures. Complementing the more theoretical analysis, we present results on an empirical evaluation on the practical importance of the clause elimination procedures in terms of the effect on solver runtimes on standard real-world application benchmarks. It turns out that the importance of applying the clause elimination procedures developed in this work is empirically emphasized in the context of state-of-the-art QSAT solving.

Style APA, Harvard, Vancouver, ISO itp.

28

Elffers, Jan, i Jakob Nordstrm. "A Cardinal Improvement to Pseudo-Boolean Solving". Proceedings of the AAAI Conference on Artificial Intelligence 34, nr 02 (3.04.2020): 1495–503. http://dx.doi.org/10.1609/aaai.v34i02.5508.

Pełny tekst źródła

Streszczenie:

Pseudo-Boolean solvers hold out the theoretical potential of exponential improvements over conflict-driven clause learning (CDCL) SAT solvers, but in practice perform very poorly if the input is given in the standard conjunctive normal form (CNF) format. We present a technique to remedy this problem by recovering cardinality constraints from CNF on the fly during search. This is done by collecting potential building blocks of cardinality constraints during propagation and combining these blocks during conflict analysis. Our implementation has a non-negligible but manageable overhead when detection is not successful, and yields significant gains for some SAT competition and crafted benchmarks for which pseudo-Boolean reasoning is stronger than CDCL. It also boosts performance for some native pseudo-Boolean formulas where this approach helps to improve learned constraints.

Style APA, Harvard, Vancouver, ISO itp.

29

Žufan, Petr, i Michal Bidlo. "Advances in Evolutionary Optimization of Quantum Operators". MENDEL 27, nr 2 (21.12.2021): 12–22. http://dx.doi.org/10.13164/mendel.2021.2.012.

Pełny tekst źródła

Streszczenie:

A comparative study is presented regarding the evolutionary design of quantum operators in the form of unitary matrices.A comparative study is presented regarding the evolutionary design of quantum operators in the form of unitary matrices. Three existing techniques (representations) which allow generating unitary matrices are used in various evolutionary algorithms in order to optimize their coefficients. The objective is to obtain as precise quantum operators (the resulting unitary matrices) as possible for given quantum transformations. Ordinary evolution strategy, self-adaptive evolution strategy and differential evolution are applied with various settings as the optimization algorithms for the quantum operators. These algorithms are evaluated on the tasks of designing quantum operators for the 3-qubit and 4-qubit maximum amplitude detector and a solver of a logic function of three variables in conjunctive normal form. These tasks require unitary matrices of various sizes. It will be demonstrated that the self-adaptive evolution strategy and differential evolution are able to produce remarkably better results than the ordinary evolution strategy. Moreover, the results can be improved by selecting a proper settings for the evolution as presented by a comparative evaluation.

Style APA, Harvard, Vancouver, ISO itp.

30

Liu, Xin. "Conflict-Driven Learning in Test Pattern Generation". Advanced Materials Research 301-303 (lipiec 2011): 1089–92. http://dx.doi.org/10.4028/www.scientific.net/amr.301-303.1089.

Pełny tekst źródła

Streszczenie:

SAT-based automatic test pattern generation (ATPG) is built on a SAT-solver, which can be scalable is that it is able to take into account the information of high-level structure of formulas. Paper analyzes specific structure of circuit instances where correlations among signals have been established. This analysis is a heuristic learning method by earlier detecting assignment conflicts. Reconvergent fanout is a fundamental cause of the difficulty in testing generation, because they introduce dependencies in the values that can be assigned to nodes. Paper exploits reconvergent fanout analysis of circuit to gather information about local signal correlation through BDD learning, and then used the learned information in the conjunctive normal form (CNF) clauses to restrict and focus the overall search space of test pattern generation. The experimental results demonstrate the effectiveness of these learning techniques.

Style APA, Harvard, Vancouver, ISO itp.

31

Zhi, Weifeng, Xiang Wang, Buyue Qian, Patrick Butler, Naren Ramakrishnan i Ian Davidson. "Clustering with Complex Constraints — Algorithms and Applications". Proceedings of the AAAI Conference on Artificial Intelligence 27, nr 1 (30.06.2013): 1056–62. http://dx.doi.org/10.1609/aaai.v27i1.8663.

Pełny tekst źródła

Streszczenie:

Clustering with constraints is an important and developing area. However, most work is confined to conjunctions of simple together and apart constraints which limit their usability. In this paper, we propose a new formulation of constrained clustering that is able to incorporate not only existing types of constraints but also more complex logical combinations beyond conjunctions. We first show how any statement in conjunctive normal form (CNF) can be represented as a linear inequality. Since existing clustering formulations such as spectral clustering cannot easily incorporate these linear inequalities, we propose a quadratic programming (QP) clustering formulation to accommodate them. This new formulation allows us to have much more complex guidance in clustering. We demonstrate the effectiveness of our approach in two applications on text and personal information management. We also compare our algorithm against existing constrained spectral clustering algorithm to show its efficiency in computational time.

Style APA, Harvard, Vancouver, ISO itp.

32

Ali, Mumtaz, i Osman Hasan. "SAT Based Fitness Scoring for Digital Circuit Evolution". Journal of Circuits, Systems and Computers 27, nr 06 (22.02.2018): 1850099. http://dx.doi.org/10.1142/s0218126618500998.

Pełny tekst źródła

Streszczenie:

Evolutionary computation uses Darwinian principles to find solutions from a given search space and forms the basis for evolving digital circuits. One of the most computationally expensive steps in evolutionary computation is the comparison of the candidate circuit or chromosome with the target truth table. We propose to use a satisfiability solver, to improve upon the efficiency of this process, which is traditionally done using exhaustive simulation. The paper presents an implementation of the satisfiability solver, which is in turn used to develop a digital circuit evolution methodology based on the principles of cartesian genetic programming. The proposed methodology performs better, in terms of speed of design space exploration, for circuits whose behavior can be expressed compactly in terms of conjunctive normal form clauses. For illustration purposes, the proposed methodology has been used to evolve various commonly used digital circuits and a few benchmarks.

Style APA, Harvard, Vancouver, ISO itp.

33

Giunchiglia, E., M. Narizzano i A. Tacchella. "Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas". Journal of Artificial Intelligence Research 26 (17.08.2006): 371–416. http://dx.doi.org/10.1613/jair.1959.

Pełny tekst źródła

Streszczenie:

Resolution is the rule of inference at the basis of most procedures for automated reasoning. In these procedures, the input formula is first translated into an equisatisfiable formula in conjunctive normal form (CNF) and then represented as a set of clauses. Deduction starts by inferring new clauses by resolution, and goes on until the empty clause is generated or satisfiability of the set of clauses is proven, e.g., because no new clauses can be generated. In this paper, we restrict our attention to the problem of evaluating Quantified Boolean Formulas (QBFs). In this setting, the above outlined deduction process is known to be sound and complete if given a formula in CNF and if a form of resolution, called ``Q-resolution'', is used. We introduce Q-resolution on terms, to be used for formulas in disjunctive normal form. We show that the computation performed by most of the available procedures for QBFs --based on the Davis-Logemann-Loveland procedure (DLL) for propositional satisfiability-- corresponds to a tree in which Q-resolution on terms and clauses alternate. This poses the theoretical bases for the introduction of learning, corresponding to recording Q-resolution formulas associated with the nodes of the tree. We discuss the problems related to the introduction of learning in DLL based procedures, and present solutions extending state-of-the-art proposals coming from the literature on propositional satisfiability. Finally, we show that our DLL based solver extended with learning, performs significantly better on benchmarks used in the 2003 QBF solvers comparative evaluation.

Style APA, Harvard, Vancouver, ISO itp.

34

WOLFMAN, STEVEN A., i DANIEL S. WELD. "Combining linear programming and satisfiability solving for resource planning". Knowledge Engineering Review 16, nr 1 (marzec 2001): 85–99. http://dx.doi.org/10.1017/s0269888901000017.

Pełny tekst źródła

Streszczenie:

Compilation to Boolean satisfiability has become a powerful paradigm for solving artificial intelligence problems. However, domains that require metric reasoning cannot be compiled efficiently to satisfiability even if they would otherwise benefit from compilation. We address this problem by combining techniques from the artificial intelligence and operations research communities. In particular, we introduce the LCNF (Linear Conjunctive Normal Form) representation that combines propositional logic with metric constraints. We present LPSAT (Linear Programming plus SATisfiability), an engine that solves LCNF problems by interleaving calls to an incremental Simplex algorithm with systematic satisfaction methods. We explore several techniques for enhancing LPSAT's efficiency and expressive power by adjusting the interaction between the satisfiability and linear programming components of LPSAT. Next, we describe a compiler that converts metric resource planning problems into LCNF for processing by LPSAT. Finally, the experimental section of the paper explores several optimisations to LPSAT, including learning from constraint failure and randomised cutoffs.

Style APA, Harvard, Vancouver, ISO itp.

35

Algazy, Kunbolat, Kairat Sakan i Nursulu Kapalova. "Evaluation of the strength and performance of a new hashing algorithm based on a block cipher". International Journal of Electrical and Computer Engineering (IJECE) 13, nr 3 (1.06.2023): 3124. http://dx.doi.org/10.11591/ijece.v13i3.pp3124-3130.

Pełny tekst źródła

Streszczenie:

The article evaluates the reliability of the new HBC-256 hashing algorithm. To study the cryptographic properties, the algorithm was implemented in software using Python and C programming languages. Also, for the algebraic analysis of the HBC-256 algorithm, a system of Boolean equations was built for one round using the Transalg tool. The program code that implements the hashing algorithm was converted into a software program for generating equations. As a result, one round of the compression function was described as conjunctive normal form (CNF) using 82,533 equations and 16,609 variables. To search for a collision, the satisfiability (SAT) problem solver Lingeling was used, including a version with the possibility of parallel computing. It is shown that each new round doubles the number of equations and variables, and the time to find the solution will grow exponentially. Therefore, it is not possible to find solutions for the full HBC256 hash function.

Style APA, Harvard, Vancouver, ISO itp.

36

Plyusnin, Nikolay. "Tunable logic of complex variables and quantum networks on its basis". Robotics and Technical Cybernetics 10, nr 4 (grudzień 2022): 267–74. http://dx.doi.org/10.31776/rtcj.10404.

Pełny tekst źródła

Streszczenie:

Continuous - additive-multiplicative (AM) logic is considered, in which logical operations are replaced by algebraic operations («×» and «+») or operations with vectors, and binary variables «0» and «1» are replaced by continuous scalar ones («0- 1») or complex variables. To build this logic, a continuous analogue of the canonical form of Boolean logic is used in the form of a perfect disjunctive or conjunctive normal form (KAM logic). A feature of KAM logic is a continuous dependence on input variables and a potential variety of continuous logic functions. Based on the previously proposed «fuzzy» (distributed) continuous function, in the form of a superposition of «clear» functions, and the tunable QAM element circuit that implements it, this element is generalized to a network QAM element with several tunable outputs. The multiplication functions in this QAM element can be performed using a known memristor, which can be replaced by a memtransistor based on a field effect transistor. In quantum QAM networks, these elements are, respectively: «k-memristor» and «k-memtransistor». One of the options for a k-memtransistor is a composite hybrid spin-field-effect transistor based on a planar spin valve with magnetic memory and a field-effect transistor with a ferroelectric memory. It is noted that the main technological problem of quantum QAM networks based on such a hybrid spin transistor is the creation of planar conducting and ferromagnetic elements based on ultrathin metallic and ferromagnetic films on silicon.

Style APA, Harvard, Vancouver, ISO itp.

37

Cepek, O., S. Gursky i P. Kucera. "On Minimum Representations of Matched Formulas". Journal of Artificial Intelligence Research 51 (23.12.2014): 707–23. http://dx.doi.org/10.1613/jair.4517.

Pełny tekst źródła

Streszczenie:

A Boolean formula in conjunctive normal form (CNF) is called matched if the system of sets of variables which appear in individual clauses has a system of distinct representatives. Each matched CNF is trivially satisfiable (each clause can be satisfied by its representative variable). Another property which is easy to see, is that the class of matched CNFs is not closed under partial assignment of truth values to variables. This latter property leads to a fact (proved here) that given two matched CNFs it is co-NP complete to decide whether they are logically equivalent. The construction in this proof leads to another result: a much shorter and simpler proof of the fact that the Boolean minimization problem for matched CNFs is a complete problem for the second level of the polynomial hierarchy. The main result of this paper deals with the structure of clause minimum CNFs. We prove here that if a Boolean function f admits a representation by a matched CNF then every clause minimum CNF representation of f is matched.

Style APA, Harvard, Vancouver, ISO itp.

38

GOERDT, ANDREAS. "On Random Betweenness Constraints". Combinatorics, Probability and Computing 19, nr 5-6 (5.10.2010): 775–90. http://dx.doi.org/10.1017/s0963548310000313.

Pełny tekst źródła

Streszczenie:

Ordering constraints are formally analogous to instances of the satisfiability problem in conjunctive normal form, but instead of a boolean assignment we consider a linear ordering of the variables in question. A clause becomes true given a linear ordering if and only if the relative ordering of its variables obeys the constraint considered.The naturally arising satisfiability problems are NP-complete for many types of constraints. We look at random ordering constraints. Previous work of the author shows that there is a sharp unsatisfiability threshold for certain types of constraints. The value of the threshold, however, is essentially undetermined. We pursue the problem of approximating the precise value of the threshold. We show that random instances of the betweenness constraint are satisfiable with high probability if the number of randomly picked clauses is ≤0.92n, where n is the number of variables considered. This improves the previous bound, which is <0.82n random clauses. The proof is based on a binary relaxation of the betweenness constraint and involves some ideas not used before in the area of random ordering constraints.

Style APA, Harvard, Vancouver, ISO itp.

39

Qiu, Zehang, Peng Xiao i Oanh Nguyen. "Construction of Data Resource Sharing Platform in College Students’ Ideological and Political Education Based on Deep Learning". Wireless Communications and Mobile Computing 2022 (15.07.2022): 1–10. http://dx.doi.org/10.1155/2022/2905887.

Pełny tekst źródła

Streszczenie:

At present, the irrational allocation of IPE (ideological and political education) resources in universities reflects the dilemma of university’s control of university students’ IPE system. In order to make educational big data really useful to us and really promote the sharing of educational resources and improve the utilization rate of resources, this paper discusses the construction of data resource sharing platform for college students in IPE field based on DL (Deep learning) based on the characteristics and existing problems of educational big data. Based on DL, the collected data are parameterized, the matching algorithm parameters are determined, the dynamic data sample subset is incrementally reduced, the discernibility matrix and logical analytic formula are established, the conjunctive normal form is obtained through calculation, and the kernel attribute is introduced into each conjunctions to realize incremental mining of dynamic data. The results show that the model in this paper achieves the best classification effect on six samples, with an average classification accuracy of 88.81%. The results show that the comprehensive shared data matching algorithm based on DL can realize the matching in a short time, and the matching process has high stability.

Style APA, Harvard, Vancouver, ISO itp.

40

Sahai, Tuhin, Anurag Mishra, Jose Miguel Pasini i Susmit Jha. "Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms". Proceedings of the AAAI Conference on Artificial Intelligence 34, nr 02 (3.04.2020): 1627–35. http://dx.doi.org/10.1609/aaai.v34i02.5524.

Pełny tekst źródła

Streszczenie:

Given a Boolean formula ϕ(x) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly e clauses, for all values of e. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the hardness of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.

Style APA, Harvard, Vancouver, ISO itp.

41

Feldman, Alexander, Ingo Pill, Franza Wotawa, Ion Matei i Johan De Kleer. "Efficient Model-Based Diagnosis of Sequential Circuits". Proceedings of the AAAI Conference on Artificial Intelligence 34, nr 03 (3.04.2020): 2814–21. http://dx.doi.org/10.1609/aaai.v34i03.5670.

Pełny tekst źródła

Streszczenie:

In Model-Based Diagnosis (MBD), we concern ourselves with the health and safety of physical and software systems. Although we often use different knowledge representations and algorithms, some tools like satisfiability (SAT) solvers and temporal logics, are used in both domains. In this paper we introduce Finite Trace Next Logic (FTNL) models of sequential circuits and propose an enhanced algorithm for computing minimal-cardinality diagnoses. Existing state-of-the-art satisfiability algorithms for minimal diagnosis use Sorting Networks (SNs) for constraining the cardinality of the diagnostic candidates. In our approach we exploit Multi-Operand Adders (MOAs). Based on extensive tests with ISCAS-89 circuits, we found that MOAs enable Conjunctive Normal Form (CNF) encodings that are significantly more compact. These encodings lead to 19.7 to 67.6 times fewer variables and 18.4 to 62 times fewer clauses. For converting an FTNL model to CNF, we could achieve a speed-up ranging from 6.2 to 22.2. Using SNs fosters 3.4 to 5.5 times faster on-line satisfiability checking though. This makes MOAs preferable for applications where RAM and off-line time are more limited than on-line CPU time.

Style APA, Harvard, Vancouver, ISO itp.

42

Itsykson, Dmitry, Alexander Okhotin i Vsevolod Oparin. "Computational and Proof Complexity of Partial String Avoidability". ACM Transactions on Computation Theory 13, nr 1 (marzec 2021): 1–25. http://dx.doi.org/10.1145/3442365.

Pełny tekst źródła

Streszczenie:

The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

Style APA, Harvard, Vancouver, ISO itp.

43

OSTROWSKI, RICHARD, i LIONEL PARIS. "FROM XSAT TO SAT BY EXHIBITING BOOLEAN FUNCTIONS". International Journal on Artificial Intelligence Tools 18, nr 05 (październik 2009): 783–99. http://dx.doi.org/10.1142/s0218213009000408.

Pełny tekst źródła

Streszczenie:

Given a Boolean formula in conjunctive normal form (CNF), the Exact Satisfiability problem (XSAT), a variant of the Satisfiability problem (SAT), consists in finding an assignment to the variables such that each clause contains exactly one satisfied literal. Best algorithms to solve this problem run in [Formula: see text] ([Formula: see text] for X3SAT). Another possibility is to transform each clause in a set of equivalent clauses for the Satisfiability problem and to use modern and powerful solvers (zChaff, Berkmin, MiniSat, RSat etc.) to find such truth assignment. In this paper we introduce three new encodings from XSAT instances to SAT instances that lead to a lot of structural information (equivalency gates and and gates) which is naturally hidden in the pairwise transformation. Some solvers (lsat,march_dl,eqsatz) can take into account this kinds of structural information to make simplifications as pretreatment and speed-up the resolution. Then we show the interest of dealing with the XSAT formalism by introducing an encoding of binary CSP and graph coloring problem into XSAT instances. Preliminary results on real-world binary CSP and graph coloring problem show the importance of exhibiting equivalencies for the XSAT problem.

Style APA, Harvard, Vancouver, ISO itp.

44

Ohta, S. "CNF-SAT modelling for banyan-type networks and its application for assessing the rearrangeability". Journal of Physics: Conference Series 2090, nr 1 (1.11.2021): 012133. http://dx.doi.org/10.1088/1742-6596/2090/1/012133.

Pełny tekst źródła

Streszczenie:

Abstract A banyan-type network is a switching network, which is constructed by placing unit switches with two inputs and two outputs in s (s > 1) stages. In each stage, 2 n – 1 (n > 1) unit switches are aligned. Past studies conjecture that this network becomes rearrangeable when s ≥ 2n-1. Although a considerable number of theoretical analyses have been done, the rearrangeability of the banyan-type network with 2n – 1 or more stages is not completely proved. As a tool to assess the rearrangeability, this study presents a CNF-SAT (conjunctive normal form - satisfiability) modelling scheme for banyan-type networks. In the proposed scheme, the routing is formulated to a SAT problem represented in CNF. By feeding the problem to a SAT solver, it is found whether the problem is satisfiable or unsatisfiable. If the problem is unsatisfiable for a certain request, the network is not rearrangeable. By contrast, if the problem is satisfiable for any requests, the network is rearrangeable. This study applies the CNF-SAT modelling scheme to various configurations of 2n – 1 stage banyan-type networks. These networks are assessed for rearrangeability by solving the SAT problems. The proposed method will be helpful to conduct future theoretical studies on banyan-type networks.

Style APA, Harvard, Vancouver, ISO itp.

45

Agrawal, Nishant. "Automatic Test Pattern Generation using Grover’s Algorithm". International Journal for Research in Applied Science and Engineering Technology 9, nr VI (14.06.2021): 2373–79. http://dx.doi.org/10.22214/ijraset.2021.34837.

Pełny tekst źródła

Streszczenie:

Quantum computing is an exciting new field in the intersection of computer science, physics and mathematics. It refines the central concepts from Quantum mechanics into its least difficult structures, peeling away the complications from the physical world. Any combinational circuit that has only one stuck at fault can be tested by applying a set of inputs that drive the circuit to verify the output response. The outputs of that circuit will be different from the one desired if the faults exist. This project describes a method of generating test patterns using the Boolean satisfaction method. First, the Boolean formula is constructed to express the Boolean difference between a fault-free circuit and a faulty circuit. Second, the Boolean satisfaction algorithm is applied to the formula in the previous step. The Grover algorithm is used to solve the Boolean satisfaction problem. The Boolean Satisfiability problem for Automatic Test Pattern Generation(ATPG) is implemented on IBM Quantum Experience. The Python program initially generates the boolean expression from the file and converts it into Conjunctive Normal Form(CNF) which is passed on to Grover Oracle and runs on IBM simulator and produces excellent results on combinational circuits for test pattern generation with a quadratic speedup. Grover’s Algorithm on this problem has a run time of O(√N).

Style APA, Harvard, Vancouver, ISO itp.

46

Łuczak, Piotr, Przemysław Kucharski, Tomasz Jaworski, Izabela Perenc, Krzysztof Ślot i Jacek Kucharski. "Boosting Intelligent Data Analysis in Smart Sensors by Integrating Knowledge and Machine Learning". Sensors 21, nr 18 (14.09.2021): 6168. http://dx.doi.org/10.3390/s21186168.

Pełny tekst źródła

Streszczenie:

The presented paper proposes a hybrid neural architecture that enables intelligent data analysis efficacy to be boosted in smart sensor devices, which are typically resource-constrained and application-specific. The postulated concept integrates prior knowledge with learning from examples, thus allowing sensor devices to be used for the successful execution of machine learning even when the volume of training data is highly limited, using compact underlying hardware. The proposed architecture comprises two interacting functional modules arranged in a homogeneous, multiple-layer architecture. The first module, referred to as the knowledge sub-network, implements knowledge in the Conjunctive Normal Form through a three-layer structure composed of novel types of learnable units, called L-neurons. In contrast, the second module is a fully-connected conventional three-layer, feed-forward neural network, and it is referred to as a conventional neural sub-network. We show that the proposed hybrid structure successfully combines knowledge and learning, providing high recognition performance even for very limited training datasets, while also benefiting from an abundance of data, as it occurs for purely neural structures. In addition, since the proposed L-neurons can learn (through classical backpropagation), we show that the architecture is also capable of repairing its knowledge.

Style APA, Harvard, Vancouver, ISO itp.

47

Kyrillidis, Anastasios, Anshumali Shrivastava, Moshe Vardi i Zhiwei Zhang. "FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints". Proceedings of the AAAI Conference on Artificial Intelligence 34, nr 02 (3.04.2020): 1552–60. http://dx.doi.org/10.1609/aaai.v34i02.5515.

Pełny tekst źródła

Streszczenie:

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XORs) are less well-studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time.To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks.

Style APA, Harvard, Vancouver, ISO itp.

48

Fang, Xing, Hongxin Zhang, Danzhi Wang, Hao Yan, Fan Fan i Lei Shu. "Algebraic Persistent Fault Analysis of SKINNY_64 Based on S_Box Decomposition". Entropy 24, nr 11 (22.10.2022): 1508. http://dx.doi.org/10.3390/e24111508.

Pełny tekst źródła

Streszczenie:

Algebraic persistent fault analysis (APFA), which combines algebraic analysis with persistent fault attacks, brings new challenges to the security of lightweight block ciphers and has received widespread attention since its introduction. Threshold Implementation (TI) is one of the most widely used countermeasures for side channel attacks. Inspired by this method, the SKINNY block cipher adopts the S_box decomposition to reduce the number of variables in the set of algebraic equations and the number of Conjunctive Normal Form (CNF) equations in this paper, thus speeding up the algebraic persistent fault analysis and reducing the number of fault ciphertexts. In our study, we firstly establish algebraic equations for full-round faulty encryption,and then analyze the relationship between the number of fault ciphertexts required and the solving time in different scenarios (decomposed S_boxes and original S_box). By comparing the two sets of experimental results, the success rate and the efficiency of the attack are greatly improved by using S_box decomposition. In this paper, We can recover the master key in a minimum of 2000s using 11 pairs of plaintext and fault ciphertext, while the key recovery cannot be done in effective time using the original S_box expression equations. At the same time, we apply S_box decomposition to another kind of algebraic persistent fault analysis, and the experimental results show that using S_box decomposition can effectively reduce the solving time and solving success rate under the same conditions.

Style APA, Harvard, Vancouver, ISO itp.

49

Semenov, Alexander, Artem Pavlenko, Daniil Chivilikhin i Stepan Kochemazov. "On Probabilistic Generalization of Backdoors in Boolean Satisfiability". Proceedings of the AAAI Conference on Artificial Intelligence 36, nr 9 (28.06.2022): 10353–61. http://dx.doi.org/10.1609/aaai.v36i9.21277.

Pełny tekst źródła

Streszczenie:

The paper proposes a probabilistic generalization of the well-known Strong Backdoor Set (SBS) concept applied to the Boolean Satisfiability Problem (SAT). We call a set of Boolean variables B a ρ-backdoor, if for a fraction of at least ρ of possible assignments of variables from B, assigning their values to variables in a Boolean formula in Conjunctive Normal Form (CNF) results in polynomially solvable formulas. Clearly, a ρ-backdoor with ρ=1 is an SBS. For a given set B it is possible to efficiently construct an (ε, δ)-approximation of parameter ρ using the Monte Carlo method. Thus, we define an (ε, δ)-SBS as such a set B for which the conclusion "parameter ρ deviates from 1 by no more than ε" is true with probability no smaller than 1 - δ. We consider the problems of finding the minimum SBS and the minimum (ε, δ)-SBS. To solve the former problem, one can use the algorithm described by R. Williams, C. Gomes and B. Selman in 2003. In the paper we propose a new probabilistic algorithm to solve the latter problem, and show that the asymptotic estimation of the worst-case complexity of the proposed algorithm is significantly smaller than that of the algorithm by Williams et al. For practical applications, we suggest a metaheuristic optimization algorithm based on the penalty function method to seek the minimal (ε, δ)-SBS. Results of computational experiments show that the use of (ε, δ)-SBSes found by the proposed algorithm allows speeding up solving of test problems related to equivalence checking and hard crafted and combinatorial benchmarks compared to state-of-the-art SAT solvers.

Style APA, Harvard, Vancouver, ISO itp.

50

Kikhtenko, N. A., N. A. Bondarenko, N. P. Bgatova, L. A. Oleynik, O. V. Poveshchenko, A. Zh Fursova i P. G. Madonov. "Investigation of Cytotoxic Effects of Recombinant Human Interferon Lambda-1 and Its Pegylated Form on Human Conjunctival Epithelial Cells". Safety and Risk of Pharmacotherapy 9, nr 4 (21.10.2021): 200–208. http://dx.doi.org/10.30895/2312-7821-2021-9-4-200-208.

Pełny tekst źródła

Streszczenie:

Currently, there are no efficacious, all-purpose antiviral medicines for the treatment of ocular surface infections caused by viruses. At the same time, type III interferons demonstrate high potency for histological barriers, such as the conjunctiva. Modification of protein molecules in native products can significantly improve their pharmacodynamic properties. Thus, it seems reasonable to develop antiviral medicines based on interferon lambda (IFN-λ1) and its pegylated form (PEG IFN-λ1).The aim of the study was to evaluate the in vitro cytotoxic effect of recombinant human IFN-λ1 and its pegylated form on Chang conjunctiva clone 1-5c-4 human conjunctival cells.Materials and methods: PEG IFN-λ1 was obtained by the electron beam immobilisation method. A normal human conjunctival cell line Chang conjunctiva clone 1-5c-4 was used for cell cultivation. The MTT test was used to assess the cytotoxic effect. Cell proliferative activity was studied by measuring microelectrode impedance. Ultrastructural changes were assessed by electron microscopy. Statistical processing was performed using the Statistica 10.0 software package.Results: IFN-λ1 (37 μg/mL) and PEG IFN-λ1 (42 μg/mL) had no significant cytotoxic effect on the human conjunctiva cell culture and the cell proliferative activity. The analysis of ultrastructural changes demonstrated that IFN-λ1 activated metabolic processes in the cells, and PEG IFN-λ1 promoted differentiation and keratinisation of epithelial cells and led to modification of the cell membrane. A ten-fold increase in IFN-λ1 and PEG IFN-λ1 concentration (to 370 μg/mL and 420 μg/mL, respectively) reduced the cell viability by 15–20% as compared to the intact control.Conclusions: the study results demonstrated that IFN-λ1 and PEG IFN-λ1 could be used as active pharmaceutical ingredients in the development of medicines for the treatment of conjunctival viral infections.

Style APA, Harvard, Vancouver, ISO itp.

Artykuły w czasopismach na temat „Conjunctive normal form”

Utwórz poprawne odniesienie w stylach APA, MLA, Chicago, Harvard i wielu innych