Solving query-answering problems using all-solution satisfiability solvers: Algorithm and correctness

Query-answering (QA) problems have attracted wider interest recently, owing partly to emerging applications involving integration between rules and ontologies in the Semantic Web´s layered architecture. Success of using satisfiability (SAT) solvers as low-level solvers for dealing with several kinds of problems motivates us to apply SAT solvers to a class of QA problems. To find all elements of an answer set, a variant of a usual SAT solver, called an all-solution satisfiability (All-SAT) solver, is used for determining all models of a given input set of propositional clauses. Using an All-SAT solver, we propose a procedure for solving QA problems. The procedure generates input for an All-SAT solver from a high-level description of a given QA problem by problem transformation in a clause space that includes set-bounded variables. Based on the equivalent transformation principle, the correctness of the proposed procedure is shown.