| Autor: |
Remshagen, Anja, Truemper, Klaus |
| Zdroj: |
Journal of Automated Reasoning; January 2005, Vol. 34 Issue: 1 p31-47, 17p |
| Abstrakt: |
Abstract 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. |
| Databáze: |
Supplemental Index |
| Externí odkaz: |
|
Full text from SpringerLink