1
$\begingroup$

I am trying to proof by resolution the following:

1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
$\{\{a+b < a*b\}; \{x_2 \not< y_2, x_2 + y_2 << x_2 * y_2\}; \{x_2 \not<< y_2, x_2 + y_2 <<< x_2 * y_2\}; \{x \not<<< y\}\}$

Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.

I don't manage to find suitable instances of the clauses. Do you have any idea?

2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols.

I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?

I'd appreciate your help on this! :)

$\endgroup$
  • $\begingroup$ If anything is unclear in my post, please let me know. $\endgroup$ – Studentu Dec 9 '18 at 22:06
1
$\begingroup$

proof by resolution that the following CNF is unsatisfiable:
$\{\{a+b < a*b\}; \{x_2 \not< y_2, x_2 + y_2 \ll x_2 * y_2\}; \{x_2 \not\ll y_2, x_2 + y_2 \lll x_2 * y_2\}; \{x \not\lll y\}\}$

You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 \not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses,

\begin{align*} & a+b < a*b\\\\ & a+b \not< a*b\\ & (a+b) + (a*b) \ll (a+b) * (a*b)\\\\ & (a+b) + (a*b) \not\ll (a+b) * (a*b)\\ & ((a+b)+(a*b))+((a+b)*(a*b)) \lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\ & ((a+b)+(a*b))+((a+b)*(a*b)) \not\lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\ \end{align*}

Applying the resolution method is now trivial.


For question number 2 consider,

\begin{align*} &\{a+b <_1 a*b\}\\ % &\{x_k \not<_{(k-1)} y_k,\ x_k + y_k <_k x_k * y_k\}\quad 1<k<n\\ &\{x_{n} \not<_{n-1}< y_{n}\} \end{align*}

and to instantiate the free variables consider terms, $s_0 = a$, $t_0 = b$, $s_k =s_{(k-1)}+t_{(k-1)}$ and $t_k =s_{(k-1)}*t_{(k-1)}$, and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.

$\endgroup$
  • 1
    $\begingroup$ Indeed that's what I did. A set such as $\{x2≪̸y2,x2+y2⋘x2∗y2\}$ is typically a a schema, that is shorthand notation for a union $\bigcup\{\{x2≪̸y2,x2+y2⋘x2∗y2\} | x2, y2 \in \mathcal{D}\}$ where $\mathcal{D}$ is their domain. $\endgroup$ – Jorge Adriano Dec 10 '18 at 1:09
  • 1
    $\begingroup$ That's the only way I can make sense of the question. Unless if you meant to write $x1≮y1,x1+y1\ll x1∗y1$ rather than $x2≮y2,x2+y2≪x2∗y2$ in the second set of your question. If you do that, then you have different variables to instantiate. Regardless each of those sets should have their variables instantiated with different values, that's the only way the question makes sense. $\endgroup$ – Jorge Adriano Dec 10 '18 at 1:17
  • 1
    $\begingroup$ For the second question you just have to generalise this example from 4 to $n$ clauses. In this example with each (instantiated) clause the number of symbol doubles. $\endgroup$ – Jorge Adriano Dec 10 '18 at 1:31
  • 1
    $\begingroup$ edited with some detail on question 2 $\endgroup$ – Jorge Adriano Dec 10 '18 at 2:31
  • 1
    $\begingroup$ Yes, should be $n$. And yes that's it from the clauses with $O(n)$ symbols you get via substitutions the clauses with no free variables and $O(2^n)$ symbols (note it is exponential, not just polynomial). $\endgroup$ – Jorge Adriano Dec 10 '18 at 10:57

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.