
It is experimentally shown that the satisfiability for Horn clauses algorithm (Dowling, Gallier) is efficient. The authors propose two relaxation schemes which map instances of a satisfiability problem for propositional formulae into problem instances for Horn clauses. One of the resulting algorithms runs in experiments several times faster than the Davis-Putnam algorithm.
efficiency, Logic, Analysis of algorithms and problem complexity, satisfiability for Horn clauses algorithm, Theorem proving (deduction, resolution, etc.)
efficiency, Logic, Analysis of algorithms and problem complexity, satisfiability for Horn clauses algorithm, Theorem proving (deduction, resolution, etc.)
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 69 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 1% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
