Theorem Prover on Propositions in Finite Domains

:

: I am looking for an efficient algorithm that finds all solutions (if

: any) to a logical proposition (with operators AND, OR and NOT) in

: which all atoms are of the form : <attribute> is_element_of <set>

:

: The solution should be stated as a dual clause like :

:

: attrib1 is_element_of set1 AND NOT attrib2 is_element_of set2 AND ...

:

: in which set1, set2 etc. are nonempty sets

: (attribx is_element_of EMPTYSET is equivalent to FALSE),

: and all attrib1, attrib2 etc. are distinct.

:

: Of course there are simple algorithms that can convert any proposition

: to dual clause normal form. The expressions however I am dealing with

: are huge. I need an efficient algorithm to beat the combinatorial

: effects.

:

: Could you set me on the right track regarding a theory or possible

: even an algorithm preferably in Prolog?

:

You can use Davis-Putnam like algorithm for generating satisfying

valuations of a formula.

M. Davis, H. Putnam. A computing procedure for quantification

theory. J. Assoc. Comput. Mach., 1960, 7. pp. 201-215.

That is you choose recursively Boolean variables from the formula,

instantiate them with values {true,false} and propagate the values

into the formula.

--

Institute of Computer Science, Tartu University

http://www.cs.ut.ee/~tqnu/