Number of solutions for a given logical equation I came across the following question while studying logic and cannot find a solution for it anywhere. I am studying by myself and think I just don't know exactly the right terms to search for it online (I'm not sure it is called a logical equation so excuse the title of this question in case it isn't):

Given the proposition $P$, it's logical value is defined as $[P] = 0$, in case $P$ is false, and $[P] = 1$, in case $P$ is true.
Consider the following open sentences defined in the set of integers:
$ P_i(x): x \le 5$
$ P_{ii}(x): x \ge 3$
$ P_{iii}(x): $ x is odd 
$ P_{iv}(x): x \ge 6$
How many solutions does the following equation have?
$ x = [P_i(x)] + 2 \cdot[P_{ii}(x)]+3\cdot[P_{iii}(x)]+4\cdot[P_{iv}(x)]$

I've made this jsfiddle and from there, I can count the number of solutions through a loop. In this case I've looped from 0 to 1000 and it yields 2 solutions. Though I can clearly reason it wouldn't be possible for a very large number to work here, since these are all sums of multiplications of 0s or 1s, I am having a hard time articulating exactly why. How would you go about finding the largest number possible, in this very specific case? So you wouldn't have to loop through values of X too far off from it?
 A: First, let's observe that $[P_i(x)]+4\cdot[P_{iv}(x)]=1+3\cdot[P_{iv}(x)]$. We can check three cases:


*

*$x<3$: Our equation becomes $x=1+3\cdot(x\%2)$ where $\%$ is the mod operator. Clearly, no even number can satisfy this equation, and neither can an odd number. So, $x\geq3$.

*$3\leq x<6$ We can convert the equation to $x=3+3\cdot(x\%2)$. Again, no even or odd numbers can satisfy this equation, so we move on to case three.

*$x\geq6$ Since we know any solution must satisfy this, we can convert the equation to $6+3\cdot(x\%2)$. So, $x=6$ and $x=9$ are solutions.
Hence, there are $\color{red}{2}$ solutions to this equation.
A: Here's how this problem would be coded in the SMT-LIB format, understood by most SMT solvers.
(define-fun Pi ((x Int)) Int (ite (<= x 5) 1 0))
(define-fun Pii ((x Int)) Int (ite (>= x 3) 1 0))
(define-fun Piii ((x Int)) Int (mod x 2))
(define-fun Piv ((x Int)) Int (ite (>= x 6) 1 0))
(declare-const x Int)
(assert (= x (+ (Pi x) (* 2 (Pii x)) (* 3 (Piii x)) (* 4 (Piv x)))))
(check-sat)
(get-model)
(assert (not (= x 6)))
(check-sat)
(get-model)
(assert (not (= x 9)))
(check-sat)
(exit)

After getting the first solution, we add a constraint that forbids that solution and solve again.  When we do it again, the SMT solver reports that the constraints are now unsatisfiable; hence we know that we have enumerated all solutions.
A: Other answers show how to get a full solution, with a bit of thought/work. But a very quick observation that narrows down the possibilities is that since logical functions can only take values $0$ and $1$, the right-hand side can’t be more than $1 + 2\cdot1 + 3\cdot1 + 4\cdot1 = 10$, and can’t be less than $0$.  So the only values you need to try for $x$ are $\{0, 1, …, 10\}$.
This is something always worth thinking of: when some complex function (like the right-hand side here) is built out of other functions, if you know restrictions/bounds on the pieces it’s build out of, then those will often give restrictions/bounds on the complex function.
(Justifying the bounds in detail: if $a \geq 0$ and $0 \leq b \leq 1$, then $0 \leq ab \leq a$.  So $0 \leq 2\cdot [P_2(x)] \leq 2$, and so on; so for any $x$, $$0 = 0 + 0 + 0 + 0 \leq [P_1(x)] + 2\cdot [P_2(x)] + 3\cdot [P_3(x)] + 4\cdot [P_4(x)] \leq 1 + 2 + 3 + 4 = 10$$
and so in particular, if $x = [P_1(x)] + 2\cdot [P_2(x)] + 3\cdot [P_3(x)] + 4\cdot [P_4(x)]$, then $0 \leq x \leq 10$.)
A: In addition to @Rushabh Mehta's answer:
note that $[P_i]$ can be seen as a "classic" (aka Pre-Calculus) function. For example,  $f_1=[P_1]$ is simply the function $$f_1(x)=[P_1(x)]=\left\{ \begin{array}{rl} 1, & x \leqslant 5 \\ 0, &x>5 \end{array} \right.$$
Therefore, you can study the given equation $x=f_1(x)+2f_2(x)+3f_3(x)+4f_4(x)$ using all techniques you already knows for this kind of problems: considering cases (as in Rushabh Mehta's answer), drawing the graph carefully,...
