1
$\begingroup$

Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula.

It is recommended to do this if $n$ is small, but if $n$ is large, then practically this is not possible to build karnaugh map for the whole given boolean formula, but this is still possible practically to build karnaugh map to some subformula, that contains less and few boolean variables.

In 3SAT, the given boolean formula is always conjunctive normal form, where each clause in the given boolean formula is disjunction of at most 3 literals.

It is practically possible from the given 3CNF formula, to choose 5 clauses arbitrarily and build for them karnaugh map.

For 5 clauses, the number of possible different boolean variables is at most 15, so the size of the karnaugh map is at most 215=32768, which is constant.

But of course it is practically to build karnaugh map for more than 5 clauses as long as there is no too many boolean variables in the boolean subformula.

Let's restrict that the number of boolean variables in the subformula is at most 16, so the size of the karnaugh map is at most 216=65536, which is also constant.

That way it is possible to minimize larger subformula to smaller formula, which suppose to be equivalent, because they have the same truth table and thus replace the subformula with it's minimal equivalent.

Do this for each subformula and that way gradually minimize the whole boolean formula.

If the boolean formula has been simplified to the constant $\bot$, then it is unsatisfiable.

Otherwise it is satisfiable.

If subformula was simplified to $\bot$, then it is unsatisfiable and this implies that the whole given boolean formula is unsatisfiable too.

For instance:

Suppose that the algorithm found the following subformula contained in a boolean formula of 1000 boolean variables and 10000 clauses:

$(x \lor y \lor z) \land (\lnot x \lor y \lor z) \land (x \lor \lnot y \lor z) \land (\lnot x \lor \lnot y \lor z) \land (x \lor y \lor \lnot z) \land (\lnot x \lor y \lor \lnot z) \land (x \lor \lnot y \lor \lnot z) \land (\lnot x \lor \lnot y \lor \lnot z)$

Building karnaugh map for it and use it to minimize this subformula simplifies it to the constant $\bot$, thus the input boolean formula is unsatisfiable, and the complexity to do the last step was very good, because this boolean subformula contains only 3 different boolean variables, no matter that in the input boolean formula n=1000, and building karnaugh map for 3 boolean variables is fine! The size of the karnaugh map is only 23=8, not 2n=21000.

Also if the found subformula is:

$$(x\lor y\lor z)\land(x\lor y\lor\overline z)\land(x\lor\overline y\lor z)\land(x\lor\overline y\lor\overline z)\land(\overline x\lor y\lor z)\land(\overline x\lor y\lor\overline z)\land(\overline x\lor\overline y\lor t)\land(\overline x\lor\overline y\lor\overline t)$$

Building karnaugh map for it and use it to minimize this subformula simplifies it also to the constant $\bot$, thus the input boolean formula is unsatisfiable, and the complexity to do the last step is still good, although now it takes twice more resources than the previous subformula, because the subformula now has 4 boolean variables, rather than 3, but building karnaugh map for 4 boolean variables is not bad too! It only took 24=16 matrix cells rather than 2n=21000.

But iterating through subformulas and building karnaugh maps for them, is not in order to find one, that can be simplified to $\bot$, but the current subformula can be satisfiable, and cannot be simplified to $\bot$, but it's simplification can much help simplifying the whole input boolean formula a lot!

Suppose that the algorithm found the following boolean subformula:

$(x\lor y\lor z)\land(x\lor y\lor\overline z)\land(x\lor\overline y\lor z)\land(x\lor\overline y\lor\overline z)\land(\overline x\lor y\lor z)\land(\overline x\lor y\lor\overline z)$

Building karnaugh map for it, which costs 23=8 by the way because it has only 3 boolean variables, and then use it to minimize it, the subformula is not simplified to $\bot$, because it is satisfiable, but it does simplify to $x \land y$.

This is great! Now you know that the input boolean formula is satisfiable if and only if x=T and y=T, so if the algorithm tries to find satisfying assignment, then it needs to set both x and y to true and now you have eliminated 2 variables from the input, and now you remain n-2 boolean variables left, and all clauses that contain either x or y are satisfied and removed from the input boolean formula. Now the boolean formula is much simpler than before!

I didn't prove it, but I think that deterministic algorithm to simplify huge boolean formula with karnaugh maps gradually in steps, can solve the boolean satisfiability problem in polynomial time, but my conjecture has not been proved yet.

So my question is:

Does my conjecture correct?

How can it be either proved to disproved?

Improve this question
$\endgroup$
11
  • 1
    $\begingroup$ For making the Karnaugh map you need to know the values of the combinations of the variables and fill them up in the table. Now you can answer your question yourself. $\endgroup$
    – User Not Found
    Aug 4, 2017 at 9:21
  • 2
    $\begingroup$ Essentially, you're asking, "How would I prove this thing which, if true, would prove that $\mathrm{P=NP}$, thus resolving the greatest open question in computer science?" We don't know. That's much too much to ask in a Stack Exchange question. $\endgroup$
    – David Richerby
    Aug 4, 2017 at 9:30
  • 1
    $\begingroup$ The "arbitrary chosen" just gives a red flag. I think that some steps are hidding combinations and because of that look appealing and faster. Just as a reminder, extraordinary claim requires extraordinary proof, so it would be perfectly ok to simply assume: "it doesn't work". $\endgroup$
    – Evil
    Aug 4, 2017 at 9:47
  • 1
    $\begingroup$ That's what I thought too, but just wanted to make sure. I think and believe that the best algorithm to solve Boolean Satisfiability is the algorthm that uses karnaugh maps, and if it's super polynomial or exponential in the worst case, then this will imply that P!=NP. $\endgroup$
    – Farewell Stack Exchange
    Aug 4, 2017 at 10:20
  • 1
    $\begingroup$ I do think that if I succeed to write the karnaugh maps algorithm, even though it's complexity is still polynomial or exponential then at least I can go to the SAT competition and win a prize. Karnaugh maps algorithm can compete with existing sat solvers algorithms, like DPLL, Resolution and etc. There is also known probability and random algorithms and heuristics that help solve some NP instances faster. I add these algorithms and heuristics to the karnaugh maps algorithm in choosing the boolean subformula then the algorithm might be fast, even though it will be still superpolynomial in the $\endgroup$
    – Farewell Stack Exchange
    Aug 4, 2017 at 10:43

1 Answer 1

Reset to default
6
$\begingroup$

"arbitrary chosen" in a NP problem where the followup results in a P algorithm typically means that the choice matters a lot and trying them all and backtracking over bad choices looking for the result is what pushes the algorithm out of P.

In addition it is possible to create a subformula that you cannot simplify that way. For example a formula that is only true if exactly 1 out of n+1 variables is true. You cannot simplify that by only looking at n variables.

Which means that there are inputs that will not be solvable with that method.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ And what about 16 variables? You said 6, but is this possible with 16 variables then? $\endgroup$
    – Farewell Stack Exchange
    Aug 4, 2017 at 10:49
  • 1
    $\begingroup$ There also exists heuristic to choose the clauses, where in one clause there is some literal and it's negation on the other clause, so resolution inference rule can be applied to each pair of clauses in the boolean subformula, but the algorithm builds karnaugh map instead, because it's not recommended to use resolution, because it doesn't simplify the boolean formula, but in contrast it extends it and this is bad for the complexity of the algorithm, because resolution inference rule is only one way implication, but not equivalence unfortunately. $\endgroup$
    – Farewell Stack Exchange
    Aug 4, 2017 at 11:03
  • 3
    $\begingroup$ @ErezZrihen same issue with exactly 1 out of 17 variables while looking at only 16. $\endgroup$
    – ratchet freak
    Aug 4, 2017 at 11:08
  • 1
    $\begingroup$ Got it. Thank you for your answer. At least it can participates in the SAT competition with some improvements and heuristics, I think. $\endgroup$
    – Farewell Stack Exchange
    Aug 4, 2017 at 11:27

Your Answer

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

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