Boolean Formula and Satisfiability

A Quick Introduction to Boolean Logic

The simplest possible Boolean formula contains a single variable.  

1: p

Here p can be either true or false.  When p is true the entire formula is true.  When p is false the formula is false.

Additionally we can negate a variable appearing in a formula.

2: ~p

When p is true ~p is false and vise versa.

From now on we will call a variable appearing in a formula a literal and a negated variable a negative literal.  For example we would say that formula 1 contains a single literal and formula 2 contains a single negative literal.

To build a formula with more than one literal we need some operators.  Boolean formulas have two operators commonly called and and or.  Below I will use the characters & and V for these when writing out formulas.

3: p&q

3 is true only when both p is true and q is true.

4: pVq

4 is true when p is true or q (or both) is true.

We can add parenthesis to a formula having the same effect as parentheses in high school maths.

5: r&(pVq)

5 is true when r is true and either p or q are true. 

Satisfiability

A formula is satisfiable if it is possible to give its variables values which make the entire formula true.

6: p

6 is definitely satisfiable because when we make p true the entire formula is true.

7: ~p

7 is also satisfiable because we can make p false and the formula true.

8: ~pVp

8 is satisfiable, in fact no matter what value we give to p this formula will be true.

9: ~p&p

9 is not satisfiable because there is no way to make p and ~p true at the same time.

Conjunctive Normal Form

A formula is said to be in conjunctive normal form (CNF) it looks like this.

6: (aV~bVc) & (~aVb) & (aVdV~cV~e) & (c) & (cVeV~f)

Each literal is connected by the V operator in a row we will call a clause.  For example the first clause in 6 is (aV~bVc).  Each clause is connected to another clause by the & operator.  For every Boolean formula there is an equivalent (equally satisfiable) formula in CNF.

A formula in CNF is satisfiable if at least one literal from each clause can be made true.

An Easy Problem

Writing a computer program to determine whether or not a Boolean formula is satisfiable is very straight forward.  We can clearly try every possible combination of true and false for every variable in the formula asking at each step whether or not the formula is satisfiable.  Unfortunately if we have n variables there are 2^n possible combinations and we quickly run out of time left in the universe for solving our problem.

Cleverer algorithms have managed to determine satisfiability in times much faster than 2^n, and adding processing power by distributing the computation is a fun next step.