OKlibrary  0.2.1.6
Tutorial.hpp File Reference

Tutorial on SAT in Maxima/Lisp by MH. More...

Go to the source code of this file.

## Detailed Description

Tutorial on SAT in Maxima/Lisp by MH.

# SAT via Maxima in the OKlibrary

## From variables to clause-sets

1. A "boolean variable" can be any expression x, such that
• "x" is positive (i.e., `is(x > 0)` yields true);
• "- x" is negative;
• `--x = x`.
2. A literal is either a variable or the negation of a variable. To obtain the underlying variable of a literal l, the function var_l(l) is provided.
```oklib_load_all();

(%i12) var_l(-1);
(%o12)                                 1
```
3. For a set S of variables, by literals_v(S) we compute the set of all literals with underlying variable in S.
```(%i13) literals_v({1,2,3});
(%o13)                     {- 3, - 2, - 1, 1, 2, 3}
```
4. A "boolean clause" is a set C of boolean literals such that C and the complement of C, comp_sl(C), have empty intersection.
```(%i14) C1:{1,-2};
(%o14)                             {- 2, 1}
(%i15) intersect(C1,comp_sl(C1));
(%o15)                                {}
```
5. A "boolean clause-set" is a set of boolean clauses.
```(%i16) C2:{-1,3}\$
(%i17) C3:{2,3,-4}\$
(%i18) F:{C1,C2,C3};
(%o18)                   {{-4, 2, 3}, {- 2, 1}, {- 1, 3}}
```
6. The variables of a clause-set can be obtained by the var_cs function:
```(%i19) var_cs(F);
(%o19)                             {1, 2, 3, 4}
```
7. The number of variables of a clause-set can be obtained by the nvar_cs function.
```(%i20) nvar_cs(F);
(%o20)                                 4
```
8. The number of clauses of a clause-set is given by the ncl_cs function.
```(%i21) ncl_cs(F);
(%o21)                                 3
```
9. The number of literal occurences in a clause-set is given by the nlitocc_cs function.
```(%i22) nlitocc_cs(F);
(%o22)                                 7
```
10. A "formal boolean clause-set" is a pair [V, F], where V is a set of variables, while F is a clause-set using only variables from V. The function cs2fcs(F) returns the formal clause-set of a clause-set F.
```(%i23) FF:cs2fcs(F);
(%o23)             [{1, 2, 3}, {{-4, 2, 3}, {- 2, 1}, {- 1, 3}}]
```
11. The variables of a formal clause-set can be obtained by the var_fcs function.
```(%i24) var_fcs(FF);
(%o24)                             {1, 2, 3, 4}
```
Note that the point of "formal clause-sets" is to allow that variables might not occur in the clause-set.
12. The number of variables of a formal clause set is given by the nvar_fcs function.
```(%i25) nvar_fcs(FF);
(%o25)                                 4
```
13. The number of clauses of a formal clause set is given by the ncl_fcs function.
```(%i26) ncl_fcs(FF);
(%o26)                                 3
```
14. A formal clause-set can be printed in Dimacs format using the print_fcs function. The first argument is a comment.
```(%i27) print_fcs("Sample boolean clause set #001",FF)\$
c Sample boolean clause set #001
p cnf 3 3
-4 2 3 0
-2 1 0
-1 3 0
```
15. For output to a file, use the output_fcs function. By default, the file is located in the directory where you started Maxima.
```(%i28) output_fcs("Sample boolean clause set #001",FF,"001.cnf")\$
```

## SAT problems

1. The pigeonhole principle for 2 pigeons in 2 pigeonholes. Here the variable php(i,j) (note the usage of function "php" for variables) means that pigeon i is in pigeonhole j and -php(i,j) means that pigeon i is not in pigeonhole j.
```(%i29)  php22:weak_php_fcs(2,2);
(%o29) [{php(1, 1), php(1, 2), php(2, 1), php(2, 2)},
{{- php(1, 1), - php(2, 1)}, {php(1, 1), php(1, 2)},
{- php(1, 2), - php(2, 2)}, {php(2, 1), php(2, 2)}}]
```
2. To solve a pigeonhole principle problem, one possibility is to use the various DLL solvers available in the Backtracking module. The simplest of these has input a formal clause-set and returns either true or false.
```(%i30) dll_simplest_first_shortest_clause(php22);
(%o30)                                true
```
3. For each DLL solver there is also a version which returns the splitting tree:
```(%i31) split_tree:dll_simplest_st_first_shortest_clause(php22);
(%o31) [php(1, 1), [- php(1, 2), [php(2, 2), [- php(2, 1), [true], [false]],
[false]], [false]], [php(2, 1), [- php(2, 2), [php(1, 2), [true], [false]],
[false]], [false]]]
```
4. From a splitting tree the satisfying assignments can be extracted using the sat_pass_st() function:
```(%i32) sat_pass_st(split_tree);
(%o32) [{- php(1, 1), php(1, 2), php(2, 1), - php(2, 2)},
{php(1, 1), - php(1, 2), - php(2, 1), php(2, 2)}]
```
5. For output, we can create a splitting tree diagram in PStree format (the file "tree.tex" is placed in the directory from where you started Maxima).
```(%i33) tex_st_f("tree.tex", split_tree)\$
```

## Special generators

1. vanderwaerden2_fcs(k,n) is the Boolean clause-set whose solutions are the partitionings of {1,...,n} into two parts such that none of them contains an arithmetic progression of size k.
```(%i34) vdw38:vanderwaerden2_fcs(3,8);
(%o34) [{1, 2, 3, 4, 5, 6, 7, 8}, {{- 8, - 7, - 6}, {- 8, - 6, - 4},
{- 8, - 5, - 2}, {- 7, - 6, - 5}, {- 7, - 5, - 3}, {- 7, - 4, - 1},
{- 6, - 5, - 4}, {- 6, - 4, - 2}, {- 5, - 4, - 3}, {- 5, - 3, - 1},
{- 4, - 3, - 2}, {- 3, - 2, - 1}, {1, 2, 3}, {1, 3, 5}, {1, 4, 7}, {2, 3, 4},
{2, 4, 6}, {2, 5, 8}, {3, 4, 5}, {3, 5, 7}, {4, 5, 6}, {4, 6, 8}, {5, 6, 7},
{6, 7, 8}}]
(%i35) dll_simplest_first_shortest_clause(vdw38);
(%o35)                               true
(%i36) vdw39:vanderwaerden2_fcs(3,9);
(%o36) [{1, 2, 3, 4, 5, 6, 7, 8, 9}, {{- 9, - 8, - 7}, {- 9, - 7, - 5},
{- 9, - 6, - 3}, {- 9, - 5, - 1}, {- 8, - 7, - 6}, {- 8, - 6, - 4},
{- 8, - 5, - 2}, {- 7, - 6, - 5}, {- 7, - 5, - 3}, {- 7, - 4, - 1},
{- 6, - 5, - 4}, {- 6, - 4, - 2}, {- 5, - 4, - 3}, {- 5, - 3, - 1},
{- 4, - 3, - 2}, {- 3, - 2, - 1}, {1, 2, 3}, {1, 3, 5}, {1, 4, 7}, {1, 5, 9},
{2, 3, 4}, {2, 4, 6}, {2, 5, 8}, {3, 4, 5}, {3, 5, 7}, {3, 6, 9}, {4, 5, 6},
{4, 6, 8}, {5, 6, 7}, {5, 7, 9}, {6, 7, 8}, {7, 8, 9}}]
(%i37) dll_simplest_first_shortest_clause(vdw39);
(%o37)                               false
```

Definition in file Tutorial.hpp.