The Monotone Satisfiability Problem with Bounded Variable Appearances

2018 ◽  
Vol 29 (06) ◽  
pp. 979-993 ◽  
Author(s):  
Andreas Darmann ◽  
Janosch Döcker ◽  
Britta Dorn
Keyword(s):  
Computational Complexity ◽  
Satisfiability Problem ◽  
Boolean Formula ◽  
Incidence Graph ◽  
Complexity Status

The prominent Boolean formula satisfiability problem SAT is known to be [Formula: see text]-complete even for very restricted variants such as 3-SAT, Monotone 3-SAT, or Planar 3-SAT, or instances with bounded variable appearance. We settle the computational complexity status for two variants with bounded variable appearance: We show that Planar Monotone Sat — the variant of Monotone Sat in which the incidence graph is required to be planar — is [Formula: see text]-complete even if each clause consists of at most three distinct literals and each variable appears exactly three times, and that Monotone Sat is [Formula: see text]-complete even if each clause consists of three distinct literals and each variable appears exactly four times in the formula. The latter confirms a conjecture stated in scribe notes [7] of an MIT lecture by Eric Demaine. In addition, we provide hardness results with respect to bounded variable appearances for two variants of Planar Monotone Sat.

FROM XSAT TO SAT BY EXHIBITING BOOLEAN FUNCTIONS

2009 ◽  
Vol 18 (05) ◽  
pp. 783-799
Author(s):  
RICHARD OSTROWSKI ◽  
LIONEL PARIS
Keyword(s):  
Graph Coloring ◽  
Boolean Functions ◽  
Structural Information ◽  
Conjunctive Normal Form ◽  
Satisfiability Problem ◽  
Boolean Formula ◽  
Truth Assignment ◽  
Coloring Problem ◽  
Graph Coloring Problem ◽  
Speed Up

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.

scholarly journals On the Computational Complexity of the Numerically Definite Syllogistic and Related Logics

2008 ◽  
Vol 14 (1) ◽  
pp. 1-28 ◽  
Author(s):  
Ian Pratt-Hartmann
Keyword(s):  
Computational Complexity ◽  
Related Problem ◽  
Satisfiability Problem ◽  
Propositional Satisfiability ◽  
Proof Systems ◽  
Transitive Verbs ◽  
Np Complete

AbstractThe numerically definite syllogistic is the fragment of English obtained by extending the language of the classical syllogism with numerical quantifiers. The numerically definite relational syllogistic is the fragment of English obtained by extending the numerically definite syllogistic with predicates involving transitive verbs. This paper investigates the computational complexity of the satisfiability problem for these fragments. We show that the satisfiability problem (= finite satisfiability problem) for the numerically definite syllogistic is strongly NP-complete, and that the satisfiability problem (= finite satisfiability problem) for the numerically definite relational syllogistic is NEXPTIME-complete, but perhaps not strongly so. We discuss the related problem of probabilistic (propositional) satisfiability, and thereby demonstrate the incompleteness of some proof-systems that have been proposed for the numerically definite syllogistic.

scholarly journals A complete classification of the complexity of the vertex 3-colourability problem for quadruples of induced 5-vertex prohibitions

2020 ◽  
Vol 22 (1) ◽  
pp. 38-47
Author(s):  
Dmitry S. Malyshev
Keyword(s):  
Graph Theory ◽  
Computational Complexity ◽  
Complete Classification ◽  
Induced Subgraphs ◽  
Simple Graphs ◽  
Forbidden Induced Subgraphs ◽  
The Third ◽  
Hereditary Class ◽  
Complexity Status

The vertex 3-colourability problem for a given graph is to check whether it is possible to split the set of its vertices into three subsets of pairwise non-adjacent vertices or not. A hereditary class of graphs is a set of simple graphs closed under isomorphism and deletion of vertices; the set of its forbidden induced subgraphs defines every such a class. For all but three the quadruples of 5-vertex forbidden induced subgraphs, we know the complexity status of the vertex 3-colourability problem. Additionally, two of these three cases are polynomially equivalent; they also polynomially reduce to the third one. In this paper, we prove that the computational complexity of the considered problem in all of the three mentioned classes is polynomial. This result contributes to the algorithmic graph theory.

scholarly journals Rotation Based MSS/MCS Enumeration

10.29007/8btb ◽  
2020 ◽  
Author(s):  
Jaroslav Bendík ◽  
Ivana Cerna
Keyword(s):  
Time Limit ◽  
Satisfiability Problem ◽  
Experimental Comparison ◽  
Boolean Formula ◽  
Enumeration Algorithm ◽  
Complete Enumeration ◽  
Enumeration Algorithms

Given an unsatisfiable Boolean Formula F in CNF, i.e., a set of clauses, one is often interested in identifying Maximal Satisfiable Subsets (MSSes) of F or, equivalently, the complements of MSSes called Minimal Correction Subsets (MCSes). Since MSSes (MC- Ses) find applications in many domains, e.g. diagnosis, ontologies debugging, or axiom pinpointing, several MSS enumeration algorithms have been proposed. Unfortunately, finding even a single MSS is often very hard since it naturally subsumes repeatedly solving the satisfiability problem. Moreover, there can be up to exponentially many MSSes, thus their complete enumeration is often practically intractable. Therefore, the algorithms tend to identify as many MSSes as possible within a given time limit. In this work, we present a novel MSS enumeration algorithm called RIME. Compared to existing algorithms, RIME is much more frugal in the number of performed satisfiability checks which we witness via an experimental comparison. Moreover, RIME is several times faster than existing tools.

scholarly journals Characterization and computation of ancestors in reaction systems

2020 ◽  
Author(s):  
Roberto Barbuti ◽  
Anna Bernasconi ◽  
Roberta Gori ◽  
Paolo Milazzo
Keyword(s):  
Computational Complexity ◽  
Polynomial Time ◽  
Boolean Formula ◽  
Minimal Size ◽  
Minimum Cardinality ◽  
Reaction Systems ◽  
Target Set ◽  
The Cost

Abstract In reaction systems, preimages and nth ancestors are sets of reactants leading to the production of a target set of products in either 1 or n steps, respectively. Many computational problems on preimages and ancestors, such as finding all minimum-cardinality nth ancestors, computing their size or counting them, are intractable. In this paper, we characterize all nth ancestors using a Boolean formula that can be computed in polynomial time. Once simplified, this formula can be exploited to easily solve all preimage and ancestor problems. This allows us to directly relate the difficulty of ancestor problems to the cost of the simplification so that new insights into computational complexity investigations can be achieved. In particular, we focus on two problems: (i) deciding whether a preimage/nth ancestor exists and (ii) finding a preimage/nth ancestor of minimal size. Our approach is constructive, it aims at finding classes of reactions systems for which the ancestor problems can be solved in polynomial time, in exact or approximate way.

A Polynomial Algorithm for Constructing a Large Bipartite Subgraph, with an Application to a Satisfiability Problem

1982 ◽  
Vol 34 (3) ◽  
pp. 519-524 ◽  
Author(s):  
Svatopluk Poljak ◽  
Daniel Turzík
Keyword(s):  
Connected Graph ◽  
Polynomial Algorithm ◽  
Short Proof ◽  
Satisfiability Problem ◽  
Boolean Formula ◽  
Complete Problem ◽  
Bipartite Subgraph ◽  
Np Complete ◽  
Image Position

Let G be a symmetric connected graph without loops. Denote by b(G) the maximum number of edges in a bipartite subgraph of G. Determination of b(G) is polynomial for planar graphs ([6], [8]); in general it is an NP-complete problem ([5]). Edwards in [1], [2] found some estimates of b(G) which give, in particular,for a connected graph G of n vertices and m edges, whereand ﹛x﹜ denotes the smallest integer ≧ x.We give an 0(V3) algorithm which for a given graph constructs a bipartite subgraph B with at least f(m, n) edges, yielding a short proof of Edwards’ result.Further, we consider similar methods for obtaining some estimates for a particular case of the satisfiability problem. Let Φ be a Boolean formula of variables x1, …, xn.

COMPLEXITY OF SEMIGROUP IDENTITY CHECKING

2004 ◽  
Vol 14 (04) ◽  
pp. 455-464 ◽  
Author(s):  
ANDRZEJ KISIELEWICZ
Keyword(s):  
Computational Complexity ◽  
General Formula ◽  
Commutative Semigroup ◽  
Simple Proof ◽  
Finite Semigroup ◽  
Structure Theory ◽  
Semigroup Identity ◽  
Commutative Semigroups ◽  
Complexity Status ◽  
Np Complete

We consider the [Formula: see text] problem, whose instance is a finite semigroup S and an identity I, and the question is whether I is satisfied in S. We show that the question concerning computational complexity of this problem is much harder, when restricted to commutative semigroups. We provide a relatively simple proof that in general the problem is co-NP-complete, and demonstrate, using some structure theory, that for a fixed commutative semigroup the problem can be solved in polynomial time. The complexity status of the general [Formula: see text] problem remains open.

scholarly journals Quantum invariants of 3-manifolds and NP vs #P

2017 ◽  
Vol 17 (1&2) ◽  
pp. 125-146
Author(s):  
Gorjan Alagic ◽  
Catharine Lo
Keyword(s):  
Computational Complexity ◽  
Quantum Computation ◽  
Complexity Class ◽  
Boolean Formula ◽  
Heegaard Splittings ◽  
Quantum Invariants ◽  
Link Diagrams

The computational complexity class #P captures the difficulty of counting the satisfying assignments to a boolean formula. In this work, we use basic tools from quantum computation to give a proof that the SO(3) Witten-Reshetikhin-Turaev (WRT) invariant of 3-manifolds is #P-hard to calculate. We then apply this result to a question about the combinatorics of Heegaard splittings, motivated by analogous work on link diagrams by M. Freedman. We show that, if #P 6⊆ FPNP, then there exist infinitely many Heegaard splittings which cannot be made logarithmically thin by local WRT-preserving moves, except perhaps via a superpolynomial number of steps. We also outline two extensions of the above results. First, adapting a result of Kuperberg, we show that any presentationindependent approximation of WRT is also #P-hard. Second, we sketch out how all of our results can be translated to the setting of triangulations and Turaev-Viro invariants.

scholarly journals MAX-SAT Problem using Hybrid Harmony Search Algorithm

2018 ◽  
Vol 27 (4) ◽  
pp. 643-658 ◽  
Author(s):  
Iyad Abu Doush ◽  
Amal Lutfi Quran ◽  
Mohammed Azmi Al-Betar ◽  
Mohammed A. Awadallah
Keyword(s):  
Search Algorithm ◽  
Harmony Search ◽  
Harmony Search Algorithm ◽  
Satisfiability Problem ◽  
Boolean Formula ◽  
Stochastic Local Search ◽  
Boolean Variable ◽  
Sat Problem ◽  
Max Sat ◽  
The Impact

Abstract Maximum Satisfiability problem is an optimization variant of the Satisfiability problem (SAT) denoted as MAX-SAT. The aim of this problem is to find Boolean variable assignment that maximizes the number of satisfied clauses in the Boolean formula. In case the number of variables per clause is equal or greater than three, then this problem is considered NP-complete. Hence, many researchers have developed techniques to deal with MAX-SAT. In this paper, we investigate the impact of different hybrid versions of binary harmony search (HS) algorithm on solving MAX 3-SAT problem. Therefore, we propose two novel hybrid binary HS algorithms. The first hybridizes Flip heuristic with HS, and the second uses Tabu search combined with Flip heuristic. Furthermore, a distinguished feature of our proposed approaches is using an objective function that is updated dynamically based on the stepwise adaptation of weights (SAW) mechanism to evaluate the MAX-SAT solution using the proposed hybrid versions. The performance of the proposed approaches is evaluated over standard MAX-SAT benchmarks, and the results are compared with six evolutionary algorithms and three stochastic local search algorithms. The obtained results are competitive and show that the proposed novel approaches are effective.

Sign in / Sign up

Export Citation Format

Share Document