From konarj@eua.ericsson.se Fri Apr 8 18:25:52 EDT 1994
Article: 21558 of comp.ai
Xref: glinda.oz.cs.cmu.edu comp.ai:21558 comp.theory:9583 sci.logic:6533
Path: honeydew.srv.cs.cmu.edu!nntp.club.cc.cmu.edu!birdie-blue.cis.pitt.edu!gatech!howland.reston.ans.net!pipex!sunic!sics.se!eua.ericsson.se!eua.ericsson.se!konarj
From: konarj@eua.ericsson.se (Arndt Jonasson)
Newsgroups: comp.ai,comp.theory,sci.logic
Subject: Hard sequences (summary)
Date: 8 Apr 1994 12:27:57 GMT
Organization: Ellemtel Telecom Systems Labs, Stockholm, Sweden
Lines: 141
Distribution: inet
Message-ID: <2o3ikd$44c@euas20.eua.ericsson.se>
NNTP-Posting-Host: euax1i7c11.eua.ericsson.se
NNTP-Posting-User: konarj
A while ago, I posted a request for "hard propositional formula sequences",
and I promised to post a summary of the answers. Here it is.
A few comments on my own. A few people suggested generating random
formulas. These are good for testing the limits of theorem provers in
practice, but not so useful for theoretical purposes (as far as I
know), for example for proving that one proof system is strictly
better than another one.
Personally, i haven't had time to investigate any of the suggestions
(not even to look at the suggested ftp site). But I will! Thanks to
all who answered.
Arndt Jonasson FH tel 5707 ~konarj
Logikkonsult NP AB konarj@eua.ericsson.se
============================================================
[First my own request:]
I'm on the hunt for "hard" formula sequences in propositional
logic. By a formula sequence I mean a sequence F(n) of propositional
tautological logic formulas, for n=1..infinity.
A sequence F(n) is hard for a proof system P if the length of the
proofs in P for deciding the truth of F(n) grows as an exponential
function of n.
Such sequences can be used to separate the relative strengths of
proof systems (tree resolution, resolution, and so on).
I'm playing around with propositional theorem provers, and would like
to know what formula sequences are commonly used for this purpose,
plus any others you may come up with.
============================================================
>From David Mitchell <mitchell@cs.toronto.edu>:
I have been working on the dual, satisfiability testing.
Some formulas that are used for testing SAT procedures are:
- The random CNF formulas with a high ratio of clauses
to variables have exponential resolution proof on average
(Chvatal and Sczemerdi)
- These random formulas are not known to be hard at lower
ratios, but at ratios where the probability of a given
formula being satisfiable is about .5, they appear to be
very hard in practice for current methods.
- There is a collection of formulas available by ftp from
Dimacs at Rutgers University which is being assembled
as a test bed. They include formulas encoding hard
graph colouring problems, parity problems, and VLSI
testing instances, amoung others. (There are also some
SAT programs there)
[In other words, ftp to dimacs.rutgers.edu]
Look in /pub/challenge/sat/*
There are lots of benchmark formulas in
/pub/challenge/sat/benchmarks/cnf/*, but I'm not at
all up to date on what is in there now. Hopefully
the documentation is clear enough to guide you.
Some of these may be useful from a theorem proving
point of view, but probably many are not.
The file /pub/challenge/sat/benchmarks/cnf/contents.tex
has brief descriptions, and relevant papers or longer
descriptions can be found in
/pub/challenge/sat/contributed/* under author's
names. (Also there you can find code for some
SAT testing programs -- some of them quite good).
A description of the random CNF formulas we sometimes
use for testing can be found in
/pub/challenge/sat/contributed/selman/hsat.ps*
============================================================
>From stefan@nada.kth.se:
[translated from Swedish]
Random formulas: Select number of variables, k and the number of
random formulas in such a way that the probability that the formula
is satisfiable is about 0.5, and all clauses occur with the same
probability. After some tries you will always find a formula that
an arbitrary method won't handle.
============================================================
From: sbuss@math.UCSD.EDU (Sam Buss):
In response to your sci.logic post asking about hard
tautologies for propositional logic. I am writing
a paper with M.L.Bonet and T.Pitassi discussing tautologies
which might be *conjectured* to require exponential length
Frege proofs and yet have polynomial size extended Frege
proofs. Some of these examples might be good candidates for
you.
We mostly consider tautologies based on combinatorial
theorems, most notably, the Odd-town theorem, the Graham-Pollak
theorem, Frankl's theorem and Bondy's theorem. Of these,
we know polynomial size propositional proofs only for the
Bondy's theorem, which is proved to be equivalent to the
pigeonhole principle w.r.t constant-depth polynomial
size proofs.
============================================================
From: toni@cs.ucsd.edu (Toni Pitassi)
[...] if you are only interested in hard examples for
Resolution or small-depth Frege systems, then there are
plenty of other examples, all based on some form of mod p
counting. One is the ''mod p'' principle,
introduced by Ajtai, stating that there is no way to partition
pn+1 elements into disjoint classes, each of size p.
Another example are the Tseitin graph tautologies. Here you
start with a connected graph, where each vertex has a charge
of either 0 or 1, and the sum of all charges is odd. The
underlying propositional formula contains variables for each edge,
and the tautology states that the mod 2 sum of all of the edges into
a vertex cannot be equal to the charge for every vertex.
============================================================
From: djimenez@naiad (Daniel Jimenez):
My favorite is primality testing by building a circuit that multiplies
two numbers and ANDs either the outputs or the complements of the outputs
depending on the coressponding bit in the number you are testing.
Such a circuit can be converted to CNF (or even 3CNF) using one of the
standard NP-completeness proofs for CNF-SAT (see Rivest's Algorithms book
for one).
If no satisfying assignment exists, the number is prime (as long as you
don't allow the number itself to be an input). If you use known composite
numbers, there is always a satisfying assignment.
These kinds of formulas have always stumped my theorem provers.
--
Arndt Jonasson FH tel 5707 ~konarj
Logikkonsult NP AB konarj@eua.ericsson.se