Using clausal graphs to determine the computational complexity of k-bounded positive one-in-three SAT

The one-in-three SAT problem is known to be NP-complete even in the absence of negated variables [T.J. Schaefer, The complexity of satisfiability problems, in: Proceedings of the 10th Annual ACM Symposium on Theory of Computing, ACM, New York, 1978, pp. 216–226], a variant known as positive (or monotone) one-in-three SAT. In this note, we use clausal graphs to investigate a further restriction: image-bounded positive one-in-three SAT (imageBP one-in-three SAT), in which each variable occurs in no more than image clauses. We show that for image, image BP one-in-three SAT is in the polynomial complexity class image, while for all image, it is NP-complete, providing another way of exploring the boundary between classes image and NP.