FWIW, the Common Lisp "Boyer" standard benchmark performs propositional logic tautology testing. The following 2 short papers give a bit of detail on how Bob Boyer's algorithm works. http://home.pipeline.com/~hbaker1/LBoyer.html http://home.pipeline.com/~hbaker1/LBoyer.ps.gz http://home.pipeline.com/~hbaker1/BoyerB.html http://home.pipeline.com/~hbaker1/BoyerB.ps.gz At 01:28 PM 12/4/2016, rcs@xmission.com wrote:
True. In fact, you can go a step further and reduce (P v ~P) to T.
The catch is that the simple algorithm requires, in effect, trying all combinations of the variables. The work is about 2^V for V variables. The Satisfiability problem asks "is there any choice of variables that makes the formula f(a,b,c,...) true?". The co-problem asks "is f(...) true for every combination?" SAT is verifiable if you can find one choice that works; co-SAT is refutable by one counterexample. But to confirm a tautology requires checking all examples, or some equivalent, mathematically sound, procedure.
This limits verification to ~50 variables (depending on your computer and your patience). Similarly for a search for a SAT example. There are algorithms & heuristics that improve this situation somewhat, but the problems appear to be of exponential difficulty. There's an annual(?) contest of SAT-solvers; I think the best can handle hard problems of a few hundred variables. Easy problems can be much bigger, with thousands of variables. These have some real world uses.
I don't think Henry expected to go beyond, say, 20 variables. A complete list of tautologies with even 10 variables and a few occurrences of each variable would be very big.
Imagine a binary hypercube of dimension V, hypervolume 2^V cells. Your job is to completely cover the hypercube with bricks of volume 1/8 of the total, with overlap permitted. This might represent the truth-volume of the clause (C & ~F & H). Your formula has about 4.3 V clauses. Each has 3 variables, and the clauses are ORed together to make the formula. Is it a tautology? Observationally, it seems to be about a 50:50 proposition. 10 variables makes 960 clauses of this shape (8 for the negation patterns, times bin(10,3)=120 for the variable choices). Select 43 clauses at random: do they cover the whole hypercube? If 50% of the formulas do, that's .50 * bin(960,43) tautologies.
Rich
---------- Quoting Dan Asimov <asimov@msri.org>:
I would have guessed that any tautology can be reduced algorithmically to a simpler formula until it becomes p v ~p ???
(So that if the algorithm can't find such a reduction, then that proves it wasn't a tautology.)
My main evidence to the contrary is that Rich didn't mention this.
?Dan
On Dec 3, 2016, at 6:40 PM, Allan Wechsler <acwacw@gmail.com> wrote:
What does it mean to "solve" a tautology? Is this somehow equivalent to boolean satisfiability?
On Sat, Dec 3, 2016 at 9:36 PM, Henry Baker <hbaker1@pipeline.com> wrote:
At 06:28 AM 12/3/2016, Henry Baker wrote:
1. Is there an easy way to enumerate/generate (all and only) *tautologies* in more-or-less increasing complexity fashion? By complexity, I mean more-or-less increasing fashion wrt the number of distinct variables and the size of the expression.
I thought about this during a long drive today and realized that there *can't* be an "efficient" (P) algorithm to enumerate all and only tautologies, else that algorithm would itself be useful to solve tautologies, and hence P=NP.
So Rich's idea of generating formulae and then doing tautology-testing may well be nearly optimal.