The skeleton for this assignment is available at the master branch of https://git.uwaterloo.ca/ECE650-F2022/ skeleton in directory pa2. Follow the instructions in Assignment 0 to correctly fetch and merge the files from

the skeleton!

This is the second in a series of assignments that is part of a single large project. The project is to build a SAT solver, and the purpose of this assignment is transform a Boolean formula F into an equisatisfiable formula F^′ in CNF using Tseitin’s Transformation.

Your Program

For this assignment, you need to write a program that

• Transform a Boolean formula F (first use your PA1 formula parser to parse a formula string input) into an equisatisfiable formula F^′ in CNF using Tseitin’s Transformation. The program is expected to output the satisfiability result of F by use of a SAT solver on F^′.

• Continuously take input from standard input,  and output to standard output.  Errors shall also be output   to standard output, but should always start with “Error:” followed by a brief description. Your program should terminate gracefully (and quietly) once it sees EOF. Your program should not generate any extraneous output; for example, do not print out prompt strings such as “please enter input” and things like that.

• Write your code in C++.

• Ensure that it compiles with the C++ compilor on

eceubuntu.uwaterloo.ca and runs on eceubuntu.uwaterloo.ca. (Use eceterm.uwaterloo.ca to log-in from off-campus; then follow the instructions to connect to eceubuntu.)

• You can modify the skeleton as you wish, but you may only #include the following libraries (and no others!) for the current assignment: iostream, fstream, sstream, iomanip, string, utility, exception, regex, algorithm, cctype, cstring, vector, stack, list, deque, and map.

Context-free Grammar for Valid Inputs

One valid input formula shall be a string generated from the Context-Free Grammar below:

Formula ::= ConjTerm | ConjTerm ’+’ Formula ConjTerm ::= Term | Term ’*’ ConjTerm

Term ::= VarName | ’-’Term | ’(’ Formula ’)’

VarName ::= a continuous sequence of letter (upper- or lowercase) or digits (0-9); the first character cannot be a digit; the total length shall be no longer than 10

* Blue represents non-terminals and red represents terminals.

* Arbitrary amounts of whitespace are permitted before, after, or in between any of these terms.

CNF F^′:

Comments:

1 represents variable v1 in this example.

Transformation Example 2

Input S_F :

CNF F^′:

(v1)

[1]

c + d

Comments:

[−1, 2, 3][−2, 1][−3, 1][1]

2 represents variable c and 3 represents variable d in this example.

Transformation Example 3

Input S_F :

CNF F^′:

Comments:

2 represents variable b in this example.

−b

[−1, −2][1, 2][1]

Transformation Example 4

Input S_F :

CNF F^′:

c ∗ (d + c)

Comments:

[−3, 4, 2][−4, 3][−2, 3][−1, 2][−1, 3][−2, −3, 1][1]

4 represents variable d and 2 represents variable c in this example.

* See provided executable sample-helper-tseitin for more examples.

SAT Solver

You need to use a SAT solver to check the satisfiablity of the transformed formula F^′.

We will be using MiniSat SAT solver available at https://github.com/agurfinkel/minisat MiniSat provides a CMake build system.  The build process creates an executable minisat and a  library

libminisat.a.  You will need to link against the library in your assignment (you can refer to the provided

CMakeLists.txt).

Sample files are available in https://git.uwaterloo.ca/ece650-f2022/skeleton/-/tree/ master/sample-code/minisat-example

Sample Run

The executable shall be called pa2.

$ ./pa2 a123

sat a+c sat

a* -- -a unsat

(( -a)+(a*b)) * Error: invalid input

(1+2+3)*(1+2+ -3)*(1+ -2 +3)*-1

Error: invalid input

You can see test cases in test\test0.in and expected outputs in test\test0.out for more examples. Also, you can play with the provided sample executable sample-pa2 on eceubuntu.

Unit Test

doctest is a single-header testing framework. We have provided the doctest header file, a sample test.cpp file of unit testing using doctest, and guidance on compiling the test executable in CMakeLists.txt. This unit test framework is just for your assistance and not a requirement.