A resolution calculus for MinSAT

2019 ◽  
Author(s):  
Chu-Min Li ◽  
Fan Xiao ◽  
Felip Manyà
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Logical Calculus ◽  
Elimination Algorithm ◽  
Variable Elimination ◽  
Resolution Rule ◽  
Resolution Calculus

AbstractThe logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy proposed here. We then describe an exact variable elimination algorithm for MinSAT based on that rule. Finally, we show how the results for Boolean MinSAT can be extended to solve the MinSAT problem of the multiple-valued clausal forms known as signed conjunctive normal form formulas.

scholarly journals A Resolution Method for Modal Logic S5

10.29007/1zgr ◽  
2018 ◽  
Author(s):  
Yakoub Salhi ◽  
Michael Sioutis
Keyword(s):  
Normal Form ◽  
Modal Logic ◽  
Graph Coloring ◽  
Propositional Logic ◽  
Possible Worlds ◽  
Conjunctive Normal Form ◽  
Clause Structure ◽  
Possible Worlds Semantics ◽  
Resolution Method ◽  
Resolution Rule

The aim of this work is to define a resolution method for the modal logic S5. Wefirst propose a conjunctive normal form (S5-CNF) which is mainly based on using labelsreferring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of theconjunctive normal form in propositional logic by using in the clause structure the modalconnective of necessity and labels. We show that every S5 formula can be transformedinto an S5-CNF formula using a linear encoding. Then, in order to show the suitabilityof our normal form, we describe a modeling of the problem of graph coloring. Finally, weintroduce a simple resolution method for S5, composed of three deductive rules, and weshow that it is sound and complete. Our deductive rules can be seen as adaptations ofRobinson’s resolution rule to the possible-worlds semantics.

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.

A reduction class containing formulas with one monadic predicate and one binary function symbol

1976 ◽  
Vol 41 (1) ◽  
pp. 45-49
Author(s):  
Charles E. Hughes
Keyword(s):  
Normal Form ◽  
Predicate Symbol ◽  
Conjunctive Normal Form ◽  
Function Symbol ◽  
Predicate Calculus ◽  
Binary Function ◽  
First Order ◽  
The Matrix ◽  
Reduction Class ◽  
Order Predicate Calculus

AbstractA new reduction class is presented for the satisfiability problem for well-formed formulas of the first-order predicate calculus. The members of this class are closed prenex formulas of the form ∀x∀yC. The matrix C is in conjunctive normal form and has no disjuncts with more than three literals, in fact all but one conjunct is unary. Furthermore C contains but one predicate symbol, that being unary, and one function symbol which symbol is binary.

Chapter 29. Theory of Quantified Boolean Formulas

2021 ◽  
Author(s):  
Hans Kleine Büning ◽  
Uwe Bubeck
Keyword(s):  
Normal Form ◽  
Boolean Function ◽  
Expressive Power ◽  
Modeling Language ◽  
Complex Problems ◽  
Quantified Boolean Formulas ◽  
Horn Formulas ◽  
Boolean Formulas ◽  
Function Models ◽  
Resolution Calculus

Quantified Boolean formulas (QBF) are a generalization of propositional formulas by allowing universal and existential quantifiers over variables. This enhancement makes QBF a concise and natural modeling language in which problems from many areas, such as planning, scheduling or verification, can often be encoded in a more compact way than with propositional formulas. We introduce in this chapter the syntax and semantics of QBF and present fundamental concepts. This includes normal form transformations and Q-resolution, an extension of the propositional resolution calculus. In addition, Boolean function models are introduced to describe the valuation of formulas and the behavior of the quantifiers. We also discuss the expressive power of QBF and provide an overview of important complexity results. These illustrate that the greater capabilities of QBF lead to more complex problems, which makes it interesting to consider suitable subclasses of QBF. In particular, we give a detailed look at quantified Horn formulas (QHORN) and quantified 2-CNF (Q2-CNF).

Chapter 13. Symmetry and Satisfiability

2021 ◽  
Author(s):  
Karem A. Sakallah
Keyword(s):  
Group Theory ◽  
Normal Form ◽  
Boolean Functions ◽  
Search Algorithm ◽  
Conjunctive Normal Form ◽  
Search Space ◽  
Decision Problems ◽  
Mathematical Language ◽  
Sat Solvers ◽  
Speed Up

Symmetry is at once a familiar concept (we recognize it when we see it!) and a profoundly deep mathematical subject. At its most basic, a symmetry is some transformation of an object that leaves the object (or some aspect of the object) unchanged. For example, a square can be transformed in eight different ways that leave it looking exactly the same: the identity “do-nothing” transformation, 3 rotations, and 4 mirror images (or reflections). In the context of decision problems, the presence of symmetries in a problem’s search space can frustrate the hunt for a solution by forcing a search algorithm to fruitlessly explore symmetric subspaces that do not contain solutions. Recognizing that such symmetries exist, we can direct a search algorithm to look for solutions only in non-symmetric parts of the search space. In many cases, this can lead to significant pruning of the search space and yield solutions to problems which are otherwise intractable. This chapter explores the symmetries of Boolean functions, particularly the symmetries of their conjunctive normal form (CNF) representations. Specifically, it examines what those symmetries are, how to model them using the mathematical language of group theory, how to derive them from a CNF formula, and how to utilize them to speed up CNF SAT solvers.

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.

Logic on electronic computers: a practical method for reducing expressions to conjunctive normal form

1956 ◽  
Vol 52 (2) ◽  
pp. 161-173
Author(s):  
N. A. Routledge
Keyword(s):  
Normal Form ◽  
Real Number ◽  
Electronic Computer ◽  
Propositional Calculus ◽  
Practical Method ◽  
Conjunctive Normal Form ◽  
Electronic Computers ◽  
The Given

ABSTRACTIn § 1 we introduce our system and prove a theorem about its syntax. In § 2 we recall some stock results about the propositional calculus. In § 3 we consider a method of deriving an expression from a given expression and a real number. In § 4 we use this to derive a sequence of expressions from a given expression. In § 5 this sequence is shown to be just all the terms of a conjunctive normal form of the given expression. In § 6 we note that we may not need to produce all of these terms. In § 7 we describe a practical method (suitable for a binary digital electronic computer) which results from all this, and in § 8 we attempt to explain just why this is so.

Sign in / Sign up

Export Citation Format

Share Document