## Description

1. A renamable Horn formula is a CNF formula that can be turned into a Horn formula by negating (all

occurrences of) some of its variables. For example,

(p1 ∨ ¬p2 ∨ ¬p3) ∧ (p2 ∨ p3) ∧ (¬p1)

can be turned into a Horn formula by negating p1 and p2.

Given a CNF formula F, it is in fact possible to derive a 2-CNF formula G such that G is satisfiable if

and only if F is a renamable Horn formula. Moreover, you can derive a renaming (that turns F into a

Horn formula) from a satisfying assignment for G.

Your task is to write a Python program that takes a CNF formula F, in DIMACS format, and also

take a positive integer n (1 ≤ n ≤ 4) as a command-line argument, and does the following (for different

values of n).

Let us take the following formula as our sample input:

c CNF formula (p1 ∨ !p2 ∨ !p3) ∧ (p2 ∨ p3) ∧ (!p1)

p cnf 3 3

1 -2 -3 0

2 3 0

-1 0

(a) [1 marks] When n = 1, your program should check whether the given formula is already a Horn

formula or not, and output already horn and not horn accordingly.

Sample output: not horn

(b) [2 marks] When n = 2, your program should output a 2-CNF formula G, also in DIMACS

format, such that G is satisfiable if and only if F is a renamable Horn formula.

Sample output:

c 2-CNF formula which is sat iff input is renamable Horn

p cnf 3 4

-2 -3 0

2 3 0

1 -3 0

1 -2 0

(c) [2 marks] When n = 3, your program should check whether F is a renamable Horn formula or

not (in other words, whether the G that you would have output in the previous case is satisfiable

or not1

). If F is already a Horn formula, the program should output already horn. Otherwise,

it should output renamable or not renamable accordingly.

Sample output: renamable

(d) [1 marks] When n = 4, your program should output a way to do the renaming of F. Essentially,

you just need to output all the variables (space separated, sorted in ascending order, all in one

line) that need to be negated. If the formula is not a renamable Horn formula or if it is already

a Horn formula to begin with, you should output not renamable or already horn accordingly.

Sample output: 1 2

[1 marks] Submit two CNF formulas as input files in DIMACS format, each having 4 or more

variables and 4 or more clauses, none of them being Horn formulas to begin with, such that one is a

renamable Horn formula while the other is not.

Submission instructions: Submit three files: assign3.py, input1.cnf, and input2.cnf. The

first one should have your code (in the template given here: https://kumarmadhukar.github.io/

courses/assign3.py), and the next two should have a CNF formula each, in DIMACS format, as

asked in the problem statement above. Please also note that your program must not print anything

other than the exact output as mentioned above.

1

It might be interesting to do this by resolution. But you are free to implement any algorithm of your choice.