How to convert/formalize a series of logical expressions into a format that can be given to a DPLL algorithm?

Question

Take the following set of logical statements:

A: B is false

B: C is false

C: B or A is true

I as given the task to formalize this so that a "DPLL" could determine if there is a solution (which rules are true, which are false) that does not lead to a contradiction.

The problem is: I have no idea how to do this. Online solvers expect expressions in a certain format, like this one here: http://www.inf.ufpr.br/dpasqualin/d3-dpll/

How do i transform my statements into these numbers?

Answer 1

You may be confusing the notation here: I'm assuming that there are three statements and three variables here. I will use lower case letters for the variable and upper case letters for the statements to make this clear:

Statement A: not b
Statement B: not c
Statement C: a or b

Now replace the lower case letters with numbers:

Statement A: not 2
Statement B: not 3
Statement C: 1 or 2

The not should be written as negative sign and the or is replaced by a colon. The resulting three lines can now be entered in the SAT-solver you linked:

-2
-3
1, 2

It outputs 1, -2, -3 as solution, so variable a had to be true while b and c had to be false.