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 : 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