Exercise 4: Using Minisat

Overview

In this exercise you will use a real sat-solver, MiniSat, to test some propositions to see if they are tautologies. If a proposition is not a tautology you will extract a counter-example. You will download and install the system on your computer, create files that MiniSat can use as input, run the system on your files, and extract answers from the output of running the system.

Learning Objectives

As you work through this exercise we expect you to learn the following:

• The format of DIMACS CNF files
• How to invoke MiniSat
• How to use the negation of a formula to test for tautology-hood.
• How to use MiniSat to find another find additional solutions (or counter examples).

Getting Started

• Read the section in the text, pages 68-78, about SAT-solvers. A perfect understanding of this material is not necessary to work through this exercise, as we are more concerned with using a SAT solver here, than in how they work.
• Download and install the MiniSat SAT solver on your machine.
• Download and read the document How to use the MiniSAT SAT Solver.
• Download and read the document CNF Files about the DIMACS CNF file format.

Directions

1. Formed a proposition by moving formula from the left of the turnstyle into an implication on the right.
   For example: p,q |- r leads to the proposition p -> (q -> r).
2. Negated the formula.
3. Turn the negated formula into CNF.

• 1. Problem (d)
  2. Sequent p \/ q, ~q \/ r |- (p \/ r)
  3. Formula p \/ q => ~q \/ r => (p \/ r)
  4. Negated ~(p \/ q => ~q \/ r => (p \/ r)
  5. CNF Negated (p \/ q) /\ (~q \/ r) /\ ~p /\ ~r
     

• 1. Problem (g)
  2. Sequent (p /\ ~p) |- ~(r => q) /\ (r => q)
  3. Formula (p /\ ~p) => (~(r => q) /\ (r => q))
  4. Negated ~((p /\ ~p) => (~(r => q) /\ (r => q)))
  5. CNF Negated p /\ (~r \/ q \/ r) /\ (~r \/ q \/ ~q) /\ ~p

• 1. Problem (h)
  2. Sequent (p => q), (s => t) |- (p \/ s) => (q /\ t)
  3. Formula (p => q) => (s => t) => p \/ s => (q /\ t)
  4. Negated ~((p => q) => (s => t) => p \/ s => (q /\ t))
  5. CNF Negated (~p \/ q) /\ (~s \/ t) /\ (p \/ s) /\ (~q \/ ~t)

What To Do

• Create a DIMACS CNF file to encode each negated CNF formula.
• Run MiniSat.
• Determine if the formula is a tautology. If it is not, find two counter examples. (See How to use the MiniSAT SAT Solver for strategies for finding more than one solution).
• You should discover at least on tautology, and one-non tautology.

What To Turn In

• Write up a simple report about what you discovered.
• Create a small directory with the *.cnf files and your report.
• Drop it in the Ex4 folder in the class drop box
• Be prepared to talk about your solution in class.

Back to the class web-page.
Back to the Course Schedule.