I have constructed a propositional theorem prover, and I am
quite curious to know whether it is as good as I expect it is.
Most propositional formulas that I manage to find appear to
be easily solvable or refutable (although typically construed
formulas such as the pigeonhole formulas, or random 3-CNFs in
the hard region can of course be chosen so large that these are
not solvable anymore).
So, I tried to apply my prover on the DIMACS benchmarks
solving all open problems in the accompanying list of results.
Recently I tried to solve all DIMACS96 benchmarks, solving
all but 3, which are all satisfiable, which is an area where
my tool performs badly. In order to find out whether I could
consider my results as competitive, I contacted the DIMACS96
workshop organizers but did not get any sensible response.
This leaves me in a confusing state. Is there anybody who
can help me in assessing the speed of my propositional
theorem prover? Does it make sense to write an article about
the blend of existing techniques that I use, or is there
somebody out there who has done so already (for a far more
competitive prover)? Are there people around
that have propositional formulas, preferably resulting from
some application that has been analyzed, that they cannot solve?
Is there anybody having results for DIMACS problems for
comparison?
Below I list results of the open DIMACS problems. My results
of the DIMACS96 problems and the syntax of input formulas.
With many greetings,
Jan Friso Groote
P.s.
For those who want to experiment with the code that I
have written, it is freely available and can be sent upon request.
Given the large number of correct results that have obtained,
I assume the code to be reasonably bug free. However, as I
experiment with it, among others by porting the code to
parallel computers and networks of computers, I cannot guarantee
bugfreeness.
----------------------------------------------------------------
Results of `DIMACS OPEN PROBLEMS' (In the accompanying table of
results these problems are left empty). The last column gives
the size of the formula (in uncompressed form).
bf0432-007.cnf Contradiction 322s (on SUN10). 54k
bf1355-075.cnf Contradiction 17s " 106k
bf2670-001.cnf Contradiction 8s " 48k
ssa2670-130.cnf Contradiction 44s " 42k
ssa7552-038.cnf Satisfiable 9s " 50k
----------------------------------------------------------------
Results of `DIMACS96' Benchmarks
The results have been obtained on a SPARC Ultra. The results
marked with an X could not be solved. Only the formula
as9-no.cnf is a contradiction. The others are satisfiable.
as1-yes.cnf X
as2-yes.cnf 1s
as3-yes.cnf 1s
as4-yes.cnf 2927s
as5-yes.cnf X
as6-yes.cnf 4s
as7-yes.cnf X
as8-yes.cnf 7s
as9-no.cnf 1s
as10-yes.cnf 19s
as11-yes.cnf 1s
as12-yes.cnf 3s
as13-yes.cnf 20s
as14-yes.cnf 1s
as15-yes.cnf 73s
tm1-yes.cnf 100s
tm2-yes.cnf 2s
---------------------------------------------------------------
Input syntax: Propositionletters are strings of letters
and digits, and may contain underscores. and is &, or is |,
if and only if is <->, implies is -> and not is ~. Brackets
may be used freely.
Examples of formulas:
(p|q|r)&
(~p|q|r)&
(c|r|q)
(((p->q)->p)->p)
(0<->1<->2<->3)<->(8->16)
----------------------------------------------------------------------
Jan Friso Groote
CWI
Department of Software Technology
Kruislaan 413
1089 SJ Amsterdam
The Netherlands
P.O.Box 94079
1090 GB Amsterdam
The Netherlands
Tel. +31 20 592 4232
Fax. +31 20 592 4199
E-mail jfg@cwi.nl
Home address
Schoenerstraat 49
3534 RL Utrecht
The Netherlands
Tel. +31 30 2431045