Workshop on Satisfiability

Certosa di Pontignano
Universita Degli Studi Di Siena
Siena, Italy
April 28 - May 3, 1996

Open Problems

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

Hans Kleine Büning - All Literal Horn ( Workshop Slide)

INSTANCE: Satisfiable Horn formula F
QUESTION: Determine {l literal | F |= l}

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

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.


  1. R.L. Graham and H.O. Pollak, On embedding graphs in squashed cubes, in: Graph Theory and Applications, Springer Verlag Lecture Notes in Mathematics 303 (1972), 99-110.

  2. J. Kahn, Recent results on some not-so-recent hypergraph matching and covering problems, RUTCOR Research Report 4-91, Rutgers University, 1991. (see Conjecture 2.19 by Alon, Saks and Seymour)

Send solution to

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?


  1. Eiter & Gottlob, Identifying the minimal transversals of a hypergraph and related problems, SIAM J. Computing, 24(6): 1278--1304, 1995.

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.)

Problems Equivalent to IMUNSAT and SIMUNSAT

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:


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.

Alasdair Urquhart - Multilated Chessboards ( Workshop Slide)

Consider the following well known puzzle: given a chessboard with two diagonally opposite squares removed, can you cover it with dominoes each of which can cover two adjacent squares? The answer is of course negative because any domino must cover a black square and a white square, and diagonally opposite squares have the same colour. This puzzle, generalized to a 2n by 2n board, can be formalized as an unsatisfiable set of clauses. We use variables Dxy to symbolize: "Square x and square y are covered by a domino." For each square x, we have a positive disjunction saying that it must be covered by a domino that also covers an adjacent square, and a set of negative disjunctions saying that x cannot be covered by more than one domino. This set of clauses has size quadratic in n. Problem: show that these sets of clauses require super-polynomial size resolution refutations.


  1. "Automation of Reasoning," edited by J. Siekmann and G. Wrightson, Vol. 2, pp. 157-8, Springer-Verlag 1983.

  2. "Short proofs for tricky formulas," by B. Krishnamurthy, Acta Informatica, Vol. 22 (1985), pp. 253-275.

Send solution to

Allen Van Gelder - No Name Problem

This is where the No Name problem description will go.