scholarly journals On the orthogonalization of arbitrary Boolean formulae

2005 ◽  
Vol 2005 (2) ◽  
pp. 61-74 ◽  
Author(s):  
Renato Bruni
Keyword(s):  
Normal Form ◽  
Boolean Function ◽  
General Procedure ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Reliability Theory ◽  
Satisfiability Problem ◽  
Propositional Satisfiability ◽  
Strongly Connected ◽  
Great Relevance

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.

scholarly journals Clause/Term Resolution and Learning in the Evaluation of Quantified Boolean Formulas

2006 ◽  
Vol 26 ◽  
pp. 371-416 ◽  
Author(s):  
E. Giunchiglia ◽  
M. Narizzano ◽  
A. Tacchella
Keyword(s):  
Normal Form ◽  
Automated Reasoning ◽  
Comparative Evaluation ◽  
State Of The Art ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Propositional Satisfiability ◽  
Quantified Boolean Formulas ◽  
Boolean Formulas ◽  
Input Formula

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.

Conservative reduction classes of Krom formulas

1982 ◽  
Vol 47 (1) ◽  
pp. 110-130 ◽  
Author(s):  
Stål O. Aanderaa ◽  
Egon Börger ◽  
Harry R. Lewis
Keyword(s):  
Normal Form ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Satisfiability Problem ◽  
Quantification Theory ◽  
Finite Models ◽  
Reduction Class

AbstractA Krom formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most two atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a conservative reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.

scholarly journals Interval Valued Fuzzy Soft Sets and Fuzzy Connectives

2019 ◽  
Vol 8 (4) ◽  
pp. 20-23
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Soft Set ◽  
Fuzzy Subset ◽  
Fuzzy Soft Set ◽  
Soft Sets ◽  
Fuzzy Soft Sets ◽  
Interval Valued ◽  
Fuzzy Connectives

The Article, We Learning A Few Operations Of Interval Valued Fuzzy Soft Sets Of Connectives And Give Elementary Properties Of Interval Valued Fuzzy Soft Sets Of Principal Disjunctive Normal Form And Principal Conjunctive Normal Form. 2000 Ams Subject Classification: 03f55, 08a72, 20n25. Keywords: Interval Valued Fuzzy Subset, Interval Valued Fuzzy Soft Set, And Principal Conjunctive Normal Form And Principal Disjunctive Normal Form Interval Valued Fuzzy Soft Set ‘’∧ ‘’ Operator And ‘’∨’’ Operator.

On sentences which are true of direct unions of algebras

1951 ◽  
Vol 16 (1) ◽  
pp. 14-21 ◽  
Author(s):  
Alfred Horn
Keyword(s):  
Normal Form ◽  
Wide Class ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Factor Algebra ◽  
The Matrix ◽  
Distinct Individual ◽  
Direct Union ◽  
Individual Variables ◽  
Image Position

It is well known that certain sentences corresponding to similar algebras are invariant under direct union; that is, are true of the direct union when true of each factor algebra. An axiomatizable class of similar algebras, such as the class of groups, is closed under direct union when each of its axioms is invariant. In this paper we shall determine a wide class of invariant sentences. We shall also be concerned with determining sentences which are true of a direct union provided they are true of some factor algebra. In the case where all the factor algebras are the same, a further result is obtained. In §2 it will be shown that these criteria are the only ones of their kind. Lemma 7 below may be of some independent interest.We adopt the terminology and notation of McKinsey with the exception that the sign · will be used for conjunction. Expressions of the form ∼∊, where ∊ is an equation, will be called inequalities. In accordance with the analogy between conjunction and disjunction with product and sum respectively, we shall call α1, …, αn the terms of the disjunctionand the factors of the conjunctionEvery closed sentence is equivalent to a sentence in prenez normal form,where x1, …, xm distinct individual variables, Q1, …, Qm are quantifiers, and the matrix S is an open sentence in which each of the variables x1, …, xm actually occurs. The sentence S may be written in either disjunctive normal form:where αi,j is either an equation or an inequality, or in conjunctive normal form:.

scholarly journals The Incremental Satisfiability Problem for a Two Conjunctive Normal Form

2016 ◽  
Vol 328 ◽  
pp. 31-45 ◽  
Author(s):  
Guillermo De Ita Luna ◽  
J. Raymundo Marcial-Romero ◽  
José A. Hernández
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Satisfiability Problem

COMMUTATIVE IMPLICATIONS ON COMPLETE LATTICES

1994 ◽  
Vol 02 (03) ◽  
pp. 333-341 ◽  
Author(s):  
WANGMING WU
Keyword(s):  
Normal Form ◽  
Complete Lattice ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Complete Lattices

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.

The decision problem for formulas with a small number of atomic subformulas

1973 ◽  
Vol 38 (3) ◽  
pp. 471-480 ◽  
Author(s):  
Harry R. Lewis ◽  
Warren D. Goldfarb
Keyword(s):  
Normal Form ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Disjunctive Normal Form ◽  
Principal Result ◽  
The Other ◽  
Universal Quantifiers

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.

scholarly journals On Minimum Representations of Matched Formulas

2014 ◽  
Vol 51 ◽  
pp. 707-723
Author(s):  
O. Cepek ◽  
S. Gursky ◽  
P. Kucera
Keyword(s):  
Normal Form ◽  
Boolean Function ◽  
Minimization Problem ◽  
Conjunctive Normal Form ◽  
Boolean Formula ◽  
Polynomial Hierarchy ◽  
Partial Assignment ◽  
Complete Problem ◽  
Boolean Minimization ◽  
Np Complete

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.

Sign in / Sign up

Export Citation Format

Share Document