Homework 05 - due 2 April 2008 (after break)
Extend the DPLL SAT solver from homework04 with the ability to generate resolution proofs.
As before, if a given formula is satisfiable, the SAT solver should produce an assignment to all variables such that the formula evaluates to true under this assignment.
Additionally, if a given formula is unsatisfiable, the SAT solver should produce unsatisfiability proof in some format. Use proof trees for resolution proofs, whose nodes indicate the variable on which resolution is performed and contain subtrees for proofs of clauses on which resolution is performed.
Optional extension (can be used for project): Extend this solver with 2-literal watching, lemma learning and heuristics. You can look at the source code of existing implementations to gain insight into techniques (such as http://sourceforge.net/projects/dpt ) but you are not allowed to copy it, you must write your own implementation.
We will run a small competition of implemented solvers.
Note that it can be useful to know about SAT solvers.
Test examples shown in the class:
Consider the notion of Substitutions for First-Order Logic.
Part a) Consider an implementation of that definition of sfsubst as a recursive function on syntax trees that directly follows its definition. Consider formulas with many identical quantifiers, . More precisely, let denote formula and denote formula for all . How many accesses to syntax tree nodes does this function perform on the abstract syntax tree of formula ?
Part b) Define the “fast, safe” substitution, fsfsubst, with the property that for a formula with syntax tree nodes, the number of accesses to syntax tree nodes is . (You do not need to implement it, but this may be helpful if for you to debug your definition.)
Part c) Prove (using appropriate proof technique) that your definition of fsfsubst has the property
You can assume that formulas are built using only these symbols:
- one constant
- one unary function symbol
- one binary relation symbol
- operations , , as the only logical operations.
Problem 4 (Optional)
Use Compactness for First-Order Logic to prove the following theorem:
If a set of sentences has arbitrarily large finite models (that is, for every , there exists a model with a finite set of at least elements), then has an infinite model.