Hans Kleine Büning | All Literal Horn - Description | Workshop Slide |
Endre Boros | Infrequent literals in DNF expressions | Workshop Slide |
Thomas Eiter | Intersecting Monotone UNSAT | Workshop Slide 1 |
Symmetric Intersecting Monotone UNSAT | Workshop Slide 2 | |
John Franco | Short UNSAT certificates | |
Oliver Kullman | No Name Problem - Description | Workshop Slide |
Paul W. Purdom | No Name Problem - Description | Workshop Slide |
Ewald Speckenmeyer | No Name Problem - Description | Workshop Slide |
Cosimo Spera | No Name Problem - Description | |
Alasdair Urquhart | Mutilated Chessboards - Description | Workshop Slide |
Allen Van Gelder | No Name Problem - Description | Workshop Slide |
The set {l literal | F |= l} obviously can be calculated in
time O(|F| * n), where |F| is the length of the formula and
n is the number of variables.
The set of positive literals (variables) {x variable | F |= x}
can be determined in time O(|F|) using unit resolution. The problem
arises with negative literals.
The unique--satisfiability problem for Horn formulas is a special case
and known to be solvable in linear time.
Now the question is whether there exists an algorithm solving the Literal Horn problem in time less than O(|F| * n).
Send solution to kbcsl@uni-paderborn.de
Endre Boros
Given a DNF formula involving n variables and n+1 terms,
any two of which
have exactly one conflicting variable, show that there is a literal (not
variable!), which occurs at most once.
References:
Send solution to boros@rutcor.rutgers.edu
Thomas Eiter - Intersecting Monotone UNSAT (IMUNSAT)
The following restriction (IMUNSAT) of the classical satisfiability problem is
currently open:
INSTANCE: A set C of clauses such that each clause is either
positive (i.e., consists entirely of positive literals) or negative
(i.e., consists entirely of negative literals) and for each positive
clause C1 and negative clause C2 of C, there exists an
atom u such that u is in C1 and !u is in
C2.
QUESTION: Is C unsatisfiable?
Reference:
This problem is the (un)satisfiability variant of a number of equivalent (under polynomial time transformation) problems in different areas of operations research and computer science. A number of people have considered essentially this problem in papers, including M. Fredman, T. Ibaraki, D.S. Johnson, L. Khachiyan, R. Khardon, E. Lawler, J. Lenstra, H. Mannila, Ch. Papadimitriou, K.-J. Räihä, A. Rinnooy Kan, M. Yannakakis, to mention some of them. The problem (in equivalent formulations) is open for more than 15 years.
There is a yet more restricted version of IMSAT, which is as hard as the general case.
Symmetric Intersecting Monotone UNSAT (SIMUNSAT)
INSTANCE: Restriction of IMSAT to instances C where the
negative clauses are precisely all clauses C- such that
C- = { !u : u is in C+} for some positive
clause C+ in C. (By this restriction, nonempty positive
clauses of C are mutually intersecting.)
QUESTION: Is C unsatisfiable?
Although this problem statement seems easy, it appears to be difficult to come up with a polynomial time algorithm. What is known to date is that the problem is most likely not coNP-complete, due to the recent quasi-polynomial time algorithm of Fredman and Khachiyan for the positive dualization problem (see below). This algorithm implies that IMUNSAT and SIMUNSAT can be solved in quasi-polynomial time, as well as all problems mentioned below.
There are a number of problems that are equivalent to SIMUNSAT (under polynomial time transformation). The problems are in different areas of logic, operations research, and computer science. We describe here some of them. (For a more detailed account, see the quoted paper of Eiter and Gottlob.)
A hypergraph H is a pair (V,E) of a finite set V and a family E = {E1, ... ,Em} of finite subsets Ei subseteq V (called edges). A hypergraph is simple, if it has no pair of edges Ei, Ej such that Ei is properly contained in Ej. A simple hypergraph is also known as a Sperner family.
Say that a simple hypergraph (V, E) is saturated if adding any further edge violates the property of being simple, i.e., (V, E} U {X}) where X subseteq V, is not simple.
The following problem is equivalent to SIMUNSAT:
Simple Hypergraph Saturation (SIMPLE-H-SAT)
INSTANCE: A simple hypergraph H = (V, E) on
vertices V = {v1, ... , n}.
QUESTION: Is H saturated?
A variant of this problem is that besides being simple, the hypergraph must be (and remain) in addition intersecting, i.e., each pair of edges Ei, Ej has nonempty intersection. This problem, known as Maximal Hypergraph Clique, has been presented by D.S. Johnson as an open problem in a lecture "Open and Closed Problems in NP-Completeness" at the Symposium and Summer School "NP-completeness: The First 20 Years", Erice, Sicily, 1991. (Actually, Johnson presented a spoiled version of the problem there (personal communication) which is clearly solvable in polynomial time).
A transversal (or hitting set) of a hypergraph H = (V, E) is a subset T subseteq V such that T meets each edge in at least one vertex, i.e., |T intersection Ei| >= 1, for all Ei in E. The transversal hypergraph of H is the hypergraph Tr(H) = (V, F) such that F is the family of all minimal (w.r.t. inclusion) transversals of H (see C. Berge's book Hypergraphs, North-Holland 1989, for a detailed study of the transversal hypergraph).
The following problem is equivalent to SIMUNSAT:
Transversal Hypergraph (TRANS-HYP)
INSTANCE: Two hypergraphs G = (V, E1) and
H = (V, E2) on vertices
V = {v1, ... , vn}.
QUESTION: Does H = Tr(G) hold?
This problem has immediate applications e.g. in Boolean logic and in the context of model based diagnosis.
Equivalent to this problem is the positive dualization problem:
Positive Dualization (POS-DUAL)
INSTANCE: Positive Boolean CNFs E and F.
QUESTION: Does F represent the dual of the function
represented by E?
A variant of this problem is the one where E is a positive CNF and F is a positive DNF, and we ask whether E and F represent the same Boolean function. Fredman and Khachiyan, On the Complexity of Dualization of Monotone Disjunctive Normal Forms, Technical Report LCS-TR-225, Dept. of Computer Science, Rutgers University, 1994, have shown that POS-DUAL can be solved in quasi-polynomial time, i.e., in time O(m^O(log m)) where m is the size of the input. See also Bioch and Ibaraki, Complexity of dualization and identification of positive boolean functions, Information and Computation, 123 (1995).
Next we consider problems equivalent to SIMUNSAT from database theory.
FD-Relation Equivalence
INSTANCE: A relation instance R (collection of tuples) and
a set F of functional dependencies in BCNF, both on a set of
attributes U.
QUESTION: Is R an Armstrong relation for F,
i.e., do on R hold exactly the dependencies represented by F?
A set F of functional dependencies on a set of attributes U is in Boyce-Codd Normal Form (BCNF), if in every nontrivial functional dependency X -> Y logically implied by F the left hand side X is a minimal key, i.e., a wrt. inclusion minimal subset X of attributes that determines all other attributes in U.
Also a variant of the key problem is equivalent to SIMUNSAT:
Additional Key (for relation instances)
INSTANCE: A relation instance R on attributes U, a set
K of minimal keys for R.
QUESTION: Is there a minimal key for R (i.e., the set of
functional dependencies F that hold on R) which is not
contained in K?
Notice that the key problem for relation schemes (instead of relation instances), where the input is a set F of functional dependencies on U, is polynomial.
We nect describe a problem from the area of reliability and distributed computing which is equivalent to SIMUNSAT.
A coterie C is, using hypergraph terminology, an intersecting hypergraph.
A coterie C' dominates a coterie C if they are different coteries on the same set of vertices and for every edge E in C there is an edge F in C' such that F subseteq E; a coterie is non-dominated (ND) if there is no coterie C' that dominates C. Nondominated coteries have been introduced by Garcia-Molina & Barbara, How to assign votes in a distributed system, JACM 32 (1985); they have been studied extensively e.g. by Ibaraki and Kameda, A theory of coteries: Mutual exclusion in distributed systems, IEEE Trans. on Parallel and Distributed Systems, 4 (1993).
The following problem is equivalent to SIMUNSAT:
Nondominated Coterie (ND-COTERIE)
INSTANCE: A coterie C.
QUESTION: Is C nondominated?
It is known that nondominatedness coincides with the property that C is a self-transversal hypergraph, i.e., a hypergraph H is identical to its transversal hypergraph. This yields the following problem equivalent to SIMUNSAT, which is a restriction of TRANS-HYP:
SELF-TRANSVERSALITY (SELF-TRANS)
INSTANCE: A hypergraph H.
QUESTION: Is H self-transversal, i.e., does
H = Tr(H) hold ?
There are other problems that are equivalent to SIMUNSAT, which have been recently identified in the area of propositional knowledge representation; see the papers by Khardon, Translating between Horn Representations and their Characteristic Models, J. Artificial Intelligence Research 3, 1995, and D. Kavvadias, Ch. Papadimitriou and M. Sideri, On Horn Envelopes and Hypergraph Tranversals, ISAAC-93 Proceedings, LNCS 762.
A polynomial time algorithm for any of the problems above would be highly appreciated.
John Franco
Does there exist an algorithm for verifying that a random 3-SAT formula
is unsatisfiable and that has polynomial time complexity with probability
tending to 1 when m/n is any constant greater than 5? or even when
m/n grows but lim m/n^(8/7)=0? or even when
\lim m/n^(2-e)=c for some small e > 0 and constant c?
Oliver Kullman
Let F be a CNF formula. Define F* to be an extension
for F if for all subsets S of clauses of F that are
satisfiable, S U F* is also satisfiable. If F is not
satisfiable, define Comp_E(F) to be the minimum value of
Comp_RES(F U F*) such that F* is an extension for F;
define Comp_RES(G) to be the minimum n such that G
|-n,RES 1.
Is Comp_E(F) polynomially bounded?
Let D = {F in CLS | forall(C_i,C_j in F, i != j) C_i intersection !C_j != emptyset}.
Is Comp_RES(F)_(F in D) polynomially bounded? Consider any feasible notion of redundant clauses with respect to sat-equivalence (like blocked clauses). Which is better: adding such clauses or deleting them?
Paul W. Purdom - No Name Problem
This is where the No Name problem description will go.
Ewald Speckenmeyer
Let I(n,k)^(m) be the set of all CNF formulas containing n
variables and m clauses, where each clause has exactly k literals.
Let f(n,m,k) be the minimum number of clauses which have to be removed
from formulas in I(n,k)^m in order to make them satisfiable.
What is f(n,m,k)?
By experiment, f(500, 5000, 3) is approximately 162.
Cosimo Spera - No Name Problem
This is where the No Name problem description will go.
References:
Send solution to urquhart@cs.toronto.edu
Allen Van Gelder - No Name Problem
This is where the No Name problem description will go.