arXiv 1504.010922015-04-05cs.CC

Technical Notes on Complexity of the Satisfiability Problem

Marek A. Suchenek

备注：: 18 pages

英文摘要：

These notes contain, among others, a proof that the average running time of an easy solution to the satisfiability problem for propositional calculus is, under some reasonable assumptions, linear (with constant 2) in the size of the input. Moreover, some suggestions are made about criteria for tractability of complex algorithms. In particular, it is argued that the distribution of probability on the whole input space of an algorithm constitutes an non-negligible factor in estimating whether the algorithm is tractable or not.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

A Critique of Kumar's "Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and Its Implications on P versus NP problem."

In this paper, we analyze the argument made by Kumar in the technical report "Necessary and Sufficient Condition for Satisfiability of a Boolean Formula in CNF and Its Implications on P versus NP problem." The paper claims to present a polynomial-time algorithm that decides CNF-SAT. We show that the paper's analysis is flawed and that the fundamental underpinning of its algorithm requires an exponential number of steps on infinitely many inputs.

2021-12-11cs.CC

Horn Fragments of the Halpern-Shoham Interval Temporal Logic (Technical Report)

We investigate the satisfiability problem for Horn fragments of the Halpern-Shoham interval temporal logic depending on the type (box or diamond) of the interval modal operators, the type of the underlying linear order (discrete or dense), and the type of semantics for the interval relations (reflexive or irreflexive). For example, we show that satisfiability of Horn formulas with diamonds is undecidable for any type of linear orders and semantics. On the contrary, satisfiability of Horn formulas with boxes is tractable over both discrete and dense orders under the reflexive semantics and over…

2017-08-28cs.CCcs.LO

关于分级模态逻辑可满足性问题复杂性的注记

A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics

Computing Laboratory（计算实验室）；Oxford University（牛津大学）；School of Computer Science（计算机科学学院）；University of Manchester（曼彻斯特大学）

本文研究了分级模态逻辑在自反性、序列性、对称性、传递性和欧几里得性等不同组合框架类上的可满足性问题，并为其获得了紧致的复杂性界限。

2009-05-19cs.AIcs.CCcs.LO

Some remarks on the survey decimation algorithm for K-satisfiability

In this note we study the convergence of the survey decimation algorithm. An analytic formula for the reduction of the complexity during the decimation is derived. The limit of the converge of the algorithm are estimated in the random case: interesting phenomena appear near the boundary of convergence.

2003-01-16cond-mat.dis-nncs.CCcs.DS

On the probabilistic approach to the random satisfiability problem

In this note I will review some of the recent results that have been obtained in the probabilistic approach to the random satisfiability problem. At the present moment the results are only heuristic. In the case of the random 3-satisfiability problem a phase transition from the satisfiable to the unsatisfiable phase is found at $α=4.267$. There are other values of $α$ that separates different regimes and they will be described in details. In this context the properties of the survey decimation algorithm will also be discussed.

2003-08-05cond-mat.dis-nncs.CC

On the survey-propagation equations for the random K-satisfiability problem

In this note we study the existence of a solution to the survey-propagation equations for the random K-satisfiability problem for a given instance. We conjecture that when the number of variables goes to infinity, the solution of these equations for a given instance can be approximated by the solution of the corresponding equations on an infinite tree. We conjecture (and we bring numerical evidence) that the survey-propagation equations on the infinite tree have an unique solution in the suitable range of parameters.

2002-12-07cond-mat.dis-nncs.CC

更多相关论文收起更多论文

Generalized Modal Satisfiability

It is well known that modal satisfiability is PSPACE-complete (Ladner 1977). However, the complexity may decrease if we restrict the set of propositional operators used. Note that there exist an infinite number of propositional operators, since a propositional operator is simply a Boolean function. We completely classify the complexity of modal satisfiability for every finite set of propositional operators, i.e., in contrast to previous work, we classify an infinite number of problems. We show that, depending on the set of propositional operators, modal satisfiability is PSPACE-complete, coNP-…

2008-04-17cs.CCcs.LO

Tight Lower Bounds for the Workflow Satisfiability Problem Based on the Strong Exponential Time Hypothesis

The Workflow Satisfiability Problem (WSP) asks whether there exists an assignment of authorized users to the steps in a workflow specification, subject to certain constraints on the assignment. The problem is NP-hard even when restricted to just not equals constraints. Since the number of steps $k$ is relatively small in practice, Wang and Li (2010) introduced a parametrisation of WSP by $k$. Wang and Li (2010) showed that, in general, the WSP is W[1]-hard, i.e., it is unlikely that there exists a fixed-parameter tractable (FPT) algorithm for solving the WSP. Crampton et al. (2013) and Cohen e…

2015-08-27cs.CCcs.CRcs.DS

Polynomial Kernels and User Reductions for the Workflow Satisfiability Problem

The Workflow Satisfiability Problem (WSP) is a problem of practical interest that arises whenever tasks need to be performed by authorized users, subject to constraints defined by business rules. We are required to decide whether there exists a plan -- an assignment of tasks to authorized users -- such that all constraints are satisfied. The WSP is, in fact, the conservative Constraint Satisfaction Problem (i.e., for each variable, here called task, we have a unary authorization constraint) and is, thus, NP-complete. It was observed by Wang and Li (2010) that the number k of tasks is often qui…

2014-09-25cs.CCcs.DS

Technical Note: Exploring Σ^P_2 / Π^P_2-hardness for Argumentation Problems with fixed distance to tractable classes

We study the complexity of reasoning in abstracts argumentation frameworks close to graph classes that allow for efficient reasoning methods, i.e.\ to one of the classes of acyclic, noeven, biparite and symmetric AFs. In this work we show that certain reasoning problems on the second level of the polynomial hierarchy still maintain their full complexity when restricted to instances of fixed distance to one of the above graph classes.

2012-01-02cs.AIcs.CC

SAT for pedestrians

The aim of this short note is mainly pedagogical. It summarizes some knowledge about Boolean satisfiability (SAT) and the P=NP? problem in an elementary mathematical language. A convenient scheme to visualize and manipulate CNF formulae is introduced. Also some results like the formulae for the number of unsatisfied clauses and the number of solutions might be unknown.

2014-08-13cs.CCmath.LO

The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability

Satisfiability is considered the canonical NP-complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms can solve large-scale industrial SAT instances very efficiently. This disparity between theory and practice is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two characteristic properties seem to be prevalent in the majority of real-world SAT instances, heterogeneous degree distribution and locality. To understand the impact of these two properties on SAT, we stu…

2021-11-23cs.CCcs.CGcs.DM

Simple Reductions from Formula-SAT to Pattern Matching on Labeled Graphs and Subtree Isomorphism

The CNF formula satisfiability problem (CNF-SAT) has been reduced to many fundamental problems in P to prove tight lower bounds under the Strong Exponential Time Hypothesis (SETH). Recently, the works of Abboud, Hansen, Vassilevska W. and Williams (STOC 16), and later, Abboud and Bringmann (ICALP 18) have proposed basing lower bounds on the hardness of general boolean formula satisfiability (Formula-SAT). Reductions from Formula-SAT have two advantages over the usual reductions from CNF-SAT: (1) conjectures on the hardness of Formula-SAT are arguably much more plausible than those of CNF-SAT, …

2020-08-26cs.CCcs.DS

《Fortune的馈赠：通过修剪树来驯服复杂性——面向入门学生的高级复杂性理论实践问题解决体验》

Fortune's Bounty: Taming Complexity by Trimming Trees --- A Hands-On Problem-Solving Experience in Advanced Complexity Suitable for Introductory Students

Rochester Institute of Technology（罗切斯特理工学院）

本文设计作业让完成CS1/CS2的本科生小组自行证明Fortune定理，帮助学生理解复杂性理论相关知识，提升问题解决与研究技能。

2026-08-14cs.CCcs.CY

关于多区块仓库中拣货路径问题及相关问题复杂性的注记

A note on the complexity of the picker routing problem in multi-block warehouses and related problems

本文证明多区块仓库中的拣货路径问题是强NP难问题，并据此确定了其他相关问题的复杂性状态。

2025-01-24cs.CCcs.DSmath.OC