# Reduction of $3SAT$ to $2P2N-3SAT$ (without trivial clauses)

Given an instance of $$3SAT$$ the objective is to reduce it directly to $$2P2N-3SAT$$ without the reduction having any 'trivial' clauses. The trivial clauses can be where the same variable in a clause is used twice as follows: $$x+\overline{x}+y=1$$ or $$x+x+y=1$$. Both these clauses are trivial since the first is trivially TRUE and the second is obviously the 2 literal clause $$x+y=1$$.

The problem is $$NPC$$ but I am unable to find a complete reduction to it in any place.

The way I am approaching is as follows:

For each variable $$(x)$$, that occurs more that $$4$$ times as a literal, let the number of times it appears as positive and negative literal be $$P_x$$ and $$N_x$$ respectively. Assuming $$P_x > N_x$$ create $$P_x-2$$ new variables $$a_0, a_1, a_2...a_{P_x-2}$$. Now add clauses: $$\overline{x}+a_0=1;\overline{a_0}+a_1=1; \overline{a_1}+a_2=1;....;\overline{a_{P_x-2}}+x=1$$

This ensures that $$x=a_0=a_1=...=a_{P_x-2}$$. Now, we replace the third occurrence of $$x$$ and $$\overline{x}$$ with $$a_0$$ and $$\overline{a_0}$$ respectively, fourth with and $$a_1$$ and $$\overline{a_1}$$ so on.

Thus, we have ensured each literal occurs either once or twice. But we are still left with clauses of length 2, and we haven't yet enforced $$2P2N$$ constraint (with non trivial clauses). I am a bit lost how to proceed further.
{"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 1, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 22, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "https://cs.stackexchange.com/questions/161329/reduction-of-3sat-to-2p2n-3sat-without-trivial-clauses", "fetch_time": 1721376610000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2024-30/segments/1720763514900.59/warc/CC-MAIN-20240719074314-20240719104314-00260.warc.gz", "warc_record_offset": 162643114, "warc_record_length": 37864, "token_count": 440, "char_count": 1411, "score": 3.796875, "int_score": 4, "crawl": "CC-MAIN-2024-30", "snapshot_type": "latest", "language": "en", "language_score": 0.8185901641845703, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00042-of-00064.parquet"}