Abstract
The Propositional Logic plays a central role in Artificial Intelligence. Extremely simple, this logic already addresses some of the most important problems in computer theory. It allows an incredible panel of pragmatic solutions to be successfully applied on a large number of (theoretically) hard problems. Its apparent simplicity allows one to design very efficient and compact algorithms to tackle, in practice, problems lying at the first levels of the complexity classes. In this chapter, we first present the kind of A.I. problems that can typically be addressed by this formalism. Then, we present an historical view of the impressive progresses observed in the practical solving of the Satisfiability (SAT) problem. Then, we introduce the concept of Knowledge Compilation, another important field of A.I. often build upon Propositional Logic. We also introduce Quantified Boolean Formula (QBF), a natural extension of SAT to quantifiers.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
A Horn clause is a clause containing at most one positive literal. A Horn formula is a formula under CNF containing only Horn clauses.
- 3.
See evaluation site Maxsat, maxsat.ia.udl.cat.
- 4.
This time is often much longer than the time of a single request.
- 5.
Note that any theory can still be compiled into a complete theory for unit resolution (del Val 1994).
- 6.
An important development effort has been carried out for providing a very simple and useful SDD package: http://reasoning.cs.ucla.edu/sdd/.
References
Achlioptas D, Ricci-Tersenghi F (2009) Random formulas have frozen variables. SIAM J Comput 39(1):260–280
Armoni R, Egorov S, Fraer R, Korchemny D, Vardi M (2005) Efficient LTL compilation for SAT-based model checking. In: Proceedings of the 2005 IEEE/ACM international conference on computer-aided design, pp 877–884
Audemard G, Simon L (2007) GUNSAT: a greedy local search algorithm for unsatisfiability. In: IJCAI’07: proceedings of the 20th international joint conference on artifical intelligence. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, pp 2256–2261
Audemard G, Simon L (2009) Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of international joint conference on artificial intelligence (IJCAI), pp 399–404
Audemard G, Simon L (2014) Lazy clause exchange policy for parallel SAT solvers. In: International conference on theory and applications of satisfiability testing (SAT), pp 197–205
Audemard G, Benhamou B, Siegel P (2000) AVAL: an enumerative method for SAT. In: Computational logic—CL 2000. Springer, pp 373–383
Audemard G, Bordeaux L, Hamadi Y, Jabbour S, Sais L (2008) A generalized framework for conflict analysis. In: International conference on theory and applications of satisfiability testing (SAT), pp 21–27
Audemard G, Lagniez JM, Mazure B, Saï L (2009) Learning in local search. In: 21st International conference on tools with artificial intelligence (ICTAI’09). IEEE Computer Society, Newark, New Jersey, USA
Audemard G, Katsirelos G, Simon L (2010) A restriction of extended resolution for clause learning SAT solvers. In: 24th conference on artificial intelligence (AAAI), pp 15–20
Audemard G, Lagniez JM, Simon L (2013) Just-in-time compilation of knowledge bases. In: Proceedings of the twenty-third international joint conference on artificial intelligence (IJCAI), pp 447–453
Audemard GA, Lagniez JM, Szczepanski N, Tabary S (2017) A distributed version of syrup. In: International conference on theory and applications of satisfiability testing (SAT)
Bacchus F, Winter J (2003) Effective preprocessing with hyper-resolution and equality reduction. In: SAT’2003, pp 341–355
Biere A (2006) AIGER format toolbox. http://fmv.jku.at/aiger/
Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDS
Biere A, Heule M, Van Maaren H, Walsh T (eds) (2009) Handbook of satisfiability. IOS Press, Amsterdam
Biere A, Lonsing F, Seidl M (2011) Blocked clause elimination for QBF. In: International conference on automated deduction. Springer, pp 101–115
Bova S (2016) Sdds are exponentially more succinct than OBDDS. In: Proceedings of the national conference on artificial intelligence (AAAI), pp 929–935
Bova S, Capelli F, Mengel S, Slivovsky F (2015) On compiling CNFs into structured deterministic DNNFs. In: International conference on theory and applications of satisfiability testing (SAT), pp 199–214
Bradley AR (2011) SAT-based model checking without unrolling. In: Verification, model checking, and abstract interpretation (VMCAI), pp 70–87
Braunstein A, Mézard M, Zecchina R (2002) Survey propagation: an algorithm for satisfiability. Technical report
Bryant R (1986) Graph - based algorithms for boolean function manipulation. IEEE Trans Comput 35(8):677–691
Büning HK, Karpinski M, Flögel A (1995) Resolution for quantified boolean formulas. Inf Comput 117(1):12–18
Buro M, Büning HK (1993) Report on a SAT competition. Bull Eur Assoc Theor Comput Sci 49:143–151
Cadoli M, Donini M (1997) A survey on knowledge compilation. AI Commun 10:137–150
Cadoli M, Giovanardi A, Schaerf M (1998) An algorithm to evaluate quantified boolean formulae. In: Proceedings of the fifteenth national/tenth conference on artificial intelligence/innovative applications of artificial intelligence, AAAI ’98/IAAI ’98, pp 262–267
Cadoli M, Schaerf M, Giovanardi A, Giovanardi M (1999) An algorithm to evaluate quantified boolean formulae and its experimental evaluation. In: Journal of automated reasoning. AAAI Press, pp 262–267
Cashmore M, Fox M, Giunchiglia E (2012) Planning as quantified boolean formula. In: ECAI 2012 - 20th European conference on artificial intelligence, pp 217–222
Castell T, Cayrol C, Cayrol M, Le Berre D (1996) Using the Davis and Putnam procedure for an efficient computation of preferred models. In: ECAI, vol 96. Pitman, pp 350–354
Chambers B, Manolios P, Vroon D (2009) Faster sat solving with better CNF generation. In: DATE
Chang CL, Lee RC (1973) Symbolic logic and mechanical theorem proving. Computer science classics. Academic Press, London
Chazal G (1996) Éléments de logique formelle. Hermès
Choi A, Zaitlen N, Han B, Pipatsrisawat K, Darwiche A, Eskin E (2008) Efficient genome wide tagging by reduction to SAT. In: Crandall K, Lagergren J (eds) Algorithms in bioinformatics, vol 5251. Lecture notes in computer science. Springer, Berlin/Heidelberg, pp 135–147
Chvátal V, Szemerédi E (1988) Many hard examples for resolution. J ACM 35:759–768
Coja-Oghlan A, Panagiotou K (2016) The asymptotic k-SAT threshold. Adv Math 288:985–1068
Cook S (1971) The complexity of theorem proving procedures. In: ACM symposium of theory of computing, pp 151–158
Cook SA (1976) A short proof of the pigeon hole principle using extended resolution. Sigact News 28–32
Coste-Marquis S, Fargier H, Lang J, Berre DL, Marquis P (2006) Representing policies for quantified boolean formulae. In: KR, pp 286–297
Coudert O, Madre JC (1992) Implicit and incremental computation of primes and essential implicant primes of boolean functions. In: 29th ACM/IEEE design automation conference (DAC’92), pp 36–39
Darwiche A (2011) SDD: a new canonical representation of propositional knowledge bases. In: Proceedings of the twenty-second international joint conference on artificial intelligence (IJCAI), pp 819–826
Darwiche A, Marquis P (2001) A perspective on knowledge compilation. In: Proceedings of the 17th international joint conference on artificial intelligence (IJCAI’01), pp 175–182
Davis M, Putnam H (1960) A computing procedure for quantification theory. JACM 7:201–215
Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. JACM 5:394–397
De Kleer J (1989) A comparison of ATMS and CSP techniques. In: IJCAI’89: proceedings of the 11th international joint conference on artificial intelligence. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, pp 290–296
de Kleer J (1992) An improved incremental algorithm for generating prime implicates. In: Proceedings of the national conference on artificial intelligence (AAAI’92), pp 780–7085
de Kleer J, Williams BC (1987) Diagnosing multiple faults. Artif Intell 32(1):97–130
de Kleer J, Mackworth AK, Reiter R (1992) Characterizing diagnoses and sytems. Artif Intell 56:197–222
del Val A (1994) Tractable databases: how to make propositional unit resolution complete through compilation. In: 4th International conference on principles of knowledge representation and reasoning (KR’94), Bonn, pp 551–561
del Val A (1999) A new method for consequence finding and compilation in restricted languages. In: 16th National conference on artificial intelligence (AAAI’99), pp 259–264
Dechter R, Rish I (1994) Directional resolution: the Davis-Putnam procedure. In: Proceedings of the 4th international conference on principles of KR & R, pp 134–145
Dimacs (1993) Second challenge on satisfiability testing organized by the center for discrete mathematics and computer science of Rutgers university
Dowling W, Gallier J (1984) Linear-time algorithms for testing the satisfiability of propositional horn formulae. J Log Program 1(3):267–284
Doyle J (1979) A truth maintenance system. AI 12(3):251–272
Dubois O, Dequen G (2001) A backbone-search heuristic for efficient solving of hard 3-sat formulae. In: Proceedings of IJCAI’2001, pp 248–253
Eén N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: proceedings of SAT, pp 61–75
Eén N, Sörenson N (2003) An extensible sat-solver. In: SAT’2003, pp 333–336
Feige U (2002) Relations between average case complexity and approximation complexity. In: Proceedings of the 34th ACM symposium on theory of computing, pp 534–543
Fossé R, Simon L (2018) On the non-degeneracy of unsatisfiability proof graphs produced by sat solvers
Franco J (1986) On the probabilistic performance of algorithms for the satisfiability problem. Inf Process Lett 23:103–106
Galil Z (1977) On the complexity of regular resolution and the Davis-Putnam procedure. Theor Comput Sci 4:23–46
Garey M, Johnson D (1979) Computers and intractability: a guide to the theory of NP-completeness. W.H. Freeman and Company, New York
Giunchiglia F, Sebastiani R (1996) Building decision procedures for modal logics from propositional decision procedure - the case study of modal k. In: Conference on automated deduction, pp 583–597
Giunchiglia E, Narizzano M, Tacchella A (2001) Qube: a system for deciding quantified boolean formulas satisfiability. In: Proceedings of the first international joint conference on automated reasoning, pp 364–369
Giunchiglia E, Narizzano M, Tacchella A (2003) Backjumping for quantified boolean logic satisfiability. Artif Intell 145(1–2):99–120
Giunchiglia E, Narizzano M, Tacchella A, (2004) Monotone literals and learning in QBF reasoning. In: Principles and practice of constraint programming - CP 2004. Lecture notes in computer science, vol 3258. Springer, Berlin, Heidelberg, pp 260–273
Giunchiglia E, Narizzano M, Tacchella A (2006) Clause/term resolution and learning in the evaluation of quantified boolean formulas. J Artif Int Res 26(1):371–416
Goldberg A (1979) On the complexity of the satisfiability problem. Technical report 16, New York University
Goldberg A, Purdom JP, Brown C (1982) Average time analysis of simplified Davis-Putnam procedures. Inf Process Lett 72–75
Grégoire É, Mazure B, Ostrowski R, Saï L (2005) Automatic extraction of functional dependencies. In: Theory and applications of satisfiability testing: 7th international conference (SAT 2004), Revised selected papers (SAT’04 Revised selected papers), LNCS, vol 3542, pp 122–132
Habet D, Li CM, Devendeville L, Vasquez M (2002) A hybrid approach for sat. In: CP ’02: proceedings of the 8th international conference on principles and practice of constraint programming. Springer-Verlag, London, UK, pp 172–184
Haken A (1985) The intractability of resolution. Theor Comput Sci 39:297–308
Hamadi Y, Jabbour S, Sais L (2009) ManySAT: a parallel SAT solver. J Satisf Boolean Model Comput (JSAT)
Heule MJ (2017) Schur number five. arXiv:171108076
Heule MJ (2018) Computing small unit-distance graphs with chromatic number 5. arXiv:180512181
Heule MJ, Kullmann O (2017) The science of brute force. Commun ACM 60(8):70–79
Heule M, Van Maaren H (2007) Effective incorporation of double look-ahead procedures. In: SAT’07: proceedings of the 10th international conference on theory and applications of satisfiability testing. Springer-Verlag, Berlin, Heidelberg, pp 258–271
Heule M, Hunt JW, Wetzler N (2013) Trimming while checking clausal proofs. In: Formal methods in computer-aided design (FMCAD), pp 181–188
Heule MJ, Kullmann O, Marek VW (2016) Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In: International conference on theory and applications of satisfiability testing. Springer, pp 228–245
Heule MJ, Seidl M, Biere A (2017) Solution validation and extraction for QBF preprocessing. J Autom Reason 58(1):97–125
Hirsch EA, Kojevnikov A (2005) Unitwalk: a new sat solver that uses local search guided by unit clause elimination. Ann Math Artif Intell 43(1–4):91–111
Hoos H, Stützle T (2004) Stochastic local search: foundations and applications. Morgan Kaufmann/Elsevier
Huang J (2007) The effect of restarts on the efficiency of clause learning. In: IJCAI’2007, pp 2318–2323
Jackson P, Sheridan D (2004) Clause form conversions for boolean circuits. In: SAT, pp 183–198
Janota M, Klieber W, Marques-Silva J, Clarke E (2016) Solving QBF with counterexample guided refinement. Artif Intell 234:1–25
Järvisalo M, Biere A, Heule M (2010) Blocked clause elimination. In: TACAS, pp 129–144
Järvisalo M, Heule MJH, Biere A (2012) Inprocessing rules, pp 355–370
Jeroslow R, Wang J (1990) Solving propositional satisfiability problems. Ann Math Artif Intell 167–187
Katebi H, Sakallah KA, Markov IL (2010) Symmetry and satisfiability: an update. In: SAT, pp 113–127
Kautz H, Selman B (1996) Pushing the envelope : planning, propositional logic, and stochastic search. In: Proceedings of the twelfth national conference on artificial intelligence (AAAI’96), pp 1194–1201
Kautz H, Selman B (2003) Ten challenges Redux: recent progress in propositional reasoning and search. In: Proceedings of CP ’03, pp 1–18
Kean A, Tsiknis G (1990) An incremental method for generating prime implicants/implicates. J Symb Comput 9(185):206
Kernighan BW, Lin S (1970) An efficient heuristic procedure for partitioning graphs. Bell Syst Tech J 49(2):291–307
Konev B, Lisitsa A (2014) A SAT attack on the erdős discrepancy problem. In: International conference on theory and applications of satisfiability testing (SAT)
Koriche F, Lagniez J-M, Marquis P, Thomas S (2013) Affine decision trees for model counting. In: Proceedings of the 23rd international joint conference on artificial intelligence (IJCAI), pp 947–953
Kottler S (2010) Sat solving with reference points. SAT 2010:143–157
Kroc L, Sabharwal A, Selman B (2007) Survey propagation revisited. In: UAI, pp 217–226
Kroc L, Sabharwal A, Selman B (2010) An empirical study of optimal noise and runtime distributions in local search. In: SAT’10
Kullmann O (1999) On a generalization of extended resolution. Discret Appl Math 96–97:149–176
Lardeux F, Saubion F, Hao JK (2006) Gasat: a genetic local search algorithm for the satisfiability problem. Evol Comput 14(2):223–253. https://doi.org/10.1162/evco.2006.14.2.223
Lassaigne R, de Rougemont M (1996) Logique et complexité. Hermés, collection informatique
Le Berre D (2000) Autour de SAT : le calcul d’impiquants p-restreints, algorithmes et applications. PhD thesis, Université Toulouse III - Paul Sabatier
Le Berre D (2001) Exploiting the real power of unit propagation lookahead. Electron Notes Discret Math 9:59–80
Le Berre D, Roussel O (2002–2009) The SAT competitions (2002–2009). www.satcompetition.org
LeBerre D, Simon L (eds) (2006) Special volume on the SAT 2005 competitions and evaluations. J Satisf Boolean Model Comput 2
Le Berre D, Roussel O, Simon L (2009) SAT competition. http://www.satcompetition.org/
Letz R (2002) Lemma and model caching in decision procedures for quantified boolean formulas. In: Proceedings of the international conference on automated reasoning with analytic tableaux and related methods, pp 160–175
Li CM, Anbulagan A (1997) Heuristics based on unit propagation for satisfiability problems. In: Proceedings of IJCAI’97, pp 366–371
Liang JH, Poupart P, Czarnecki K, Ganesh V (2017) An empirical study of branching heuristics through the lens of global learning rate. In: International conference on theory and applications of satisfiability testing, pp 119–135
Luby M, Sinclair A, Zuckerman D (1993) Optimal speedup of Las Vegas algorithms. Inf Process Lett 47(4):173–180
Luo M, Li CM, Xiao F, Manya F, Lu Z (2017) An effective learnt clause minimization approach for CDCL SAT solvers. In: Twenty-sixth international joint conference on artificial intelligence (IJCAI)
Madre JC, Coudert O (1991) A logically complete reasoning maintenance system based on a logical constraint solver. In: 12th international joint conference on artificial intelligence (IJCAI’91), Australia, Sydney, pp 294–299
Marquis P (1999) Handbook of defeasible reasoning and uncertainty management systems, vol 5, Chapter consequence finding algorithms. Kluwer Academic Publishers, pp 41–145
Mazure B, Sais L, Gregoire E (1997) Tabu search for sat. In: Proceedings of AAAI, pp 281–285
Mazure B, Saïs L, Grégoire E (1998) Boosting complete techniques thanks to local search methods. Ann Math Artif Intell 22(3–4):319–331. https://doi.org/10.1023/A:1018999721141
McMillan K (2003) Interpolation and SAT-based model checking. In: International conference on computer-aided verification (CAV), pp 1–13
Mitchell D, Selman B, Levesque H (1992) Hard and easy distributions of sat problems. In: Proceedings of the national conference on artificial intelligence (AAAI’92), pp 459–465
Monasson R, Zecchina R, Kirkpatrick S, Selman B, Troyansky L (1998) Determining computational complexity from characteristic phase transition. Nature 400:133–137
Moskewicz M, Conor C, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th design automation conference (DAC’01)
Newsham Z, Ganesh V, Fischmeister S, Audemard G, Simon L (2014) Impact of community structure on SAT solver performance. In: International conference on theory and applications of satisfiability testing (SAT), pp 252–268
Oh C (2015) Between SAT and UNSAT: the fundamental difference in CDCL SAT. In: Theory and applications of satisfiability testing (SAT), pp 307–323
Ostrowski R, Grégoire E, Mazure B, Saï L (2002) Recovering and exploiting structural knowledge from CNF formulas. In: CP’02
Pan G, Vardi MY (2004) Symbolic decision procedures for QBF. In: Proceedings of 10th international conference on principles and practice of constraint programming (CP 2004). Springer, pp 453–467
Pearl J (1982) Reverend bayes on inference engines: a distributed hierarchical approach. In: AAAI’82, pp 133–136
Peitl T, Slivovsky F, Szeider S (2017) Dependency learning for QBF. In: International conference on theory and applications of satisfiability testing (SAT)
Pham DN, Thornton J, Sattar A (2007) Building structure into local search for sat. In: IJCAI’07
Piette C, Hamadi Y, Saïs L (2008) Vivifying propositional clausal formulae. In: European conference on artificial intelligence (ECAI), pp 525–529
Pipatsrisawat K, Darwiche A (2007) A lightweight component caching scheme for satisfiability solvers. In: proceedings of SAT, pp 294–299
Pipatsrisawat K, Darwiche A (2009) On the power of clause-learning SAT solvers with restarts. In: Principles and practice of constraint programming - CP 2009
Plaisted D, Greenbaum S (1986) A structure-preserving clause form translation. J Symb Comput 2(3):466–483
Prasad M, Biere A, Gupta A (2005) A survey of recent advances in SAT-based formal verification. J Softw Tools Technol Transf 7(2):156–173
Quine W (1955) A way to simplify truth functions. Am Math Mon 52:627–631
Reiter R (1987) A theory of diagnosis from first principles. Artif Intell 32(1):57–96
Reiter R, de Kleer J (1987) Foundations of assumption-based truth maintenance systems: preliminary report. In: Proceedings of the sixth national conference on artificial intelligence (AAAI’87), pp 183–188
Rintanen J (1999) Improvements to the evaluation of quantified boolean formulae. In: Proceedings of the 16th international joint conference on artificial intelligence - volume 2, pp 1192–1197
Rish I, Dechter R (2000) Resolution versus search: two strategies for sat. J Approx Reason
Robinson J (1965) A machine oriented based on the resolution principle. J ACM 12(1):23–41
Safarpour S, Mangassarian H, Veneris A, Liffiton MH, Sakallah KA (2007) Improved design debugging using maximum satisfiability. In: FMCAD ’07: proceedings of the formal methods in computer aided design. IEEE Computer Society, pp 13–19
Saïs L (ed) (2008) Probléme SAT : progrés et défis. Hermés / Lavoisier
Selman B, Kautz H (1993) Domain-independant extensions to GSAT: solving large structured satisfiability problems. In: Proceedings of the international joint conference on artificial intelligence (IJCAI’93), pp 290–295
Selman B, Kautz H (1996) Knowledge compilation and theory approximation. J ACM 43(2):193–224
Selman B, Levesque H, Mitchell D (1992) A new method for solving hard satisfiability problems. In: AAAI, pp 440–446
Selman B, Kautz H, Cohen B (1995) Local search strategies for satisfiability testing. In: DIMACS series in discrete mathematics and theoretical computer science, pp 521–532
Selman B, Kautz H, Mcallester D (1997) Ten challenges in propositional reasoning and search. Morgan Kaufmann, San Francisco, pp 50–54
Shostak R (1979) A practical decision procedure for arithmetic with function symbols. J ACM 26(2):351–360
Siegel P (1987) Représentation et utilisation de la connaissance en calcul propositionnel. Université de Provence, GIA-Luminy, Thèse d’état
Silva JPM, Sakallah KA (1996) Grasp a new search algorithm for satisfiability. In: ICCAD ’96: proceedings of the 1996 IEEE/ACM international conference on computer-aided design. IEEE Computer Society, Washington, DC, USA, pp 220–227
Simon L (2001) Multirésolution pour le test de consistance et la déduction en logique propositionnelle. PhD thesis, Université Orsay Paris XI
Simon L, del Val A (2001) Efficient consequence finding. In: 17th international joint conference on artificial intelligence (IJCAI’01), Seattle, Washington, USA, pp 359–365
Stålmarck G (1994) A system for determining propositional logic theorem by applying values and rules to triplets that are generated from a formula, US Patent 5,276,897; Canadian Patent 2,018,828; European Patent 0 403 545; Swedish Patent 467 076
Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time. In: Proceedings of the fifth annual ACM symposium on theory of computing, ACM, New York, NY, USA, STOC ’73, pp 1–9
Subbarayan S, Bordeaux L, Hamadi Y (2007) Knowledge compilation properties of tree-of-BDDs. In: AAAI’07
Tison P (1967) Generalized consensus theory and application to the minimization of boolean circuits. In: IEEE transactions on computers, vol EC-16, pp 446–456
Tompkins DAD, Hoos HH (2004) UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: SAT, pp 37–46
Tseitin G (1968) Structures in constructives mathematics and mathematical logic, A.O. Slesenko, chap on the complexity of derivations in the propositional calculus, pp 115–125
Tseitin G (1983) On the complexity of proofs in propositional logics. In: Siekmann J, Wrightson G (eds) Automation of reasoning: classical papers in computational logic 1967–1970, vol 2. Springer, Berlin
Val A (2000) Tractable classes for directional resolution. In: Proceedings of the 17th (U.S.) National conference on artificial intelligence
Velev MN (2004) Efficient translation of boolean formulas to CNF in formal verification of microprocessors. In: ASP-DAC ’04: proceedings of the 2004 Asia and South Pacific design automation conference, pp 310–315
Woeginger GJ (2003) Exact algorithms for np-hard problems: a survey. In: Combinatorial optimization, pp 185–207
Zhang H (1997) SATO: an efficient propositional prover. In: Proceedings of the international conference on automated deduction (CADE’97), volume 1249 of LNAI, pp 272–275
Zhang L, Malik S (2002) Towards a symmetric treatment of satisfaction and conflicts in quantified boolean formula evaluation. In: Proceedings of the 8th international conference on principles and practice of constraint programming, pp 200–215
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Simon, L. (2020). Reasoning with Propositional Logic: From SAT Solvers to Knowledge Compilation. In: Marquis, P., Papini, O., Prade, H. (eds) A Guided Tour of Artificial Intelligence Research. Springer, Cham. https://doi.org/10.1007/978-3-030-06167-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-06167-8_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-06166-1
Online ISBN: 978-3-030-06167-8
eBook Packages: Intelligent Technologies and RoboticsIntelligent Technologies and Robotics (R0)