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 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.