Java assignment help

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

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 creating a CnfFormula object (see file-format below),

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

• verifies and displays whether the user’s assignment satisfies the cnf-formula,

• determines whether the cnf-formula is satisfiable and if so, output the assignment,

• as Java comments give the Big-O analysis of the verify and isSatisfiable methods,

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

Input File Format

Consider the cnf-formula,

(𝑥1 ∨ 𝑥3 ∨ 𝑥4) ∧ (�̅�1 ∨ 𝑥3) ∧ (�̅�1 ∨ 𝑥4 ∨ �̅�2) ∧ �̅�3 ∧ (𝑥2 ∨ �̅�4)

This cnf-formula is 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:

𝑐𝑙𝑎𝑢𝑠𝑒1 ^ 𝑐𝑙𝑎𝑢𝑠𝑒2^ … ^𝑐𝑙𝑎𝑢𝑠𝑒𝑛

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.

𝑙𝑖𝑡𝑒𝑟𝑎𝑙1 v 𝑙𝑖𝑡𝑒𝑟𝑎𝑙2 v … v 𝑙𝑖𝑡𝑒𝑟𝑎𝑙𝑛

A literal is either a variable name or a negated variable, in which case the variable name is

preceded by the letter ‘n’ (Naturally, n’s and v’s cannot be used in a variable name.)

Class Diagram

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

CnfFormula and Clause

• literals() – return the variable names (i.e. literals) used in this formula/clause

• verify(Assignment) – return true, if the truth assignments for the variables in the

Assignment satisfy this formula/clause

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

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 (expr.verify(assignment)) {

JOptionPane.showMessageDialog(null, "Satisfied");

} else {

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

}

isSatisfiable(formula);

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

AssignmentView

The AssignmentView class is given in the online shell for this Topic. 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.

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.

Assignment Exemplary Advanced Proficient Not Demonstrated

or Major Issues

Cnf Formula

Definition

All classes and methods

appropriately defined

25

I/O Program Input and Output

appropriately defined

15

General design

Java Constructs

Appropriate design for the

problem

Java constructs appropriately

used

20 – 16 15

Execution and Program executes correctly for

all Cnf-Formula test cases

Program executes correctly for

most Cnf-Formula test cases

Program executes correctly

for an appropriately tested

user Cnf-Formula

30 – 21 20 – 16 15

Analysis Correct Big-Oh Analysis Reasonable Big-Oh analysis

10 – 6 5 – 1

Deductions Submitted on time

Appropriately commented

Executes using NetBeans

Inappropriate comments 1-10%

Compiles correctly

3% deducted per day late Not submitted within

five days of due date

or does not compile