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.
Similar content being viewed by others
References
B. Aspvall, M.F. Plass and R.E. Tarjan, A linear-time algorithm for testing the truth of certain quantified Boolean formulas, Inform. Process. Lett. 8 (1979) 121–123.
S. Cook, The complexity of theorem proving procedures,Proc. 3rd ACM Symp. on Theory of Computing (1971) pp. 151–158.
S. Even, A. Itai and A. Shamir, On the complexity of timetable and multicommodity flow problems, SIAM J. Comput. 5 (1976) 691–703.
T. Ibaraki and N. Katoh, On-line computation of transitive closure for graphs, Inform. Process. Lett. 16 (1983) 95–97.
G.F. Italiano, Amortized efficiency of a path retrieval data structure, Theoretical Computer Sci. 48 (1986).
R.M. Karp, Reducibility among Combinatorial Problems, in:Complexity of Computer Computations (Plenum, New York, 1972) pp. 85–104.
R. Petreschi and B. Simeone, A switching algorithm for the solution of quadratic Boolean equations, Inform. Process. Lett. 11 (1980) 193–198.
R. Petreschi and B. Simeone, Numerical comparison of 2-satisfiability algorithms, TR-9, Dept. of Statistics, University “La Sapienza”, Rome (1988).
R. Raghavan, J. Cohoon and S. Sahni, Single bend wiring, J. Algorithms 7 (1986) 232–257.
E. Rich,Artificial Intelligence (McGraw-Hill, New York, 1983).
B. Simeone, Consistency of quadratic Boolean equations and the König-Egerváry property for graphs, Ann. Discr. Math. 25 (1985) 281–290.
D.L. Waltz, Understanding line drawings of scenes with shadows, in:The Psychology of Computer Vision (McGraw-Hill, New York, 1975).
P.H. Winston,Artificial Intelligence (Addison-Wesley, Reading, MA, 1984).
Author information
Authors and Affiliations
Additional information
To the memory of Bob Jeroslow
Rights and permissions
About this article
Cite this article
Jaumard, B., Marchioro, P., Morgana, A. et al. On-line 2-satisfiability. Ann Math Artif Intell 1, 155–165 (1990). https://doi.org/10.1007/BF01531076
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01531076