In my opinion a very efficient and practical way to approach this sort of problem lies in rewriting all the connectives via a scheme developed by St. Lesniewski. I say this on the basis of finding short wffs equivalent to each of the binary and unary operators using just the connectives for "$\rightarrow$" and "$\lnot$", and having read that this scheme allows for efficient conversion to normal forms. This will not come as a complete description of the scheme here or how St. Lesniewski did it on paper exactly, but it does seem close enough for a start. First, I'll just write some of the connectives in this scheme. The "|-" here preferably will not get confused with "$\vdash$". I'll only list some of the members of each group.
1st group: |-, |-|
| | |
2nd group: o-, o-, -o-, -o-, o
|
For the members of the first group, if a false argument becomes true via the connective, then we draw a vertical line on the left end of the middle line. If a true argument becomes true, then we draw a vertical line on the right end of the middle line. If we do not draw a line in a position, then the argument represented by that position becomes false via the connective. Thus, for example, "-|" represents some connective for which the argument gets taken to a false value when the argument of the connective is false, and the argument gets taken to a true value when the argument of the connective is true.
For the members of the second group, if both arguments hold as false, and we have a line above the circle, then the connective takes that pair of values to a true value. If both arguments hold as true, and we have a line below the circle, then the connective takes that pair of values to a true value. If we have a line on the right side of the circle, and if the first argument qualifies as false and the second argument qualifies as true, then the connective takes that ordered pair of values to a true value. And the spot I've have mentioned comes as the other case as to when the connective takes the arguments to a true value, when we have a line in that spot. So, in St. Lesniewski's scheme
|
o- denotes the material conditional.
|
and
o denotes logical conjunction.
|
and
|- denotes logical negation.
and
-o- denotes logical disjunction.
|
So, in St. Lesniewski's scheme, you've wanted to find a way to represent
-o- using variables and the other connectives named above.
Counting the variables and the connectives both as symbols of the same class, it does come as possible to use only 8 symbols. I'll only write the connectives here unless you specifically request that I include the variables, instead of hinting at the 8 symbol solution that I know. Each of "( )", "[ ]", "{ }", "| |" represents some variable. You only need two symbols for variables. Here's the hint:
| | |
o- o- ( ) [ ] |- o- { } | |
| | |