#2,2-SAT is solvable in linear-time

A linear-time algorithm, with respect to the size of the instance Boolean formula, is presented for the #SAT problem restricted to formulae of the form #2; 2-CF, i.e. formulae whose clauses have just two literals and in which each variable appears at most twice. Keyword: Satisfiability, #SAT problem, counting problem, linear-time algorithm. 1 Introduction 1.1. The satisfiability problem for Boolean formulae, SAT, is NP-complete, as was shown by Cook [2]. Its restriction, 2-SAT, to formulae whose clauses have just two literals can be solved in linear time [5], but the corresponding "optimization" and "counting" problems Max2SAT (given a 2-formula find an assignment which maximizes the number of satisfied clauses), and #2-SAT (given a 2-formula count the number of assignments satisfying all the clauses), are NP-hard. 1.2. From the standpoint of NP-completeness, one basic approach to compare the problem classes P and NP is to consider for a NP-complete problem a restriction of it in P, a..