Generalizations of matched CNF formulas

A CNF formula is called matched if its associated bipartite graph (whose vertices are clauses and variables) has a matching that covers all clauses. Matched CNF formulas are satisfiable and can be recognized efficiently by matching algorithms. We generalize this concept and cover clauses by collections of bicliques (complete bipartite graphs). It turns out that such generalization indeed gives rise to larger classes of satisfiable CNF formulas which we term biclique satisfiable. We show, however, that the recognition of biclique satisfiable CNF formulas is NP-complete, and remains NP-hard if the size of bicliques is bounded. A satisfiable CNF formula is called var-satisfiable if it remains satisfiable under arbitrary replacement of literals by their complements. Var-satisfiable CNF formulas can be viewed as the best possible generalization of matched CNF formulas as every matched CNF formula and every biclique satisfiable CNF formula is var-satisfiable. We show that recognition of var-satisfiable CNF formulas is ₂ ^P-complete, answering a question posed by Kleine Büning and Zhao.     

Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable

Recognition of minimal unsatisfiable CNF formulas (unsatisfiable CNF formulas which become satisfiable if any clause is removed) is a classical D^P-complete problem. It was shown recently that minimal unsatisfiable formulas with n variables and n+k clauses can be recognized in time . We improve this result and present an algorithm with time complexity ; hence the problem turns out to be fixed-parameter tractable (FTP) in the sense of Downey and Fellows (Parameterized Complexity, 1999).Our algorithm gives rise to a fixed-parameter tractable parameterization of the satisfiability problem: If for a given set of clauses F, the number of clauses in each of its subsets exceeds the number of variables occurring in the subset at most by k, then we can decide in time whether F is satisfiable; k is called the maximum deficiency of F and can be efficiently computed by means of graph matching algorithms. Known parameters for fixed-parameter tractable satisfiability decision are tree-width or related to tree-width. Tree-width and maximum deficiency are incomparable in the sense that we can find formulas with constant maximum deficiency and arbitrarily high tree-width, and formulas where the converse prevails.     

Three ∑ P 2 -complete problems in computational learning theory

The consistency problem associated with a concept classC is to determine, given two setsA andB of examples, whether there exists a conceptc inC such that eachx inA is a positive example ofc and eachy inB is a negative example ofc. We explore in this paper the following intuition: for a concept classC, if the membership problem of determining whether a given example is positive for a concept isNP-complete, then the corresponding consistency problem is likely to be _P ² -complete. To support this intuition, we prove that the following three consistency problems for concept classes of patterns, graphs and generalized Boolean formulas, whose membership problems are known to beNP-complete, are _P ² -complete: (a) given two setsA andB of strings, determine whether there exists a patternp such that every string inA is in the languageL(p) and every string inB is not in the languageL(p); (b) given two setsA andB of graphs, determine whether there exists a graphG such that every graph inA is isomorphic to a subgraph ofG and every graph inB is not isomorphic to any subgraph ofG; and (c) given two setsA andB of Boolean formulas, determine whether there exists a 3-CNF Boolean formula such that for every A, is satisfiable and for every B, is not satisfiable. These results suggest that consistendy problems in machine learning are natural candidates for _P ² -complete problems if the corresponding membership problems are known to beNP-complete.In addition, we prove that the corresponding prediction problems for concept classes of polynomial-time nondeterministic Turing machines, nondeterministic Boolean circuits, generalized Boolean formulas, patterns and graphs are prediction-complete for the classR _NP of all concept classes whose membership problems are inNP.     

On finding short resolution refutations and small unsatisfiable subsets

We consider the parameterized problems of whether a given set of clauses can be refuted within k resolution steps, and whether a given set of clauses contains an unsatisfiable subset of size at most k  . We show that both problems are complete for the class W[1]$\mathrm{W}[1]$, the first level of the W-hierarchy of fixed-parameter intractable problems. Our results remain true if restricted to 3-SAT instances and/or to various restricted versions of resolution including tree-like resolution, input resolution, and read-once resolution. Applying a metatheorem of Frick and Grohe, we show that, restricted to classes of sets of clauses of locally bounded treewidth, the considered problems are fixed-parameter tractable. For example, the problems are fixed-parameter tractable for planar CNF formulas.     

d-正则(k,s)-SAT问题的NP完全性

研究具有正则结构的SAT问题是否是NP完全问题,具有重要的理论价值.(k,s)-CNF公式类和正则(k,s)-CNF公式类已被证明存在一个临界函数f(k),使得当s≤f(k)时,所有实例都可满足;当s≥f(k)+1时,对应的SAT问题是NP完全问题.研究具有更强正则约束的d-正则(k,s)-SAT问题,其要求实例中每个变元的正负出现次数之差不超过给定的自然数d.通过设计一种多项式时间的归约方法,证明d-正则(k,s)-SAT问题存在一个临界函数f(k,d),使得当s≤f(k,d)时,所有实例都可满足;当s≥f(k,d)+1时,d-正则(k,s)-SAT问题是NP完全问题.这种多项式时间的归约变换方法通过添加新的变元和新的子句,可以更改公式的子句约束密度,并约束每个变元正负出现次数的差值.这进一步说明,只用子句约束密度不足以刻画CNF公式结构的特点,对临界函数f(k,d)的研究有助于在更强正则约束条件下构造难解实例.     

A New Lower Bound on the Maximum Number of Satisfied Clauses in Max-SAT and Its Algorithmic Applications

A pair of unit clauses is called conflicting if it is of the form (x), $(\bar{x})$ . A CNF formula is unit-conflict free (UCF) if it contains no pair of conflicting unit clauses. Lieberherr and Specker (J. ACM 28:411?C421, 1981) showed that for each UCF CNF formula with m clauses we can simultaneously satisfy at least $\hat{ \varphi } m$ clauses, where $\hat{ \varphi }=(\sqrt{5}-1)/2$ . We improve the Lieberherr-Specker bound by showing that for each UCF CNF formula F with m clauses we can find, in polynomial time, a?subformula F?? with m?? clauses such that we can simultaneously satisfy at least $\hat{ \varphi } m+(1-\hat{ \varphi })m'+(2-3\hat {\varphi })n''/2$ clauses (in F), where n?? is the number of variables in F which are not in F??. We consider two parameterized versions of MAX-SAT, where the parameter is the number of satisfied clauses above the bounds m/2 and $m(\sqrt{5}-1)/2$ . The former bound is tight for general formulas, and the later is tight for UCF formulas. Mahajan and Raman (J. Algorithms 31:335?C354, 1999) showed that every instance of the first parameterized problem can be transformed, in polynomial time, into an equivalent one with at most 6k+3 variables and 10k clauses. We improve this to 4k variables and $(2\sqrt{5}+4)k$ clauses. Mahajan and Raman conjectured that the second parameterized problem is fixed-parameter tractable (FPT). We show that the problem is indeed FPT by describing a polynomial-time algorithm that transforms any problem instance into an equivalent one with at most $(7+3\sqrt{5})k$ variables. Our results are obtained using our improvement of the Lieberherr-Specker bound above.     

Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution

We work with an extension of Resolution, called Res(2), that allows clauses with conjunctions of two literals. In this system there are rules to introduce and eliminate such conjunctions. We prove that the weak pigeonhole principle PHP^cn_n and random unsatisfiable CNF formulas require exponential-size proofs in this system. This is the strongest system beyond Resolution for which such lower bounds are known. As a consequence to the result about the weak pigeonhole principle, Res(log) is exponentially more powerful than Res(2). Also we prove that Resolution cannot polynomially simulate Res(2) and that Res(2) does not have feasible monotone interpolation solving an open problem posed by Krají ek.     

不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

k-LSAT(k≥3)是NP-完全的(英文)

合取范式(conjunctive normal form,简称CNF)公式F是线性公式,如果F中任意两个不同子句至多有一个公共变元.如果F中的任意两个不同子句恰好含有一个公共变元,则称F是严格线性的.所有的严格线性公式均是可满足的,而对于线性公式类LCNF,对应的判定问题LSAT仍然是NP-完全的.LCNF≥k是子句长度大于或等于k的CNF公式子类,判定问题LSAT≥k的NP-完全性与LCNF≥k中是否含有不可满足公式密切相关.即LSAT≥k的NP-完全性取决于LCNF≥k是否含有不可满足公式.S.Porschen等人用超图和拉丁方的方法构造了LCNF≥3和LCNF≥4中的不可满足公式,并提出公开问题:对于k≥5,LCNF≥k是否含有不可满足公式?将极小不可满足公式应用于公式的归约,引入了一个简单的一般构造方法.证明了对于k≥3,k-LCNF含有不可满足公式,从而证明了一个更强的结果:对于k≥3,k-LSAT是NP-完全的.     

Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference

A formula (in conjunctive normal form) is said to be minimal unsatisfiable if it is unsatisfiable and deleting any clause makes it satisfiable. The deficiency of a formula is the difference of the number of clauses and the number of variables. It is known that every minimal unsatisfiable formula has positive deficiency. Until recently, polynomial-time algorithms were known to recognize minimal unsatisfiable formulas with deficiency 1 and 2. We state an algorithm which recognizes minimal unsatisfiable formulas with any fixed deficiency in polynomial time.     

Testing satisfiability of CNF formulas by computing a stable set of points

We show that a conjunctive normal form (CNF) formula F is unsatisfiable if and only if there is a set of points of the Boolean space that is stable with respect to F. So testing the satisfiability of a CNF formula reduces to looking for a stable set of points (SSP). We give some properties of SSPs and describe a simple algorithm for constructing an SSP for a CNF formula. Building an SSP can be viewed as a natural way of search space traversal. This naturalness of search space examination allows one to make use of the regularity of CNF formulas to be checked for satisfiability. We illustrate this point by showing that if a CNF F formula is symmetric with respect to a group of permutations, it is very easy to make use of this symmetry when constructing an SSP. As an example, we show that the unsatisfiability of pigeon-hole CNF formulas can be proven by examining only a set of points whose size is quadratic in the number of holes. Finally, we introduce the notion of an SSP with excluded directions and sketch a procedure of satisfiability testing based on the construction of such SSPs.     

Testing satisfiability of CNF formulas by computing a stable set of points

We show that a conjunctive normal form (CNF) formula F is unsatisfiable if and only if there is a set of points of the Boolean space that is stable with respect to F. So testing the satisfiability of a CNF formula reduces to looking for a stable set of points (SSP). We give some properties of SSPs and describe a simple algorithm for constructing an SSP for a CNF formula. Building an SSP can be viewed as a natural way of search space traversal. This naturalness of search space examination allows one to make use of the regularity of CNF formulas to be checked for satisfiability. We illustrate this point by showing that if a CNF F formula is symmetric with respect to a group of permutations, it is very easy to make use of this symmetry when constructing an SSP. As an example, we show that the unsatisfiability of pigeon-hole CNF formulas can be proven by examining only a set of points whose size is quadratic in the number of holes. Finally, we introduce the notion of an SSP with excluded directions and sketch a procedure of satisfiability testing based on the construction of such SSPs.     

On exact selection of minimally unsatisfiable subformulae

A minimally unsatisfiable subformula (MUS) is a subset of clauses of a given CNF formula which is unsatisfiable but becomes satisfiable as soon as any of its clauses is removed. The selection of a MUS is of great relevance in many practical applications. This expecially holds when the propositional formula encoding the application is required to have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). While selection of a MUS is a hard problem in general, we show classes of formulae where this problem can be solved efficiently. This is done by using a variant of Farkas lemma and solving a linear programming problem. Successful results on real-world contradiction detection problems are presented.     

Satisfiability Checking in ?ukasiewicz Logic as Finite Constraint Satisfaction

Although it is well-known that every satisfiable formula in ?ukasiewicz’ infinite-valued logic $\mathcal{L}_{\infty}$ can be satisfied in some finite-valued logic, practical methods for finding an appropriate number of truth degrees do currently not exist. Extending upon earlier results by Aguzzoli et al., which only take the total number of variable occurrences into account, we present a detailed analysis of what type of formulas require a large number of truth degrees to be satisfied. In particular, we reveal important links between this number of truth degrees and the dimension, and structure, of the cycle space of an associated bipartite graph. We furthermore propose an efficient, polynomial-time algorithm for establishing a strong upper bound on the required number of truth degrees, allowing us to check the satisfiability of sets of formulas in $\mathcal{L}_{\infty}$ , and more generally, sets of fuzzy clauses over ?ukasiewicz logic formulas, by solving a small number of constraint satisfaction problems. In an experimental evaluation, we demonstrate the practical usefulness of this approach, comparing it with a state-of-the-art technique based on mixed integer programming.     

Biclique cryptanalysis on lightweight block cipher: HIGHT and Piccolo

Biclique cryptanalysis is an attack that improves the computational complexity by finding a biclique which is a kind of bipartite graph. We present a single-key full-round attack of lightweight block ciphers, HIGHT and Piccolo by using biclique cryptanalysis. In this paper, a 9-round biclique is constructed for HIGHT and a 4-round biclique for Piccolo. These new bicliques are used to recover secret keys for the full rounds of HIGHT, Piccolo-80 and Piccolo-128, the computational complexity of 2^125.93, 2^79.34 and 2^127.36, respectively. The computational complexity of attacking HIGHT by a biclique cryptanalysis is reduced from 2^126.4. This is the first full-round attack on both Piccolo-80 and Piccolo-128.     

Topology on the set of R 0 semantics for R 0 algebras

This paper introduces the concepts of R ₀ valuation, R ₀ semantic, countable R ₀ category , R ₀ fuzzy topological category , etc. It is established in a natural way that the fuzzy topology δ and its cut topology on the set Ω _M consisting of all R ₀ valuations of an R ₀ algebra M, and some properties of fuzzy topology δ and its cut topology are investigated carefully. Moreover, the representation theorem for R ₀ algebras by means of fuzzy topology is given, that is to say the category is equivalent to the category . By studying the relation between valuations and filters, the Loomis–Sikorski theorem for R ₀ algebras is obtained. As an application, K-compactness of the R ₀ logic is discussed.     

Normal forms in BL and ŁΠ algebras of functions

Three types of normal forms are introduced for fuzzy logic functions: disjunctive, conjunctive and additive. Disjunctive and conjunctive normal forms are considered in two variants: infinite and finite. It is proved that infinite normal forms are universal representation formulas whereas finite normal forms are universal approximation formulas for any L-valued function where L is a support set of any complete BL-algebra. The additive normal form lies in the middle of the two others. For all of them the estimation of the quality of approximation is suggested.     

Tuples of Disjoint $\mathsf{NP}$ -Sets

Disjoint -pairs are a well studied complexity-theoretic concept with important applications in cryptography and propositional proof complexity. In this paper we introduce a natural generalization of the notion of disjoint -pairs to disjoint k-tuples of -sets for k≥2. We define subclasses of the class of all disjoint k-tuples of -sets. These subclasses are associated with a propositional proof system and possess complete tuples which are defined from the proof system. In our main result we show that complete disjoint -pairs exist if and only if complete disjoint k-tuples of -sets exist for all k≥2. Further, this is equivalent to the existence of a propositional proof system in which the disjointness of all k-tuples is shortly provable. We also show that a strengthening of this conditions characterizes the existence of optimal proof systems. An extended abstract of this paper appeared in the proceedings of the conference CSR 2006 (Lecture Notes in Computer Science 3967, 80–91, 2006). Supported by DFG grant KO 1053/5-1.