scientific article; zbMATH DE number 1737608

Classical propositional logic (03B05) Complexity of computation (including implicit computational complexity) (03D15) Boolean functions (06E30) Logic programming (68N17) Analysis of algorithms and problem complexity (68Q25)

Review text

The paper deals with testing satisfiability of propositional logic programs represented as \(\alpha =C_1\land \dots \land C_n\), where the \(C_i\)'s are clauses. S.~Andrei introduced the following definitions and proved the following theorem. Denote: \[ \begin{aligned} r(C_1,\dots ,C_k) &= \Biggl|\text{atom}(\alpha)\setminus \Biggl \{A\mid A\in \bigcup _{j=1}^k C_j\Biggr\}\Biggr |,\\ \text{dif}(C_1,\dots ,C_k) &= \begin{cases} 0&\text{if } (\exists i<j)\;(\exists A)\;(A\in C_i\text{ and }\neg A\in C_j),\\ 2^{r(C_1,\dots ,C_k)} &\text{otherwise}, \end{cases} \\ \text{det}(\alpha) &= 2^{|\text{atom}(\alpha)|}- \sum _{k=1}^m(-1)^k\Biggl (\sum _{1\leq i_1<\cdots <i_k\leq m} \text{dif}(C_{i_1},\dots ,C_{i_k})\Biggr). \end{aligned} \] Theorem. (S. Andrei) \(\alpha \) is satisfiable iff \(\text{det}(\alpha)\neq 0\). The main contribution of the paper under review is an algorithm for testing satisfiability using this theorem. The algorithm is claimed to be more efficient than that of Iwama and Kazuo.

Recommendations

Cited in

(8)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4529644)