History


Please fill in your query. A complete syntax description you will find on the General Help page.
An effective algorithm for the futile questioning problem. (English)
J. Autom. Reasoning 34, No. 1, 31-47 (2005).
Summary: In the futile questioning problem, one must decide whether acquisition of additional information can possibly lead to the proof of a conclusion. Solution of that problem demands evaluation of a quantified Boolean formula at the second level of the polynomial hierarchy. The same evaluation problem, called Q-ALL SAT, arises in many other applications. In this paper, we introduce a special subclass of Q-ALL SAT that is at the first level of the polynomial hierarchy. We develop a solution algorithm for the general case that uses a backtracking search and a new form of learning of clauses. Results are reported for two sets of instances involving a robot route problem and a game problem. For these instances, the algorithm is substantially faster than state-of-the-art solvers for quantified Boolean formulas.
WorldCat.org
Valid XHTML 1.0 Transitional Valid CSS!