SAT solver based on tableaux method

• Install
• Manual
• Examples

Following part contains basic definitions for those unfamiliar with the tableaux method.

A tableau is a labeled binary tree. The nodes of this tree are called entries. Each entry is labeled with a signed propositions (i.e. proposition preceded by either a T or an F).

A tableau proof of a proposition A is a contradictory tableau with root entry F(A). A tableau refutation for a proposition A is a contradictory tableau with root entry T(A)

Entry E has been reduced on P if all the entries on one path through the atomic tableau with root E occur on P.

Atomic tableaux:

A tableau can be constructed inductively:

1. Every atomic tableau is a tableau
2. If T is a tableau and E is an entry of T of maximal depth such that there is a noncontradictory path P of T on which E is unreduced, then if T' is the tableau gotten by adjoining the unique atomic tableau with root E to the end of every noncontradictory path P' of T on which E is unreduced, then T' is a tableau.

Reference:

Nerode, A., & Shore, R. A. (1997). Logic for applications. New York: Springer.

To compile the sources a makefile, which is present in the repository, can be used. The executable will be placed in a build directory: build/tableaux-sat

tableaux-sat [-Tdp] [--dot] [--proof]

Input format: a formula must consist of valid connectives and propositional letters. a propositional letter can contain alphanumeric characters. Letters and proposition can be separated by spaces (they will be removed).

Program will output the satisfiability (SATISFIABLE or UNSATISFIABLE) on the first line and a model (if it exists).If the formula is satisfiable the next lines contain the model in following format

<propositional_letter> = <0 or 1>

If some of the propositional letters in the formula is not present in the output, it means that its value is independent. The leftmost non-contradictory branch of the tableau is taken as a model.

See an example

Theory mode is enabled by option -T.

Input format: Each formula is on separate line. The first line contains a formula to prove in the theory. Following line contain axioms of the theory. These axioms will be signed with T. The output is in the same format as in the first part.

See an example

The program will output the tableau in the dot language format when -d or --dot options are set. The output can be used with a program such as graphviz to generate an image.

Contradictory branches are marked with an astersisk *.

See an example

Proof mode can be set with options -p or --proof. In proof mode the root entry will be signed with F.

See an example

Priority can be modified using parantheses (, ).

All examples can be executed by running demo.sh.

$ tableaux-sat
p & ~p

UNSATISFIABLE

$ tableaux-sat -T
s
q - p
r - q
(r - p) - s

SATISFIABLE
q = 0
r = 0
s = 1

$ tableaux-sat -T --dot
p
~q
p | q

graph tableau {
        node[shape="plaintext", fontname="courier"]
        nodesep=0.4
        ranksep=0.5

        E1[label="T(p) "]
        E1 -- E2

        E2[label="T(~q) "]
        E2 -- E3

        E3[label="T(p|q) "]
        E3 -- E4

        E4[label="F(q) "]
        E4 -- E5
        //hidden node to balance the tree
        E4hidden [label="", width=.1, style=invis]
        {rank=same;E4hidden; E5; E6}
        E4 -- E4hidden[style=invis]
        E4 -- E6

        E6[label="T(q)*"]

        E5[label="T(p) "]
}

Image generated from the output by graphviz:

Note that nodes on contradictory branches are marked by an asterisk.

$ tableaux-sat --proof
~(p | q) = (~p & ~q)

PROVABLE

Tableau from example 2:

Tableau from example 4:

© Peter Grajcar