7.3 - λ-calculus and Computability

This assignment focuses on conjunctive normal form formulas (cnf-formula) and satisfiability.

Functional requirements

In this assignment, you must create a Netbeans Java program that:

• prompts the user for the location of a file to load a cnf-formula (use JFileChooser)


• reads a CNF formula from the file to create a CnfFormula object (see file-format below),


• prompt the user for a variable assignment (see AssignmentView below),


• run the methodverify()toverify and display whether the user’s assignment satisfies the cnf-formula,


• determines whether the cnf-formula is satisfiable and if so, outputs the valid variable assignments

Non-functional requirements

• as Java comments give the Big-O analysis of theverify()andisSatisfiable()methods,


• as a separate file, submit the cnf-formula file you “unit” tested on.

Input File Format

Consider thecnf-formula,

Thiscnf-formulais represented as one line in the input file,

(x1 v x3 v x4) ^ (nx1 v x3) ^ (nx1 v x4 v nx2) ^ nx3 ^ (x2 v nx4)

The general format of this cnf-formula in the input file is:

clause₁^clause₂^...^clause_n

Where each clause in the cnf-formula is separated by a caret ‘^’ character. A clause is either a literal or a disjunction of literals surrounded by where a letter ‘v’ is used to separate multiple literals.

litteral₁^litteral₂^...^litteral_n

A literal is either a variable name or a negated variable, in which case the variable name is preceded by the letter ‘n’ (Naturally, the symbols "n" and "v" cannot be used in a variable name.)

Class diagram

Minimally, your program must implement the following UML class diagram (notes follow).

SatNpApp

• 
  verify(Assignment)– utility method that sends a verify message to a CnfFormula


• 
  isSatisfied()– utility method that finds an assignment, if any, that satisfies the current CnfFormula

Other classes

• 
  getListOfVariables()– returns the list of the variables used in the corresponding object (CNF Formula or Clause)


• 
  verify(Assignment)– returns true, if the truth-value assignments for the variables inAssignmentsatisfy this formula/clause/literal

You will notice that the class Literal is defined as a subclass of Variable. Indeed, a literal is simple a variable that can be negated or not. A variable, in our case, is a very simple class because it only contains a name field.

Note also that we should have added an arrow from CnfFormula, Clause and Literal to Assignment but we didn't for the sake of clarity.

UI for Assignments

To get the user choices for the truth-value assignments to the variables, you need some kind of UI using the GUI or the console, for example using an AssignmentView class. There are several ways of achieving that - you are free to implement it the way you like. If you want,an example of AssignmentView class is givenhere. It can be used to easily assign the truth values for an assignment. It is implemented using the model, view, controller design pattern in which an Assignment object is the model. You will also needGPanel.java.

Example of Main() method

Here’s one way to implement the main(…) method in the SatNpApp:

view = new AssignmentView();






File file = chooseExprLocation();







try{



CnfFormula formula = loadCnfFormula(file);







do{



Assignment assignment = new Assignment(formula);







view.setModel(assignment);



view.setVisible(true);







if(formula.verify(assignment)) {



JOptionPane.showMessageDialog(null, "Satisfied");



}else{



JOptionPane.showMessageDialog(null, "Not Satisfied");



}







isSatisfiable(formula);







}while(trueFalsePrompt("Test another input string?"));

Submission

This is an individual assignment. If you have questions email the faculty (don’t post in the forum).

Submit your NetBeans project and example DFA input file to the Topic 9 drop box folder in the online course shell for this course section in Worldclass.Don't forget the Big-O analysis.

Rubrics