1. Homepage
  2. Programming
  3. ECE.650 Methods and Tools for Software Engineering - Programming Assignment 2: Tseitin's Transformation

ECE.650 Methods and Tools for Software Engineering - Programming Assignment 2: Tseitin's Transformation

Contact Us On WeChat
CanadaUniversity of WaterlooECE.650Methods and Tools for Software EngineeringTseitin's Transformation

ECE650 Programming Assignment 2: CourseNana.COM



The skeleton for this assignment is available at the master branch of 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 0 in CNF using Tseitin’s Transformation. CourseNana.COM

Your Program CourseNana.COM

For this assignment, you need to write a program that CourseNana.COM

  • Transform a Boolean formula F (first use your PA1 formula parser to parse a formula string input) into an equisatisfiable formula F 0 in CNF using Tseitin’s Transformation. The program is expected to output the satisfiability result of F by use of a SAT solver on F0.
  • 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;forexample,donotprintoutpromptstringssuchas“please enter input”andthingslikethat.
  • Write your code in C++.

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

Context-free Grammar for Valid Inputs CourseNana.COM

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

Formula ::= ConjTerm | ConjTerm +Formula
::= Term | Term *ConjTerm
::= 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.

Semantics of the Input CourseNana.COM

One valid input is a string representation of a Boolean formula SF in conformity with the aforementioned CFG. In SF , a Boolean variable is a sequence of letters (either in upper- or lowercase) or digits (0-9); however, the variable name cannot start with a digit and its total length cannot be longer than 10. ”+” represents the 2-argument infix Boolean function OR; ”” represents the 2-argument infix Boolean function AN D; ”” represents the prefix 1-argument Boolean function NOT . The order of operations is: parenthesis > NOT > AND > OR. CourseNana.COM

Tseitin’s Transformation CourseNana.COM

Similar to Boolean evaluator, Tseitin’s Transformation works recursively on the tree representation of a Boolean formula by traversing tree nodes. See in the course slide ”normal-forms-solver” for how to conduct Tseitin’s Trans- formation. The skeleton code stores the resulting CNF in the format of std::vector<std::vector<int>>: each inner vector represents a clause and each element in the inner vector is a literal; the outer vector represents the conjunction of clauses. This way of storing of CNF formulas is only a suggestion, not a requirement. We do not test on the intermediate results of CNF formulas; we only check the final satisfiability results. CourseNana.COM

Transformation Example 1 CourseNana.COM

Input SF : CNF F0: CourseNana.COM

1 represents variable v1 in this example. CourseNana.COM

Transformation Example 2 CourseNana.COM

Input SF : c+d  CNF F0 
[1, 2, 3][2, 1][3, 1][1] CourseNana.COM

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

Transformation Example 3 CourseNana.COM

Input SF : CNF F0: CourseNana.COM

2 represents variable b in this example. CourseNana.COM

[1, 2][1, 2][1] CourseNana.COM

Transformation Example 4 CourseNana.COM

Input SF : CNF F0: CourseNana.COM

, 4, 2][4, 3][2, 3][1, 2][1, 3][2, 3, 1][1] CourseNana.COM

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

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

SAT Solver CourseNana.COM

You need to use a SAT solver to check the satisfiablity of the transformed formula F0.
We will be using MiniSat SAT solver available at
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). CourseNana.COM

Initiate CourseNana.COM

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

Sample Run CourseNana.COM

The executable shall be called pa2. CourseNana.COM

$ ./pa2 a123 sat

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

(1+2+3)*(1+2+ -3)*(1+ -2 +3)*-1 Error: invalid input CourseNana.COM

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

Unit Test CourseNana.COM

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

Error Handling CourseNana.COM

You program should be able to identify invalid inputs according to the CFG and print an error message starting with “Error:”. CourseNana.COM

Marking CourseNana.COM

Your output has to perfectly match what is expected. You should also follow the submission instructions carefully. It discusses how to name your files, how to submit, etc. The reason is that our marking is automated. CourseNana.COM

• Does not compile/make/crashes: automatic 0
• Your program runs, awaits input and does not crash on input: + 20 • Passes Test Case 1: + 20
• Passes Test Case 2: + 20
• Passes Test Case 3: + 15
• Passes Test Case 3: + 10
• Correctly detects errors: + 10
• Programming style: + 5

CMake CourseNana.COM

As discussed below under “Submission Instructions”, you should use a CMakeLists.txt file to build your project. We will build your project using the following sequence: CourseNana.COM

cd pa2 && mkdir build && cd build && cmake ../ CourseNana.COM

If your code is not compiled from scratch (i.e., from the C++ sources), you get an automatic 0. CourseNana.COM

Get Expert Help On This Assignment

Scan above qrcode with Wechat

Canada代写,University of Waterloo代写,ECE.650代写,Methods and Tools for Software Engineering代写,Tseitin's Transformation代写,Canada代编,University of Waterloo代编,ECE.650代编,Methods and Tools for Software Engineering代编,Tseitin's Transformation代编,Canada代考,University of Waterloo代考,ECE.650代考,Methods and Tools for Software Engineering代考,Tseitin's Transformation代考,Canadahelp,University of Waterloohelp,ECE.650help,Methods and Tools for Software Engineeringhelp,Tseitin's Transformationhelp,Canada作业代写,University of Waterloo作业代写,ECE.650作业代写,Methods and Tools for Software Engineering作业代写,Tseitin's Transformation作业代写,Canada编程代写,University of Waterloo编程代写,ECE.650编程代写,Methods and Tools for Software Engineering编程代写,Tseitin's Transformation编程代写,Canadaprogramming help,University of Waterlooprogramming help,ECE.650programming help,Methods and Tools for Software Engineeringprogramming help,Tseitin's Transformationprogramming help,Canadaassignment help,University of Waterlooassignment help,ECE.650assignment help,Methods and Tools for Software Engineeringassignment help,Tseitin's Transformationassignment help,Canadasolution,University of Waterloosolution,ECE.650solution,Methods and Tools for Software Engineeringsolution,Tseitin's Transformationsolution,