<script type="application/ld+json">

{

"@context": "https://schema.org",

"@type": "FAQPage",

"mainEntity": {

"@type": "Question",

"name": "What is the boolean satisfiability problem?",

"acceptedAnswer": {

"@type": "Answer",

"text": "In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula."

}

}

}

</script>

Table of contents

Key takeawaysCollaboration platforms are essential to the new way of workingEmployees prefer engati over emailEmployees play a growing part in software purchasing decisionsThe future of work is collaborativeMethodologyIn logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula.

In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable.

In order to ensure that we are able to satisfy any formula first we need to have the necessary operators to represent it. For that purpose, we can use 0 and 1 values to represent False and True values respectively. As it is explained by George Boole in 1847, we can use three intuitive operators where:

- x and y = min(x, y)
- x or y = max(x, y)
- not x = 1- x

To make things easier, we’ll use a new operator to replace the or and not; Choice, and when you type (x | y | z) = 1 means you can choose which x, y or z is 1, but only one and exactly one. In fact, you could type (x | y) = 1, which means x = 1 - y = not y.

Considering the · operator A·B = A and B, now we are prepared to show beautiful formulas…

And…, [(x1 | … | xn) = 1] ↔ [x1 + … + xn = 1]. Later, we will use another notation, but now let’s study what can we do with this operator.

Proposition. Having the next equation (A|B|C)·(B|D|E)·(C|E|F)=1, where A, B, …, F are Boolean variables, the following statements are fulfilled:

B = not A and not D

F = A ↔ D

So we can construct the next theorem: for every x, y Boolean values:

(not x | x and y | z1)·(x and y | not y | z2)·(z1 | z2 | x ↔ y) = 1

So, as corollary: we can represent every Boolean formula as a conjunction (·) of choices of Boolean variables.

You can consider some other studies about how different problems (interesting for the Computer Science) could be represented.

Share