1
$\begingroup$

Theorem. Let none of the assignments of length $\log n$ make a set of unsatisfiable 2-clauses. Then formula is satisfiable.

$n$ is input length here.

Let we name an assignment that make the formula to contain unsatisfiable 2-SAT contradictive.

This allows us to find all minimal contradictive assignments in $O(n^{\log n})$ time. And we can make a new formula. However, if formula we got is not in $P$, can we say, that original formula is satisfiable?

Example of one is just unsatisfiable full CNF that has $\log n$ variables involved.

Second example is $x_1\land(\overline{x_1}\lor x_2)\land...\land(\overline{x_1}\lor...\lor x_{k-1})\land(\overline{x_1}\lor...\lor\overline{x_{k-1}}\lor x_k)\land(\overline{x_1}\lor...\lor\overline{x_k})$. This formula is Horn CNF and solvable in linear time.

Trying to solve this in a way of generating formulas.

Let we have a formula $f$ from class $P$ and a set of 2-clauses $g$.

Then, moving literals from $f$ to $g$ and negating them will allow to generate any 3SAT instance.

If $f$ is Horn SAT, then resulting formula will not have any restrictions that Schaefer's dichotomy theorem says. E.g. there can be both Horn and dual Horn clauses of length 3, which are not combined to XOR clauses.

This made me more sure that conjecture is true. And now I even think that if it is impossible to find Horn SAT that implies contradiction, then formula is satisfiable. Of course, finding such Horn formula takes polynomial time.

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ "However, if formula we got is not in P" -- what does that even mean? A single problem instance can never be a member of P. $\endgroup$
    – Raphael
    Commented Aug 13, 2017 at 12:39
  • 1
    $\begingroup$ @Raphael, I mean that it must be an instance of Horn-renamable-SAT/2-SAT/XOR-SAT or SAT that has $\log n$ variables. I think, this can be checked in polynomial time. $\endgroup$
    – rus9384
    Commented Aug 13, 2017 at 12:51
  • $\begingroup$ What is the length of an assignment? What does it mean for an assignment to make a set of unsatisfiable 2-clauses? Also please edit the question to address the feedback from Raphael; his comment is absolutely correct, and what you are saying reflects a misunderstanding of what it means to be in P. Finally, what is your question, exactly? $\endgroup$
    – D.W. ♦
    Commented Aug 14, 2017 at 4:02

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.