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.

NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability

2020 ◽  
Vol 30 (7) ◽  
pp. 736-751
Author(s):  
Hans Kleine Büning ◽  
P. Wojciechowski ◽  
K. Subramani
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Principal Result ◽  
Satisfying Assignment ◽  
Boolean Formulas ◽  
Complete Procedure ◽  
Np Complete ◽  
Resolution Refutation ◽  
Original Formula ◽  
Cnf Formulas

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.

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.

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

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.

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.

The decision problem for formulas in prenex conjunctive normal form with binary disjunctions

1970 ◽  
Vol 35 (2) ◽  
pp. 210-216 ◽  
Author(s):  
M. R. Krom
Keyword(s):  
Normal Form ◽  
Positive Solution ◽  
Decision Problem ◽  
Conjunctive Normal Form ◽  
Decision Problems ◽  
First Order ◽  
Reduction Class ◽  
Image Position ◽  
Positive Integers ◽  
Order Predicate Calculus

In [8] S. J. Maslov gives a positive solution to the decision problem for satisfiability of formulas of the formin any first-order predicate calculus without identity where h, k, m, n are positive integers, αi, βi are signed atomic formulas (atomic formulas or negations of atomic formulas), and ∧, ∨ are conjunction and disjunction symbols, respectively (cf. [6] for a related solvable class). In this paper we show that the decision problem is unsolvable for formulas that are like those considered by Maslov except that they have prefixes of the form ∀x∃y1 … ∃yk∀z. This settles the decision problems for all prefix classes of formulas for formulas that are in prenex conjunctive normal form in which all disjunctions are binary (have just two terms). In our concluding section we report results on decision problems for related classes of formulas including classes of formulas in languages with identity and we describe some special properties of formulas in which all disjunctions are binary including a property that implies that any proof of our result, that a class of formulas is a reduction class for satisfiability, is necessarily indirect. Our proof is based on an unsolvable combinatorial tag problem.

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.

Closing the GAP—A 5Å Scanning Microscope

1969 ◽  
Vol 27 ◽  
pp. 6-7
Author(s):  
A. V. Crewe
Keyword(s):  
Normal Form ◽  
The Other ◽  
Resolving Power ◽  
Scanning Microscope ◽  
Conventional Microscope ◽  
Other Hand ◽  
Closing The Gap ◽  
Thermal Sources ◽  
Better Than ◽  
Transmission Microscope

We have become accustomed to differentiating between the scanning microscope and the conventional transmission microscope according to the resolving power which the two instruments offer. The conventional microscope is capable of a point resolution of a few angstroms and line resolutions of periodic objects of about 1Å. On the other hand, the scanning microscope, in its normal form, is not ordinarily capable of a point resolution better than 100Å. Upon examining reasons for the 100Å limitation, it becomes clear that this is based more on tradition than reason, and in particular, it is a condition imposed upon the microscope by adherence to thermal sources of electrons.

METHODS OF REDUCING OF LARGE BOOLEAN FORMULAS REPRESENTED IN A CONJUNCTIVE NORMAL FORM FOR DETERMINING THEIR SATISFIABILITY

2020 ◽  
Author(s):  
N.I. Gdansky ◽  
◽  
A.A. Denisov ◽  
Keyword(s):  
Normal Form ◽  
Normal Forms ◽  
Conjunctive Normal Form ◽  
Boolean Formulas

The article explores the satisfiability of conjunctive normal forms used in modeling systems.The problems of CNF preprocessing are considered.The analysis of particular methods for reducing this formulas, which have polynomial input complexity is given.

Sign in / Sign up

Export Citation Format

Share Document