Applied Logic (2ITX0) Summary 2019

Applied Logic Summary 2019
Check the summary of Logic and Set Theory for the pre-knowledge of this subject.


Theme 1: SAT and SMT
A propositional formula is satisfiable (SAT) if you can give values to the variables such that the formula
yields true; SAT is composed from Boolean variables and corresponding operators. We will express several
problems as SAT problems and solve them using the corresponding tools. The basic method to know if a
propositional formula is SAT is to use truth tables but the amount of rows is exponential in the number of
variables. So the bad news is that SAT is NP-complete which means that certain classes of problems are
not solvable in realistic time. However, current SAT solvers are successful for several big formulas. SAT is
extended to SMT (Satisfiability Modulo Theories). In SAT and SMT we don’t think about how to solve it but
we only specify the problem. We use the tool Z3 to solve SMT problems. In Z3 you can do the following
operators:
(declare-const <name constant> <type of constant>) Declare a variable which has a value after running Z3
(e.g. (declare-const S2 Bool) )
(declare-fun <name function> (<type of input>) <type Declare a function which has a formula after running Z3
of output>) (e.g. (declare-fun M (Int) Int) )
(assert <program>) After “assert” is the program that Z3 will run using the
earlier declared variables and functions
(and <first argument> <second argument> … <last Does all operations mentioned between the brackets
argument>)
(or <first argument> <second argument> … <last Does one of the operations mentioned between the
argument>) brackets
( <operator> <arguments> ) Mathematical operations, such as >, <, >=, <=, =, +, *,
-, etc., are written in prefix notation (see on the left). +
may have any number of arguments.
(implies <first argument> <second argument>) For implication (→) in a propositional formula
(iff <first argument> <second argument>) For bi-implication (<->) in a propositional formula
(ite <condition> <result if true> <result if false>) The if-then-else operation first has the condition which
is Boolean, then the result in case the condition is true
and then the result in case the condition is false
(minimize <name constant>) Z3 tries to find the minimum or maximum value of a
OR (maximize <name constant>) variable. Put this outside “assert”.
(check-sat) Checks whether the described program is satisfiable
(get-model) Gets the values for which the described program is
satisfiable

An example of a SAT/SMT problem that has been discussed is the eight queens problem (in which we
looked at the rows, columns and diagonals of a chess board). A trick to find all solutions is by adding a
negation of a found solution to a formula and repeating this until the formula is unsatisfiable. There is also
the rectangle fitting problem (in which we looked at the width, height and coordinates of the rectangles).
For generating a formula in SMT syntax of a SAT formula with a lot of repetition, it is better to use a
program than edit it yourself. We can also solve a sudoku by SAT/SMT (we looked at every row, every
column and every fat 3 by 3 block) or generate one (start by a full sudoku and remove until the formula
extended by the negation of the known solution is satisfiable which means it has another solution).
Planning/scheduling can also be done by SAT/SMT (jobs have a certain running time, some jobs should
run before others, people are assigned to jobs, etc.). Finding the smallest value of a variable can be done
by using binary search (finding a value v for which it is satisfiable and for which v-1 is unsatisfiable) or by
using the built in feature minimize.




1
by Isabel Rutten

, Applied Logic Summary 2019
A conjunctive normal form (CNF) is a conjunction of clauses. A clause is a disjunction of
literals and is a property that we know to be true. A literal is either a variable or the
negation of a variable. The resolution rule states that if there are clauses of the Fig. 1: Formal notation
shape p v V and p v W, then the new clause V v W may be added (see fig. 1: above of resolution rule
the line: assumptions that hold. Underneath the line: conclusions. Alternatives to this
line: , , ). By using the Tseitin transformation (and thus also the resolution rule) we
can check the satisfiability of a CNF: from clauses new clauses can be derived, trying to
derive a contradiction: the empty clause . If this succeeds, we know that the CNF is
unsatisfiable. Unit resolution is the following: if a clause consists of a single literal l (a
unit clause) then the resolution rule allows to remove the literal l from a clause Fig. 2: Formal notation
containing l. A proof system is a set of proof rules of the shape seen in figures 1 of unit resolution
and 2 (so with the horizontal line). A proof system is sound if all its rules are valid and
from the empty clause we can conclude that the CNF is unsatisfiable. A proof system is complete if
every property in the corresponding format that holds, can be proved by only using the proof rules and if for
every unsatisfiable CNF, the empty clause can be derived. To prove that the CNF is a tautology,
prove that is unsatisfiable. To prove that implies , prove that and is unsatisfiable. To prove
that and are equivalent, prove that ( <-> ) so ( or ) and ( and ) is unsatisfiable.
Lewis Carroll made an example with the Tseitin transformation in which sentences can be rewritten to
clauses by defining variables.
DPLL is an algorithm to establish whether a CNF is satisfiable. The idea of DPLL is to first apply unit
resolution as long as possible (so as long as a clause occurs consisting of one literal, also unit-resol) and
then choose a variable p, introduce the cases p and p and for both cases go on recursively. If it is
satisfiable then all involved unit clauses yield a satisfying assignment. Otherwise, it is a big case analysis
yielding for all cases. DPLL always terminates and thus is a complete method to establish satisfiability.
For case analysis, all choices for a variable are correct but one choice may be more efficient than another.
DPLL transforms to resolution: if we have a DPLL proof that a CNF X is unsat, then it can be
transformed to a sequence of resolution steps starting in X and ending in the empty clause and thus the
resolution is complete.
Establishing the satisfiability of an arbitrary propositional formula that is not a CNF can be done by
transforming the formula to CNF while preserving satisfiability and then apply a DPLL based SAT solver on
this CNF. Finding this CNF is always possible but is however often unacceptably large. We can make a
corresponding clause for every 0 in the truth table of a formula and then use the conjunction of all those
clauses. This always works but there may be many clauses due to the exponential amount of rows in a
truth table. The solution to this is the Tseitin transformation: this is a linear transformation of an arbitrary
propositional formula to CNF while preserving satisfiability. The key idea is to
give a name to every subformula (except literals) and use this name as a fresh
variable. For every subformula there is a small CNF cnf( ). Transform the
big formula to the conjunction of all small cnfs of the subformulas. A subformula
stays the same if it consists of one literal but gets a name if not. The
subformula a with the name b is stated with a small CNF as follows: cnf(b <->
a). The whole formula also gets a name. Also the connections between the
subformulas get cnfs. Then we make a conjunction of these cnfs. See figure 3
for an example.
In order to get a real CNF we still need to compute the formulas cnf(b <-> a).
See: cnf(p <-> q) = (p or q) and ( p or q)
cnf(p <-> (q or r)) = ( p or q or r) and (p or q) and (p or r)
cnf(p <-> (q and r)) = (p or q or r) and ( p or q) and ( p or r)
cnf(p <-> (q <-> r)) = (p or q or r) and (p or q or r) and ( p or q or r) and
( p or q or r)
Fig. 3: Example of the
Tseitin transformation

2
by Isabel Rutten