On-line 2-satisfiability |
| |
Authors: | Brigitte Jaumard Paola Marchioro Aurora Morgana Rossella Petreschi Bruno Simeone |
| |
Affiliation: | (1) HEC-GERAD, Montréal, Canada;(2) Dipartimento di Matematica, Università La Sapienza , Roma, Italy;(3) Dipartimento di Statistica, Probabilità e Statistica Applicata, Università La Sapienza , Roma, Italy |
| |
Abstract: | We deal with the followingon-line 2-satisfiability problemP(m, n): starting fromC(0)=true, consider a sequence ofm Boolean formulasC(k) (inn variables and in conjunctive normal form), each of them being the intersection of the previous one with a single clause which is the union of two literals. Solve the sequence of 2-satisfiability problemsC(k)=true,k=1,...,m. It is well known that a 2-satisfiability problem involvingm clauses can be solved inO(m) time. Thus, by a naive approach one can solveP(m, n) in overallO(m
2) time. We present an algorithm with overallO(nm) time complexity, which for every formula not only checks its satisfiability, but also actually computes a solution (if any), and moreover, detects all forced and all identical variables. Our algorithm makes use of an efficient on-line transitive closure procedure by Italiano. We discuss two applications to the design of integrated electronic circuits and to edge classification in automated perception.To the memory of Bob Jeroslow |
| |
Keywords: | Satisfiability on-line algorithms transitive closure |
本文献已被 SpringerLink 等数据库收录! |
|