Is there an (efficient) algorithm to determine whether an equation of two terms in the language of elementary set theoretic operators is an identity?

By elementary set theoretic operations I refer to those which are usually imaged in Venn diagrams -- union, intersection, set difference, etc. In the formulation of my question I included the word efficient'' between parentheses because in computing complexity this term is used with different meanings and here I am not very interested in complexity. I would like to learn about any algorithm which would not just "exhaust all possibilities" (like substituting 0s and 1s, in case of boolean terms), an algorithm which would be useful or instructive when implemented as a computer program.

This question naturally came after another question of mine: Is the equational theory of generalized boolean algebras decidable?

As a follow-up to Andreas Blass's answer, a good reference is Fascicle 6 of Volume 4 of Don Knuth's Art of Computer Programming, which is devoted to Satisfiability. In a nutshell, most propositional SAT algorithms may be roughly divided in two classes: algorithms based on random walks, and conflict-driven clause-learning (CDCL) algorithms.

There has been steady progress in these algorithms over the last two decades. CDCL algorithms, in particular, have many practical applications and are capable to both prove and refute satisfiability. In fact, they produce resolution proofs in the latter case. (Sometimes these proofs are quite large.)

It is not uncommon for these SAT solvers to decide problem instances with hundreds of thousands of propositional variables and millions of clauses. Their worst-case runtime is still exponential, and they are sometimes stumped by much smaller problem instances. Still, from an engineering standpoint they are little marvels and definitely worthy of your attention. Source code is available for some of the best tools like lingeling or glucose.

The theory you describe is decidable, by the algorithm you mentioned but don't want, namely substituting 0's and 1's in all possible ways. Indeed, deciding whether a Boolean equation (using $$\cap,\cup,-$$) is an identity amounts to deciding whether a formula in propositional logic is a tautology. Whether this can be done in polynomial time is a big open problem (the P=NP problem). Nevertheless, much is known about algorithms that, in many cases, work much better than the plug-in-0's-and-1's algorithm. In particular, people have programmed heuristics for guessing which combinations of 0's and 1's are likely to give counterexamples. I'm not an expert on these methods, but until an expert comes along and gives you a better answer, you could google "SAT-solvers" and find a good deal of information. ("SAT" refers to the problem of deciding whether a formula in propositional logic is satisfiable; that's equivalent to asking whether the formula's negation is not a tautology, so it's essentially the same question for your purposes.)