Disclaimer: this is a repost of a MS question with the same title — https://math.stackexchange.com/questions/5072398/complexity-of-the-clause-fragment-of-%c5%81ukasiewicz-logic
People who know the semantics of Łukasiewicz logic may skip to the ‘the question proper’ part of the description.
A reminder on the semantics of Ł
Variables are evaluated over $[0,1]$; there are three connectives: $\neg$, $\odot$, and $\oplus$ defined as follows:
$$v(\neg\phi)=1-v(\phi)\quad v(\phi\odot\chi)=\max(0,v(\phi)+v(\chi)-1)\quad v(\phi\oplus\chi)=\min(1,v(\phi)+v(\chi))$$
A formula $\phi$ is $1$-satisfiable when there is a valuation $v$ s.t. $v(\phi)=1$. A formula $\phi$ is positively satisfiable when $v(\phi)>0$ for some $v$.
A prelude to the question
As usual, literals are propositional variables and their negations, and $\oplus$-clauses are literals joined with $\oplus$. We know that $1$-satisfiability of sets of $\oplus$-clauses (i.e., whether there is a valuation where every clause has value $1$) can be checked in polynomial time. Indeed, we just transform every clause
$$\bigoplus\limits^m_{i=1}p_i\oplus\bigoplus\limits^n_{j=1}\neg q_j$$
into
$$\sum\limits^m_{i=1}x_{p_i}+\sum\limits^n_{j=1}(1-x_{q_i})\geq1$$
which gives us a system of linear inequalities over $\mathbb{R}$. Likewise, sets of clauses can be checked for positive satisfiability in polynomial time.
Note, however, that the above definition of the satisfiability of sets of clauses (all clauses should have value above $0$) does not correspond to the $\odot$-joining of clauses but rather to $\wedge$-joining (with $v(\phi\wedge\chi)=\min(v(\phi),v(\chi))$). Indeed, it is possible that $v(\phi)>0$ and $v(\chi)>0$ but $v(\phi\odot\chi)=0$ (e.g., set $\phi=p$, $\chi=\neg p$ and $v(p)=\frac{1}{2}$).
The question proper
Thus, if we want to know whether a set of clauses $\{\kappa_1,\ldots,\kappa_m\}$ is satisfiable, it makes sense to check whether $\bigodot\limits^m_{i=1}\kappa_i$ is positively satisfiable. An additional benefit is that it works well with the order-entailment:
$$\phi\models_\leq\chi\text{ iff }\forall v:v(\phi)\leq v(\chi)$$
gives us
$$\phi\odot\chi\models_\leq\psi\text{ iff }\phi\models_\leq\neg\chi\oplus\psi$$
Now, the question is as follows: given $\phi=\bigodot^n_{j=1}\left(\bigoplus^m_{i=1}p^j_i\oplus\bigoplus^{m'}_{i'=1}\neg q^j_{i'}\right)$, what is the complexity of deciding its positive satisfiability?
Note that if all clauses have at least two literals, $\phi$ is trivially $1$-satisfiable (just evaluate everything at $\frac{1}{2}$). And if there is only one single-literal clause in $\phi$, the same argument results in immediate positive satisfiability.
Thus, the question is whether there is a polynomial algorithm for deciding positive satisfiability of $\odot$-conjunctions of $\oplus$-clauses when there are many single-literal clauses and many clauses with two or more literals.
A simple but wrong solution
Observe that ‘naive single-pass resolution’ does not work:
$$p\odot q\odot(\neg p\oplus\neg q)\odot(\neg p\oplus q)$$
is, of course, positively unsatisfiable. But if we begin resolution with the second clause, and not the first one, we get $\neg p\odot q$. Note, furthermore, that in general, one cannot reuse a literal to resolve several clauses because $p$ and $p\odot p$ are not equivalent.