Advanced C Programming - Max Planck Society

1 Advanced C ProgrammingSebastian Term 2008/09computer sciencesaarlanduniversity1 Why Advanced C? Our Iwe need experienced C programmers Religious IportabilityIefficiencyIpowerful and flexible Real IunixInetwork softwareIembedded systemsIresearch: graphics, vision, formal methodsIentertainment: games, films2 Content ISAT Solving IBasic C SetupEfficient Algorithms ISAT Solving IIStyle, Signals, Timing and ToolsSAT Solving IIIM emory Management and Tools3 Content IISoftware Engineering in the SmallKnow the Compiler and ProcessorEfficient Algorithms IIParallelismRecent C Standards4 Propositional logicIlogic of truth valuesIdecidable (but NP-complete)Ican be used to describe functions over a finite domainIimportant for hardware applications ( , model checking)5 SyntaxIpropositional variables:P,Q,R Ilogical symbols: and, or, not,>true, falseIliterals are propositional variables or their negation:P, PIclauses are (posssibly empty) disjunctions of literals.

2 P Q RIclause sets are sets of clauses interpreted as the conjunction of allclausesIliterals, clauses and clause sets are formulas6 SemanticsClassicalIn classical logic (dating back to Aristoteles) there are only two truthvalues true and false which we shall denote, respectively, by 1 and propositional variable has no intrinsic meaning. The meaning of apropositional variable has to be defined by a -valuationis a mapA: {0,1}.where{0,1}is the set oftruth Value of a Literal, Clause, Clause SetGiven a -valuationA, it can be extended to formulasA: formulas {0,1}inductively as follows:A( ) = 0A(>) = 1A(P) =A(P)A( P) = 1 A(P)A(A B) = max(A(A),A(B))A(C D) = min(A(C),A(D))9 Models, Validity, and SatisfiabilityValidityFisvalid inA(Ais amodelofF;Fholds underA):A|=F: A(F) = 1 Fisvalid(or is atautology):|=F: A|=Ffor all -valuationsA(Un)SatisfiabilityFis calledsatisfiableif there exists anAsuch thatA|=F.

3 OtherwiseFis calledunsatisfiable(orcontradictory).Hen ce,Fis valid iff Fis say thatN|=FiffN Fis UnsatisfiabilityEvery formulaFcontains only finitely many propositional ,A(F) depends only on the values of those finitely manyvariables propositional variables, then it is sufficient tocheck 2nvaluations to see whetherFis satisfiable or not truth the satisfiability problem is clearly decidable (but, by Cook s Theorem,NP-complete). Nevertheless, in practice, there are (much) bettermethods than truth tables to check the satisfiability of a DPLL ProcedureGoalGiven a propositional formula in CNF (or alternatively, a finite setNofclauses), check whether it is satisfiable (and optionally: outputonesolution, if it is satisfiable).AssumptionClauses contain neither duplicated literals nor complementary the complementary literal ofL, ,P= Pand P= ValuationsSince we will construct satisfying valuations incrementally, we considerpartial valuations(that is, partial mappingsA: {0,1}).

4 Every partial valuationAcorresponds to a setMof literals that does notcontain complementary literals, and vice versa:IA(L) is true, ifL (L) is false, ifL (L) is undefined, if neitherL MnorL clause istrueunder a partial valuationA(or under a setMof literals)if one of its literals is true; it is false if all its literals arefalse; otherwise ClausesObservationLetAbe a partial valuation. If the setNcontains a clauseC, such thatall literals but one inCare false underA, then the following propertiesare equivalent:Ithere is a valuation that is a model ofNand is a valuation that is a model ofNand extendsAand makesthe remaining called aunit clause;Lis called aunit Davis-Putnam-Logemann-Loveland ProcedurebooleanDPLL(literal setM, clause setN){if (all clauses inNare true underM) return true;elsif (some clause inNis false underM) return false;elsif (Ncontains unit clauseP) return DPLL(M {P},N);elsif (Ncontains unit clause P) return DPLL(M { P},N);else{letPbe some undefined variable inN;if (DPLL(M { P},N)) return true;else return DPLL(M {P},N);}}Initially, DPLL is called with an empty literal set and the clause IterativelyIn practice, there are several changes to the procedure:IThe branching variable is not chosen algorithm is implemented iteratively.

5 The backtrack stack is managed explicitly(it may be possible and useful to backtrack more than one level).IInformation is reused by DPLL with RefinementsThe DPLL procedure is modelled by a transition relation DPLLon a setof N,whereMis alist of annotated literalsandNis a set of literalIL: deduced literal, due to unit : decision literal (guessed literal).17 DPLL RulesUnit PropagateM N {C L} DPLLM L N {C L}ifCis false underMandLis undefined N DPLLM Ld NifLis undefined N {C} DPLL failifCis false underMandMcontains no decision RulesBackjumpM LdM N DPLLM L Nif there is some backjump clause C L such thatN|=C L ,Cis false underM , andL is undefined underM .19 BacktrackingThe Backjump rule is always applicable, if the list of literalsMcontainsat least one decision literal and some clause inNis false are many possible backjump clauses. One candidate:L1 .. Ln,where theLiare all the decision literals inM LdM.

6 (But usually thereare better choices.)20 DIMACS SAT File Input FormatSyntax{c<comment>} p cnf<number of variables> <number of clauses>{<clause>0} A<clause>is a sequence of integers from +<number of variables>to <number of variables>, except 0, separated by clausesP Q R,Q Rcan be coded by the filec first, simple examplep cnf 3 21 -2 3 02 -3 021