Formalization And Implementation Of Modern SAT Solvers
Noname manuscript No.(will be inserted by the editor)Formalization and Implementation of Modern SATSolversFilip MarićReceived: date / Accepted: dateAbstract Most, if not all, state-of-the-art complete SAT solvers are complexvariations of the DPLL procedure described in the early 1960’s. Published descriptions of these modern algorithms and related data structures are giveneither as high-level (rule-based) transition systems or, informally, as (pseudo)programming language code. The former, although often accompanied with(informal) correctness proofs, are usually very abstract and do not specifymany details crucial for efficient implementation. The latter usually do notinvolve any correctness argument and the given code is often hard to understand and modify. This paper aims at bridging this gap: we present SATsolving algorithms that are formally proved correct, but at the same time theycontain information required for efficient implementation. We use a tutorial,top-down, approach and develop a SAT solver, starting from a simple designthat is subsequently extended, step-by-step, with the requisite series of features. Heuristic parts of the solver are abstracted away, since they usually donot affect solver correctness (although they are very important for efficiency).All algorithms are given in pseudo-code. The code is accompanied with correctness conditions, given in Hoare logic style. Correctness proofs are formalizedwithin the Isabelle theorem proving system and are available in the extendedversion of this paper. The given pseudo-code served as a basis for our SATsolver argo-sat.This work was partially supported by Serbian Ministry of Science grant 144030.Filip MarićFaculty of MathematicsUniversity of BelgradeSerbiaE-mail: filip@matf.bg.ac.yu
21 IntroductionPropositional satisfiability problem (SAT) is the problem of deciding if there isa truth assignment under which a given propositional formula (in conjunctivenormal form) evaluates to true. It is a canonical NP-complete problem [Coo71]and it holds a central position in the field of computational complexity. SATproblem is also important in many practical applications such as electronicdesign automation, software and hardware verification, artificial intelligence,and operations research. Thanks to recent advances in propositional solving,SAT solvers are becoming a tool suitable for attacking more and more practical problems. Some of the solvers are complete, while others are stochastic.For a given SAT instance, complete SAT solvers can either find a solution (i.e.,a satisfying variable assignment) or show that no solution exists. Stochasticsolvers, on the other hand, cannot prove that an instance is unsatisfiable although they may be able to find a solution for certain kinds of large satisfiableinstances quickly. The majority of the state-of-the-art complete SAT solversare based on the branch and backtracking algorithm called Davis-PutnamLogemann-Loveland, or DPLL [DP60,DLL62]. Starting with the work on theGRASP and SATO systems [MSS99,Zha97], and continuing with Chaff, BerkMin and MiniSAT [MMZ 01,GN02,ES04], the spectacular improvements inthe performance of DPLL-based SAT solvers achieved in the last years aredue to (i) several conceptual enhancements of the original DPLL procedure,aimed at reducing the amount of explored search space, such as backjumping,conflict-driven lemma learning, and restarts, and (ii) better implementationtechniques, such as the two-watch literals scheme for unit propagation. Theseadvances make it possible to decide the satisfiability of industrial SAT problems with tens of thousands of variables and millions of clauses.While SAT solvers have become complex, describing their underlying algorithms and data structures has become a nontrivial task. Some papers describeconceptual, higher level concepts, while some papers describe system level architecture with smart implementation techniques and tricks. Unfortunately,there is still a large gap between these two approaches. Higher level presentations, although clean and accompanied with correctness proofs, omit manydetails that are vital to efficient solver implementation. Lower level presentations usually give SAT solver algorithms in a form of pseudo-code. The opensource SAT solvers themselves are, in a sense, the most detailed presentationsor specifications of SAT solving techniques. The success of MiniSAT [ES04],and the number of its re-implementations, indicate that detailed descriptionsof SAT solvers are needed and welcome in the community. However, in order toachieve the highest possible level of efficiency, these descriptions are far fromthe abstract, algorithmic level. Often, one procedure in the code contains several higher level concepts or one higher level algorithm is spread across severalcode procedures. The resulting pseudo-code, although almost identical to theaward winning solvers, is, in our opinion, hard to understand, modify, and reason about. This paper is an attempt to bring these two approaches together.We claim that SAT solvers can be implemented so that (i) the code follows
3higher level descriptions that make the solver easy to understand, maintain,modify, and to prove correct, and (ii) it contains lower level implementationtricks, and therefore achieves high efficiency. We support this claim by (i) ourSAT solver argo-sat, that represents a rational reconstruction of MiniSAT,obeying the given two requirements, and (ii) our correctness proofs (formalizedin Isabelle) for the presented algorithms, accompanying our SAT solver.1Complicated heuristics (e.g., for literal selection, for determining the appropriate clause database size, restart strategy) represent important parts ofmodern SAT solvers and are crucial for solver efficiency. While a great effortis put on developing new heuristics, and researchers compete to find moreand more effective ones, we argue that those can be abstracted from the corepart of the solver (the DPLL algorithm itself) and represented as just a fewadditional function calls (or separated into external classes in object-orientedsetting). No matter how complicated these heuristics are, they do not affectthe solver correctness as long as they meet a several, usually trivial, conditions.Separating the core DPLL algorithm from complicated, heuristic parts of thesolver leads to simpler solver design, and to more reliable and flexible solvers.In the rest of the paper, we develop the pseudo-code of a SAT solver fromscratch and outline its correctness arguments along the way. We take a topdown approach, starting with the description of a very simple solver, andintroduce advanced algorithms and data structures one by one. The partialcorrectness of the given code is proved using the proof system Isabelle (in theHoare style). Isabelle proof documents containing the proofs of correctness conditions are available in [Mar08]. A longer version of this paper, available fromhttp://argo.matf.bg.ac.rs contains these proofs presented in a less formal,but more readable manner. In this paper we do not deal with termination issues. Still, it can be shown that all presented algorithms are terminating2 .Overview of the paper. In §2 we briefly describe the DPLL algorithm, presenttwo rule-based SAT solver descriptions, and describe the basics of programverification and Hoare logic. In §3 we introduce the background theory inwhich we will formalize and prove the properties of a modern SAT solver, anddescribe the pseudo-code language used to describe the implementation. Thebulk of the paper is in §4: it contains descriptions of SAT solver algorithmsand data structures and outlines their correctness proofs. We start from thebasic backtrack search (§4.1), then introduce unit propagation (§4.2), backjumping, clause learning and firstUIP conflict analysis (§4.3), conflict clauseminimization (§4.4), clause forgetting (§4.5), restarts (§4.6), exploiting literalsasserted at zero level of assertion trail (§4.7), and introduce efficient detectionof conflict and unit clauses using watch literals (§4.8, §4.9). In §5 we give ashort history of SAT solver development, and in §6 we draw final conclusions.1Web page of argo-sat is http://argo.matf.bg.ac.rs/Formal termination proofs of rule-based systems on which our implementation is basedare available in [Mar08].2
4function dpll (F : Formula) : (SAT, UNSAT)beginif F is empty thenreturn SATelse if there is an empty clause in F thenreturn UNSATelse if there is a pure literal l in F thenreturn dpll(F [l ])else there is a unit clause [l] in F thenreturn dpll(F [l ])else beginselect a literal l occurring in Fif dpll(F [l ]) SAT thenreturn SATelsereturn dpll(F [l ])endendFig. 1 DPLL algorithm - recursive definition2 BackgroundDavis-Putnam-Logemann-Loveland (DPLL) algorithm. Most of the completemodern SAT solvers are based on the DPLL algorithm [DP60,DLL62]. Its recursive version is shown in the Figure 1, where F denotes a set of propositionalclauses, tested for satisfiability, and F [l ] denotes the formula obtainedfrom F by substituting the literal l with , its opposite literal l with , andsimplifying afterwards. A literal is pure if it occurs in the formula but its opposite does not. A clause is unit if it contains only one literal. This recursiveimplementation is practically unusable for larger formulae and therefore it willnot be used in the rest of this paper.Rule-based SAT solver descriptions. During the last few years, two transition rule systems which model the DPLL-based SAT solvers and related SMTsolvers have been published [NOT06,KG07]. These descriptions define the toplevel architecture of solvers as a mathematical object that can be grasped asa whole and fruitfully reasoned about. Both systems are accompanied withpen-and-paper correctness and termination proofs. Although they succinctlyand accurately capture all major aspects of the solvers’ global operation, theyare high level and far from the actual implementations. Both systems modelthe solver behavior as transitions between states. States are determined bythe values of solver’s global variables. These include the set of clauses F , andthe corresponding assertion trail M . Transitions between states are performedonly by using precisely defined transition rules. The solving process is finishedwhen no more transition rules apply (i.e., when final states are reached).The system given in [NOT06] is very coarse. It can capture many differentstrategies seen in the state-of-the art SAT solvers, but this comes at a price— several important aspects still have to be specified in order to build animplementation based on the given set of rules.
5Decide:/Ml Fl, l M : M ldUnitPropag:l l1 . . . lk FConflict:C no cf lctExplain:l Cl1 , . . . , lk MM : M ll1 . . . lk FC : {l1 , . . . , lk }l, l /Ml1 , . . . , lk Ml l1 . . . lk Fl1 , . . . , lk lC : C {l1 , . . . , lk } \ {l}Learn:l1 . . . lk /FC {l1 , . . . , lk }F : F {l1 . . . lk }Backjump:C {l, l1 , . . . , lk }l l1 . . . lk Flevel l m level liC : no cf lctM : M [m] lForget:c FF \c cC no cf lctF : F \ cRestart:C no cf lctM : M [0]Fig. 2 Rules of dpll as given in [KG07]. (li lj denotes that the literal li precedes lj inM , and M [m] denotes the prefix of M up to the level m)The system given in [KG07] gives a more detailed description of someparts of the solving process (particularly the conflict analysis phase) thanthe one given in [NOT06]. Since the system of [KG07] is used as a basis ofthe implementation given in this paper, we list its transition rules in Figure2. Together with the formula F and the trail M , the state of the solver ischaracterized by the conflict analysis set C which is either a set of literals, orthe distinguished symbol no cf lct. The input to the system is an arbitrary setof clauses F0 . Solving starts from the initial state in which F F0 , M [ ],and C no cf lct. The rules have guarded assignment form: above the line isthe condition that enables the rule application, below the line is the updateto the state variables.Formal proofs. Over the last years, in all areas of mathematics and computerscience, machine checkable formal proofs have gained more and more importance. There are growing efforts in this direction, with many extremely complex theorems formally proved and with many software tools for producing andchecking formal proofs. Some of them are Isabelle, HOL, Coq, PVS, Mizar,etc. A comparison of these tools can be found in [Wie03].Program verification. Program verification is the process of formally provingthat a computer program meets its specification (that formally describes theexpected program behavior). Following the lessons from major software failures, an increasing amount of effort is being invested in this field. Many fundamental algorithms and properties of data structures have been formalized and
6verified. Also, a lot of work has been devoted to formalization of compilers,program semantics, communication protocols, security protocols, etc. Formalverification is important for SAT and SMT solvers and the first steps towardsthis direction have been made [KG07,NOT06,Bar03].Hoare logic. Verification of imperative programs is usually done in Floyd-Hoarelogic [Hoa69], a formal system that provides a set of logical rules in order toreason about the correctness of computer programs with the rigor of mathematical logic. The central object in Hoare logic is Hoare triple which describeshow the execution of a piece of code changes the state of a computation. AHoare triple is of the form {P } code {Q}, where P (the precondition) and Q(the postcondition) are formulae of a meta-logic and code is a programminglanguage code. Hoare triple should be read as: ”Given that the assertion Pholds at the point before the code is executed, and the code execution terminates, the assertion Q will hold at the point after the code was executed”.3 Notation and DefinitionsIn this section we introduce the notation and definitions that will be used inthe rest of the paper.3.1 Background TheoryIn order to reason about the correctness of SAT solver implementations, wehave to formally define the notions we are reasoning about. This formalizationwill be made in higher-order logic of the system Isabelle. Formulae and logicalconnectives of this logic ( , , , , ) are written in the usual way. Thesymbol denotes syntactical identity of two expressions. Function and predicate applications are written in prefix form, as in (f x1 . . . xn ). Existentialquantifier is written as and universal quantifier is written as .We assume that the background theory we are defining includes the builtin theory of lists and (finite) sets. Syntax of these operations is summarizedin the first column of the Figure 3, and the semantics is informally describedin the second column.Basic types. The logic used is typed, and we define the basic types.Definition ue or falsenatural numbernatural number.either a positive variable ( vbl) or a negative variable ( vbl)a list of literalsa list of clausesa list of literals
7(a, b)[][e1 , . . . , en ]e # listlist1 @list2e listlist1 list2list \ elist1 \ list2(first list)(second list)(head list)(tail list)(last list)(length list)(unique list){}e setset1 set2 set {a1 7 b1 , . . . , ak 7 bk }H(ai )the ordered pair of elements a and b.the empty list.the list of n given elements e1 , . . . , en .the list obtained by prepending element e to the list list.the list obtained by appending lists list1 and list2 .e is a member of the list list.all elements of list1 are also elements of list2 .the list obtained by removing all occurrences of the element efrom the list list.the list obtained from the list list1 by removing all elementsof the list list2 from it.the first element of the list list. (assuming the list is not empty).the second element of the list list(assuming the list has at least two elements).a synonym for (first list).the list obtained by removing the first element of the list list.the last element in the nonempty list list.the length of the list list.true iff the list list contains no repeating elements.the empty set.element e is a member of the set set.the set union of set1 and set2the number of elements in the set set.the mapping of elements {a1 , . . . , ak } to elements {b1 , . . . , bk }the image of the element ai in the mapping H(provided that it has been defined).Fig. 3 List and set operationsAlthough we use typed logic, for the sake of readability we sometimes omitsorts and use the following naming convention: Literals (i.e., variables of thetype Literal) are denoted by l (e.g. l, l′ , l0 , l1 , l2 , . . .), variables by vbl, clausesby c, formulae by F , and valuations by v.Although most of the following definitions are formalized using the primitive recursion, in order to simplify the presentation and improve readabilitywe give them as natural language descriptions.Definition 2 The opposite literal of a literal l, denoted l, is defined by: vbl vbl, vbl vbl.We abuse the notation and overload some symbols. For example, the symbol denotes both set membership and list membership. It is also used todenote that a literal occurs in a formula.Definition 3 A formula F contains a literal l (i.e., a literal l occurs in aformula F ), denoted l F , iff c. c F l c.Symbol vars is also overloaded and denotes the set of variables occurringin a clause, formula, or valuation.Definition 4 The set of variables that occur in a clause c is denoted by(vars c). The set of variables that occur in a formula F is denoted (vars F ).The set of variables that occur in a valuation v is denoted (vars v).
8The semantics (satisfaction and falsification relations) is defined by:Definition 5 A literal l is true in a valuation v, denoted v l, iff l v.A clause c is true in a valuation v, denoted v c, iff l. l c v l.A formula F is true in a valuation v, denoted v F , iff c. c F v c.We will write v 2 l to denote that l is not true in v, v 2 c to denote that cis not true in v, and v 2 F to denote that F is not true in v.Definition 6 A literal l is false in a valuation v, denoted v l, iff l v.A clause c is false in a valuation v, denoted v c, iff l. l c v l.A formula F is false in a valuation v, denoted v F , iff c. c F v c.We will write v 2 l to denote that l is not false in v, v 2 c to denote thatc is not false in v, and v 2 F to denote that F is not false in v. We will saythat l (or c, or F ) is unfalsified in v.Definition 7 A valuation v is inconsistent, denoted (inconsistent v), iff itcontains both literal and its opposite i.e., l. v l v l. A valuation isconsistent, denoted (consistent v), iff it is not inconsistent.Definition 8 A model of a formula F is a consistent valuation under whichF is true. A formula F is satisfiable, denoted (sat F ) iff it has a model i.e., v. (consistent v) v FDefinition 9 A formula F entails a clause c, denoted F c, iff c is true inevery model of F . A formula F entails a literal l, denoted F l, iff l is truein every model of F . A formula F entails valuation v, denoted F v, iff itentails all its literals i.e., l. l v F l. A formula F1 entails a formula F2denoted F1 F2 , if every model of F1 is a model of F2 .Definition 10 Formulae F1 and F2 are logically equivalent, denoted F1 F2 ,if any model of F1 is a model of F2 and vice versa, i.e., if F1 F2 , and F2 F1 .Definition 11 A clause c is unit in a valuation v with a unit literal l, denoted(isUnit c l v) iff l c, v 2 l, v 2 l and v (c \ l) (i.e., l′ . l′ c l′ 6 l v l′ ).Definition 12 A clause c is a reason for propagation of literal l in valuationv, denoted (isReason c l v) iff l c, v l, v (c \ l), and for each literall′ (c \ l), the literal l′ precedes l in v.Definition 13 The resolvent of clauses c1 and c2 over the literal l, denoted(resolvent c1 c2 l) is the clause (c1 \ l)@(c2 \ l).Assertion Trail. In order to build a non-recursive implementation of the dpllalgorithm, the notion of valuation should be slightly extended. During thesolving process, the solver should keep track of the current partial valuation.In that valuation, some literals are called decision literals. Non-decision literals are called implied literals. These check-pointed sequences that represent
9valuations with marked decision literals will be stored in the data structurecalled assertion trail. All literals that belong to the trail will be called assertedliterals. Assertion trail operates as a stack and literals are always added andremoved from its top. We extend the background theory with the followingtype:Definition 14Traila list of literals, with some of them marked as decision literals.A trail can be implemented, for example, as a list of (Literal, Boolean)ordered pairs. We will denote trails by M (e.g. M, M ′ , M0 , . . .).Example 1 A trail M could be [ 1, 2, 6, 5, 3, 4, 7]. The decisionliterals are marked with the symbol on their left hand sides.Definition 15 (decisions M ) is the list of all marked elements (i.e., of alldecision literals) from a trail M .Definition 16 (lastDecision M ) is the last element in a trail M that is marked.Definition 17 (decisionsTo M l) is the list of all marked elements from a trailM that precede the first occurrence of the element l, including l if it is marked.Example 2 For the trail given in Example 1, (decisions M ) [ 2, 5, 7],(lastDecision M ) 7, (decisionsTo M 4) [ 2, 5],(decisionsTo M 7) [ 2, 5, 7].Definition 18 The current level for a trail M , denoted (currentLevel M ), isthe number of marked literals in M , i.e., (currentLevel M ) (length (decisions M )).Definition 19 The decision level of a literal l in a trail M , denoted (level l M ),is the number of marked literals in the trail that precede the first occurrenceof l, including l if it is marked, i.e., (level l M ) (length (decisionsTo M l)).Definition 20 (prefixToLevel M level) is the prefix of a trail M containingall elements of M with levels less or equal to level.Definition 21 (prefixBeforeLastDecision M ) is the prefix of a trail M up tothe last element that is marked, not including that element.3Example 3 For the trail in Example 1, (level 1 M ) 0, (level 4 M ) 2,(level 7 M ) 3, (currentLevel M ) 3, (prefixToLevel M 1) [ 1, 2, 6],(prefixBeforeLastDecision M ) [ 1, 2, 6, 5, 3, 4].Definition 22 The last asserted literal of a clause c, denoted (lastAssertedLiteral c M ),is the literal from c that is in M , such that no other literal from c comes afterit in M .3 Note that some of the defined functions are partial, and are not defined for all trails.For example, (prefixBeforeLastDecision M ) is defined only for trails that contain a decisionliteral.
10Definition 23 The maximal decision level for a clause c in a trail M , denoted(maxLevel c M ), is the maximum of all decision levels of all literals from c thatbelong to M , i.e., (maxLevel c M ) (level (lastAssertedLiteral c M ) M ).Example 4 Let c is [ 4, 6, 3], and M is the trail from the example 1. Then,(maxLevel c M ) 2, and (lastAssertedLiteral c M ) 4.3.2 Pseudo-code LanguageAll algorithms in the following text will be specified in a pascal-like pseudocode language. An algorithm specification consists of a program state declaration, followed by a series of function definitions.The program state is specified by a set of global variables. The state isgiven in the following form, where Typei can be any type of the backgroundtheory.varvar1 : Type1.vark : TypekA block is a sequence of statements separated by the symbol ;, where astatement is one of the following:begin block endx : expressionif condition then statementif condition then statement else statementwhile condition do statementrepeat statement until conditionfunction name(arg1 , ., argn )returnConditions and expressions can include variables, functions calls, and evenbackground theory expressions.Function definitions are given in the following form, where Typei is thetype of the argument argi , and Type is the return type of the function.function name (arg1 : Type1 , ., argk : Typek ) : TypebeginblockendIf a function does not return a value, then its return type is omitted. Afunction returns a value by assigning it to a special variable ret. An explicitreturn statement is supported. Parameters are passed by value. If a parameterin the parameter list is marked with the keyword var, then it is passed byreference. Functions marked as const do not change the program state. Inorder to save some space, local variable declarations will be omitted whentheir type is clear from the context.We allow the use of meta-logic expressions within our algorithm specifications. The reason for this is twofold. First, we want to simplify the presentationby avoiding the need for explicit implementation of some trivial concepts. For
11example, we assume that lists are supported in the language and we directlyuse the meta-logic notation for the list operations, having in mind that theircorrect implementation can be easily provided. Second, during the algorithmdevelopment, we intentionally leave some conditions at a high level and postpone their implementation. In such cases, we use meta-logic expressions inalgorithm descriptions to implicitly specify the intended (post)conditions forthe unimplemented parts of the code. For example, we can write if M Fthen, without specifying how the test for M F should effectively be implemented. These unimplemented parts of the code will be highlighted. Alternatively, a function satisfies(M : Trail, F : Formula) : Boolean could beintroduced, which would have the postcondition {ret M F }. Theabove test would then be replaced by if satisfies(M, F) then.4 SAT Solver Algorithms and Data StructuresIn this section, we present SAT solver algorithms and data structures, andoutline their correctness proofs. Our implementation will follow the rules ofthe framework described in [KG07]. We give several variants of SAT solver,labeled as SAT solver v.n. To save space, instead of giving the full code for eachSAT solver variant, we will only print changes with respect to the previousversion of code. These changes will be highlighted. Lines that are added willbe marked by on the right hand side, and lines that are changed will bemarked by * on the right hand side. Each solver variant contains a function:function solve (F0 : Formula) : {SAT, UNSAT}which determines if the given formula F0 is satisfiable or unsatisfiable. Thisfunction sets the global variable satF lag and returns its value.The partial correctness of the SAT solver v.n is formalized by the followingsoundness theorem:Theorem 1 SAT solver v.n satisfies the Hoare triple:{ } solve(F0 ) {(satF lag U N SAT (sat F0 )) (satF lag SAT M F0 )}This theorem will usually be proved by proving two lemmas:1. Soundness for satisfiable formulae states that if the solver returns the valueSAT , then the formula F0 is satisfiable.2. Soundness for unsatisfiable formulae states that if the solver returns thevalue U N SAT , then the formula F0 is unsatisfiable.Notice that, under the assumption that solver is terminating (which is notproved in this paper), these two soundness lemmas imply solver completeness.To prove soundness, a set of conditions that each solver variant satisfieswill be formulated. Also, preconditions that have to be satisfied before eachfunction call will be given. All proofs that these conditions are invariants ofthe code and that preconditions are met before each function call are availablein the longer version of this paper.
124.1 Basic Backtrack SearchThe simplest, but still sound and complete, SAT solver can be implementedusing the truth-table method which enumerates and checks all valuations. Inthis section we give a solver that is based on iterative backtrack search. Theonly improvement over the basic truth-table satisfiability checking is the useof early search-tree pruning. This code can be also seen as a non-recursiveimplementation of a simplified DPLL algorithm (pure literal and unit clauserules are omitted). All successive solver refinements are based on this simplecode, so we will present it and prove its correctness for methodological reasons.First we give an informal description of the solver. Formula F0 is testedfor satisfiability. The trail M represents the current partial valuation. Initiallyit is empty. Literals are added to the trail and marked as decision literals.Whenever a literal is added to the trail, F0 is checked for inconsistency. WhenF0 is inconsistent with the current trail, we say that a conflict occurred. Theclause c F0 , such that M c is called a conflict clause. When a conflictoccurs, the last decision literal on the trail is flipped, i.e., it and all literalsafter it are backtracked, and its opposite is added to the trail, but this time asa non-decision literal. If a conflict occurs with no decision literals on the trail,then we say that a conflict at decision level zero occurred and F0 is determinedto be unsatisfiable. If M contains all variables that occur in F0 and conflictdoes not occur, then F0 is determined to be satisfiable and M is its model.SAT solver v.1varsatF lag : {UNDEF, SAT, UNSAT}F0 : FormulaM : Trailfunction solve (F0 : Formula) : {SAT, UNSAT}beginsatF lag UNDEF;M : [];while satF lag UNDEF do beginif M F0 thenif (decisions M ) [] thensatF lag : UNSATelseapplyBacktrack()elseif (vars M ) (vars F0 ) thensatF lag : SATelseapplyDecide()endendfunction applyDecide()beginl : selectLiteral();assertLiteral(l, true)end
13function applyBacktrack()beginl : (lastDecision M);M : (prefixBeforeLastDecision M );assertLiteral(l,
from F by substituting the literal l with , its opposite literal l with , and simplifying afterwards. A literal is pure if it occurs in the formula but its op-posite does not. A clause is unit if it contains only one literal. This recursive implementation is practically unusable for
tion uses rules and procedures to prescribe behaviour [31]. The nature of formalization is the degree to which the workers are provided with rules and procedures [32] that deprive versus encourage creative, autonomous work and learning. In organization with high formalization, there are explicit rules which are likely to impede the
use a type theory with dependent types as encoded by Lean to de ne logical objects and operations. Then, we describe features of Lean which facilitate the formalization of mathematical objects. Lastly, after presenting the group theory concepts informally, we present our de nitions of these concepts within the type theory, and we state and .
interface between safety-critical real-time operating systems and application software, as well as a set of functionalities aimed to improve the safety and certification process of such safety-critical systems. The formalization is a complete model of ARINC 653, and provides a necessary foundation for the formal development
[english text – texte anglais] www.edu.int intergovernmental organization formalization framework agreement for recognition and endorsement of the edu
Modern's abc of Objective Chemistry Modern's abc of Objective Mathematics Modern's abc of Objective Biology Modern's abc of Crash Course Physics (JEE-Main) Modern's abc of Crash Course Chemistry (JEE-Main) Modern's abc of Crash Course Mathematics (JEE-Main) E info@mbdgroup.com W www.mbdgroup
formal logic, especially incorporation of negation as failure, facilitate the formalization of the human . In modern times this effort culminated in boolean logic [11], first order logic [14], and various other advanced logics. These logics, however, are limited and could . The Primer pr
PUBLICATIONS OF JOHN CORCORAN ON ARISTOTLE Indeed, one of the great strides forward in the modern study of Aristotle’s syllogistic was the realization that it is a system of natural deduction. —Kevin Flannery, SJ [2001, 219]. Corcoran [ ] has convincingly shown that the best formalization of Aristotle’s reductio ad impossibile is by
Introduction The three-year (2010-2013) ‘Fields of Britannia’ project, funded by the Leverhulme Trust, aims to explore the transition from Roman Britain to medieval England and Wales from a broad landscape perspective, reaching beyond the traditional site-based approach. One of the most distinctive features of the British landscape today is its intricate pattern of fields, and it is their .
