Part 1:

1. Define a class called Main

2. This class expects an input file name to be provided thro the command line argument; if the file is not provided then the program exits with an error message. You need to know how to provide a command line argument in Eclipse IDE.

3. Assume the existence of classes called DPSolver and Timer.

4. Main will contain only the main function, which should

a) pass the input file to a DPSolver object.

b) Start the system clock using the start() in Timer.

c) Use the solve() in DPSolver to solve the sat problem in the input file.

d) Stop the system clock using the stop() in Timer.

e) Print out the time taken to solve the problem

5. Write the Timer class with three methods: start(), stop() and getDuration().

Part 2:

1. Write a class called FormulaReader

2. This class defines a method called read() that reads the formula from the and stores it in a 2D array called formula each clause in the input file is to be stored in one row of the 2D array. In the input file,

a) Skip all the lines in the input file until p cnf. Use the pattern class to implement this step.

b) Read and save the number of variables and clauses.

c) Read and save the formula.

3. Define get methods for the number of variables, number of clauses and the formula.

Implementation of a SAT Solver In Java using Backtracking Develop a solver for the Satisfiability problem using backtracking Preliminaries Let's begin with some definitions. (Don't get psyched by the formality; you're familiar with most of this already!) This project deals with Boolean formulae. A Boolean formula is comprised of Boolean variables, the negation operator (Boolean not), th conjunction operator (Boolean and). We use x1, x2, etc., to denote Boolean variabl Definition of literal A literal is a Boolean variable or the negation of a Boolean variable Definition of clause A clause is a disjunction (or) of literals, or a single literal Definition of formula in conjunctive normal fornm A formula is a conjunction (and) of clauses, or a single clause. r not-x4). This formula is comprised of Boolean variables x1, x2, x3 and x4, and has three clauses Definition of assignment An assignment for a formula is a setting of truth values (either true or false) for the variables in the formula. An example assignment for the example formula given above is: x1, x2 and x4 are set to true and x3 is set to false. We will write this assignment as (x1, x2, x3, x4) - (true, true, false, true) Definition of satisfving assignment for a formula An assignment that makes a formula evaluate to true is a satisfying assignment. Observe that the assignment (x1, x2, x3, x4) = (true, true, false, true) makes each clause in the example formula evaluate to true, and thus makes the example formula evaluate to true and is a satisfying assignment On the other hand, the assignment (x1, x2, x3, x4) = (false, false, true, true) makes the above formula evaluate to false since it does not satisfy the formula's first clause, and therefore it is not a satisfying assignment. Definition of partial assigument for a formula A partial assignment is a setting of truth values for 0 or more variables in a formula. A partial assignment for the example formula given above is: x1 and x4 are set to true, and x3 is set to false. We will write this satisfying partial assignment as (x1, x2, x3, x4) = (true, false, true). Definition of satisfiable formula A Boolean formula is satisfiable when it has a satisfying assignment. Definition of the Satisfiability Problem (SAT Given a Boolean formula, determine whether or not it is satisfiable. This material is based upon work supported by the National Science Foundation under Grant No. 1140753 Implementation of a SAT Solver In Java using Backtracking Develop a solver for the Satisfiability problem using backtracking Preliminaries Let's begin with some definitions. (Don't get psyched by the formality; you're familiar with most of this already!) This project deals with Boolean formulae. A Boolean formula is comprised of Boolean variables, the negation operator (Boolean not), th conjunction operator (Boolean and). We use x1, x2, etc., to denote Boolean variabl Definition of literal A literal is a Boolean variable or the negation of a Boolean variable Definition of clause A clause is a disjunction (or) of literals, or a single literal Definition of formula in conjunctive normal fornm A formula is a conjunction (and) of clauses, or a single clause. r not-x4). This formula is comprised of Boolean variables x1, x2, x3 and x4, and has three clauses Definition of assignment An assignment for a formula is a setting of truth values (either true or false) for the variables in the formula. An example assignment for the example formula given above is: x1, x2 and x4 are set to true and x3 is set to false. We will write this assignment as (x1, x2, x3, x4) - (true, true, false, true) Definition of satisfving assignment for a formula An assignment that makes a formula evaluate to true is a satisfying assignment. Observe that the assignment (x1, x2, x3, x4) = (true, true, false, true) makes each clause in the example formula evaluate to true, and thus makes the example formula evaluate to true and is a satisfying assignment On the other hand, the assignment (x1, x2, x3, x4) = (false, false, true, true) makes the above formula evaluate to false since it does not satisfy the formula's first clause, and therefore it is not a satisfying assignment. Definition of partial assigument for a formula A partial assignment is a setting of truth values for 0 or more variables in a formula. A partial assignment for the example formula given above is: x1 and x4 are set to true, and x3 is set to false. We will write this satisfying partial assignment as (x1, x2, x3, x4) = (true, false, true). Definition of satisfiable formula A Boolean formula is satisfiable when it has a satisfying assignment. Definition of the Satisfiability Problem (SAT Given a Boolean formula, determine whether or not it is satisfiable. This material is based upon work supported by the National Science Foundation under Grant No. 1140753