Journal articles: 'Conjunctive Normal Form (CNF)'

1

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

2

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

3

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

Full text

Abstract:

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).

APA, Harvard, Vancouver, ISO, and other styles

4

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

5

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

6

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

7

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

8

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

9

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

10

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

11

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

12

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

13

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

14

Kleine Büning, Hans, P. Wojciechowski, and K. Subramani. "NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability." Mathematical Structures in Computer Science 30, no. 7 (August 2020): 736–51. http://dx.doi.org/10.1017/s096012952000016x.

Full text

Abstract:

AbstractIn this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

APA, Harvard, Vancouver, ISO, and other styles

15

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

16

Algazy, Kunbolat, Kairat Sakan, and 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, no. 3 (June 1, 2023): 3124. http://dx.doi.org/10.11591/ijece.v13i3.pp3124-3130.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

17

SUBRAMANI, K. "CASCADING RANDOM WALKS." International Journal of Foundations of Computer Science 16, no. 03 (June 2005): 599–622. http://dx.doi.org/10.1142/s0129054105003182.

Full text

Abstract:

In this paper, we discuss a simple, Monte Carlo algorithm for the problem of checking whether a Quantified Boolean Formula (QBF) in Conjunctive Normal Form (CNF), with at most two literals per clause has a model. The term k-CNF is used to describe boolean formulas in CNF, with at most k literals per clause and the problem of checking whether a given k-CNF formula is satisfiable is called the k-SAT problem. A QBF is a boolean formula, accompanied by a quantifier string which imposes a linear ordering on the variables of that formula. The problem of finding a model for a QBF formula in CNF, with at at most k literals per clause is called the QkSAT problem. The QkSAT problem is PSPACE-complete, for k≥3. However, the Q2SAT problem can be decided in polynomial time; the graph-based procedure, discussed in [1], is the first such algorithm for this problem. This procedure requires the construction of a global implication graph, corresponding to the input formula and searching for certain paths in this graph. Hence the complete set of clauses must be part of the input. We propose an incremental, randomized approach for the Q2SAT problem that is essentially local in nature, in that the complete clausal set need not be provided at any time, in the presence of a verifier. We show that the randomized algorithm can be analyzed as a one-dimensional random walk, with one reflecting barrier and one absorbing barrier. On a Q2SAT instance with m clauses on n variables, our coin-flipping algorithm runs in time O(n2 · V(m, n)), where V(m, n) is the time required to verify that a given model satisfies the formula. Additionally, if the instance is satisfiable, the probability that our algorithm fails to find a model is less than one half. The design and analysis of a randomized algorithm for a problem, is important from both the theoretical and the practical perspectives. Randomized approaches tend to be simple and elegant, thereby making the process of checking correctness, effortless as well. The randomized approach discussed in this paper lays the groundwork for analyzing a number of problems related to 2CNF formulas and directed graphs. We remark that our work in this paper is the first randomized algorithm for a class of QBFs.

APA, Harvard, Vancouver, ISO, and other styles

18

Sahai, Tuhin, Anurag Mishra, Jose Miguel Pasini, and 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, no. 02 (April 3, 2020): 1627–35. http://dx.doi.org/10.1609/aaai.v34i02.5524.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

19

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

20

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

Full text

Abstract:

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).

APA, Harvard, Vancouver, ISO, and other styles

21

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

22

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

23

To, Son, Tran Son, and Enrico Pontelli. "Conjunctive Representations in Contingent Planning: Prime Implicates Versus Minimal CNF Formula." Proceedings of the AAAI Conference on Artificial Intelligence 25, no. 1 (August 4, 2011): 1023–28. http://dx.doi.org/10.1609/aaai.v25i1.8015.

Full text

Abstract:

This paper compares in depth the effectiveness of two conjunctive belief state representations in contingent planning: prime implicates and minimal CNF, a compact form of CNF formulae, which were initially proposed in conformant planning research (To et al. 2010a; 2010b). Similar to the development of the contingent planner CNFct for minimal CNF (To et al. 2011b), the present paper extends the progression function for the prime implicate representation in (To et al. 2010b) for computing successor belief states in the presence of incomplete information to handle non-deterministic and sensing actions required in contingent planning. The idea was instantiated in a new contingent planner, called PIct, using the same AND/OR search algorithm and heuristic function as those for CNFct. The experiments show that, like CNFct, PIct performs very well in a wide range of benchmarks. The study investigates the advantages and disadvantages of the two planners and identifies the properties of each representation method that affect the performance.

APA, Harvard, Vancouver, ISO, and other styles

24

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

25

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

26

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

27

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

28

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

29

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

30

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

31

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

32

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

33

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

34

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

36

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

37

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

38

Cheremisinova, L. D., and 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, no. 1 (February 2010): 1–10. http://dx.doi.org/10.3103/s0146411610010013.

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

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

Full text

APA, Harvard, Vancouver, ISO, and other styles

40

Bansal, Avinash. "Alternative Vidhi to Conversion of Cyclic CNF->GNF." INTERNATIONAL JOURNAL OF COMPUTERS & TECHNOLOGY 3, no. 1 (August 1, 2012): 132–33. http://dx.doi.org/10.24297/ijct.v3i1b.6778.

Full text

Abstract:

In automata theory Greibach Normal Form shows that A->aV n*, where â€˜aâ€™ is terminal symbol and Vn is nonterminal symbol where * shows zero or more rates of Vn [1]. Most popular questions, conversion of following cyclic CNF into GNF are: Question 1 S->AA | a, A->SS | b Question 2 S->AB, A->BS | b, B->SA | a Question 3 S->AB, A->BS | b, B->AS | a [1] To solve these questions, we need two technical lemmas and required one or more another variable like Z1. In these questions, we have cyclic nature of production called cyclic CNF. We have modified the same rule by which we get the more reliable answer with less number of productions in right hand side without using lemmas and any another variable. This above method can be applied on all problems by which we produce the GNF.

APA, Harvard, Vancouver, ISO, and other styles

41

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

42

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

43

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

44

Novikov, D. Ya, and 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, no. 4 (August 2011): 206–17. http://dx.doi.org/10.3103/s0146411611040055.

Full text

APA, Harvard, Vancouver, ISO, and other styles

45

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

46

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

47

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

48

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

49

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

50

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

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Conjunctive Normal Form (CNF)'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles