Theorem Prover on Propositions in Finite Domains
Author Message
Theorem Prover on Propositions in Finite Domains

Hello,

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?

Jan van der Vorst

Sun, 07 Nov 1999 03:00:00 GMT
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/

Sun, 14 Nov 1999 03:00:00 GMT
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/

Sun, 14 Nov 1999 03:00:00 GMT

 Page 1 of 1 [ 3 post ]

Relevant Pages