The Role of Reformulation in the Automatic Design of Satisfiability Procedures
- VanBaalen, Jeffrey
- Apr. 1992.
- Physical Description:
- 1 electronic document
- Restrictions on Access:
- Unclassified, Unlimited, Publicly available.
- Recently there has been increasing interest in the problem of knowledge compilation (Selman & Kautz91). This is the problem of identifying tractable techniques for determining the consequences of a knowledge base. We have developed and implemented a technique, called DRAT, that given a theory, i.e., a collection of firstorder clauses, can often produce a type of decision procedure for that theory that can be used in the place of a general-purpose first-order theorem prover for determining many of the consequences of that theory. Hence, DRAT does a type of knowledge compilation. Central to the DRAT technique is a type of reformulation in which a problem's clauses are restated in terms of different nonlogical symbols. The reformulation is isomorphic in the sense that it does not change the semantics of a problem.
- Document ID: 19960047165.
Accession ID: 96N32927.
Proceedings of the Workshop on Change of Representation and Problem Reformulation; 161-172; NASA-TM-111484.
- No Copyright.
View MARC record | catkey: 15649937