Information Technology Reference
In-Depth Information
some new truth-value using another selection heuristic select val ( α, p, h ). Such
selections of variables and such changes of their truth-values are repeated until
either h ( α )
∈ d or the allocated time to modify h into a satisfying valuation has
elapsed. The process is repeated (if needed) up to a specified number of times.
The above procedure defines informally an incomplete SAT M solver (clearly,
it cannot be used to determine unsatisfiability of a formula).
Polarity and SAT M . The classical notion of polarity of a variable p in a
formula α ( p ) captures the monotonic behavior of the term operation f α ( p )in-
duced by α ( p )over p in a partially ordered algebra of truth-values. The selection
heuristics select var ( α, h )and select val ( α, p, h )ofanSAT M solver can be de-
fined in terms of polarity. This is done in the non-clausal solver polSAT for
classical propositional logic as well as in its extensions to finitely-valued logics
(cf. [12]).
Improving the Eciency of Resolution with SAT M Solvers. An unre-
stricted use of the resolution rule during the deductive process may very quickly
result in combinatoric explosion of the set of deduced resolvents making the
completion of a reasoning task unattainable in an acceptable amount of time. In
an ecient resolution-based reasoning program the generation of resolvents that
would evidently have no impact on the completion of a reasoning task must be
blocked. Tautological resolvents are just that sort of formulas.
For many resolution logics the tautology problem is coNP-complete. For some
of these logics, SAT M solvers can be used to guide the search for refutation so
that the use of tautologies during the refutation process is unlikely. At the same
time the refutational completeness of the deductive process is preserved.
References
1. Blok, W.J. and Pigozzi, D. Algebraizable Logics . Memoirs of the American Math-
ematical Society, vol. 77, no 396 (1989).
2. Denecke, K. and Wismath, S.L. Universal Algebra and Applications in Computer
Science , Chapman & Hall/CRC (2002).
3.Fitting,M.andOrlowska, E. (eds.) Beyond Two: Theory and Applications of
Multiple-Valued Logic . Studies in Fuzziness and Soft Computing, Phisica-Verlag
(2003).
4. Fitting, M. Bilattices and the semantics of logic programming. Journal of Logic
Programming 11, pp. 91-116 (1991).
5. Ginsberg, M.L. Multivalued logics: a uniform approach to reasoning in artificial
intelligence. Comput. Intell. , vol. 5, pp. 265-316.
6. Hahnle, R. Automated Deduction in Multiple-Valued Logics . Clarendon Press
(1993).
7. Kraus, S., Lehmann, D. and Magidor, M. Nonmonotonic Reasoning, Preferential
Models and Cumulative Logics. Artificial Intelligence 44, pp. 167-207 (1990).
8. Makinson, D. General Patterns in Nonmonotonic Reasoning. In Handbook of Logic
in Artificial Intelligence and Logic Programming . Vol 3: Nonmonotonic and Un-
certain Reasoning (Gabbay, D.M., Hogger, C.J., and Robinson J.A. eds.). Oxford
University Press (1994).
Search WWH ::




Custom Search