# ### Site Tools

plt17:assignment_1

# SAT Solver in Scala

## Introduction

The first goal of this assignment is to make you comfortable in functional programming with Scala. During the assignment you will get familiar with satisfiability solvers which are used as back-end engines for several other verifiers. Your task is to implement different algorithms for a SAT solver and to compare their performance against each other.

## Scala IDE

The choice of programming environment is entirely up to you. We recommend using the Scala IDE for Eclipse (http://scala-ide.org/). You may choose to use other frameworks such as IntelliJ IDEA or use your favorite text editor and run the compiler from the command-line.

The standard way to represent a Boolean formula in conjunctive normal form is the DIMACS format. The format is used as input to modern SAT-solvers. A file in the DIMACS format begins with a line specifying that the formula is in normal form, the number of variables in the formula, and how many clauses it contains. For example, p cnf 4 3 specifies that the file contains a formula in conjunctive normal form with 4 variables and 3 clauses. Then, the next lines describe the clauses, one on each line. Each line contains a list of positive or negative integers, and ends with a zero. A positive integer $i$ indicates that the $i^{\text{th}}$ variable appears in the clause, whereas a negative integer $-i$ indicates that the negation of the $i^{\text{th}}$ variable appears in the clause. For example, here's a formula, followed by its encoding using the DIMACS format:

$(x_1\vee x_3\vee \overline{x_4}) \wedge (x_4) \wedge (x_2 \vee \overline{x_3})$

c
c
p cnf 4 3
1  3  -4  0
4  0
2  -3  0

Write a function that takes three parameters (number of variables, number of clauses, filename) and makes a random Boolean formula for the given parameters. The function writes the result formula in DIMACS format into the given filename.

Write a function that gets a DIMACS benchmark file and uses the truth table algorithm to solve it. You can return a Boolean value from the function to show the satisfiability of the given input, or, display the result on the standard output. You may assume that the input file is a correct DIMACS benchmark for a CNF formula, you do not need to check the input file.

Write a function that gets a DIMACS benchmark file and uses a concurrent version of the truth table algorithm to solve it. A powerful and easy way to write concurrent programs in Scala is to use the Akka actor library. Alternatively you can use Scala Futures that provides a simple way to run an algorithm concurrently. Write an actor that takes a boolean formula and checks a subset of rows in its truth table. Spawn multiple instances of that actor to cover all the rows. For example, for a Boolean formula with 4 variables, there are $2^4=16$ rows in the truth table. You can use one actor to check 8 rows and another for the rest of 8 rows. Or, you can use 4 actors that each of them checks 4 rows of the truth table. The actor gets a parameter (in the message) to know which subset of the table it should check. The function in this task should also take an argument to know how many actors it should spawn to check the Boolean formula. The function should assert that the given number is only a power of 2. You can return a Boolean value from the function to show the satisfiability of the given input, or, display the result on the standard output. You may assume that the input file is a correct DIMACS benchmark for a CNF formula, you do not need to check the input file.

Write a function that gets a DIMACS benchmark file and uses the DPLL algorithm (as described in Lecture 5) to solve it. You can e.g. return a Boolean value from the function to show the satisfiability of the given input, or, display the result on the standard output. You may assume that the input file is a correct DIMACS benchmark for a CNF formula, you do not need to check the input file.

You are now able to compare the different versions of the your SAT solvers. To have a comparison with a real SAT solver that runs on Java, your comparison will also include the Sat4j solver. First make a good library of benchmarks using the function of the first task. The sizes of the benchmarks should be large enough to challenge your SAT solver, try to avoid creating tiny hello-world examples that can be solved in milliseconds. The smallest benchmark should take the truth-table solver several seconds to solve. Try to generate at least 50 different benchmarks with different sizes. Record the elapsed time for the truth-table solver, parallel truth-table solver (with 2, 4 and 8 actors), your DPLL solver and finally Sat4j. To ensure that your SAT solvers are correct, you need also to check their results against the output of Sat4j. Draw a plot to compare the results. The y-axis of the plot is the elapsed time. The x-axis is the size of the benchmark. If you have several benchmarks with the same time, you may want to put the average elapsed time for a solver. There will be totally 6 lines in the plot to show how the solvers compare to each other. Write a report (at least one page) to justify the results of your experiments. In your report include some of your suggestions to improve the performance of your SAT solvers.

• You are not allowed to use mutable variables in this assignment. If you choose to define mutable variables using e.g. var your grade will be significantly reduced. 