Transcript ppt - CSE
Challenges for SAT and QBF Prof. Toby Walsh Cork Constraint Computation Centre University College Cork Ireland www.4c.ucc.ie/~tw Thanks • • • • • Ian Gent Joao Marques-Silva Ines Lynce Steve Prestwich … Every morning … I cycle across the River Lee … And see this rather drab house … Every morning … I read the plaque on the wall of this house … Dedicated to the memory of George Boole … Professor of Mathematics at Queens College (now University College Cork) George Boole (1815-1864) • Boolean algebra The Mathematical Analysis of Logic, Cambridge, 1847 The Calculus of Logic, Cambridge and Dublin Mathematical journal, vol. 3, 1948 • Essentially reduced propositional logic to algebraic manipulations George Boole (1815-1864) • Boolean algebra The Mathematical Analysis of Logic, Cambridge, 1847 The Calculus of Logic, Cambridge and Dublin Mathematical journal, vol. 3, 1948 • Essentially reduced propositional logic to algebraic manipulations Cork Constraint Computation Center University College Cork • Generously funded by SFI, EI, Xerox, EU, .. • • ~20 staff • • • Still hiring Active visitor’s programme Researching all areas of constraint programming • • • • €8M for initial 5 years Satisfiability Modelling Uncertainty Hosting • • • CP-2003 IJCAR-2004 SAT-2005 Outline • What is a challenge? • Why do we need them? • What are my 10 challenges? • Financial • Technological • Social What is a challenge? Perhaps even what is a grand challenge? What is a Grand Challenge? • Prove P=NP • open • Develop world class chess program • completed, 1990s • Translate Russian into English • failed, 1960s UK Computing Research Committee’s workshop on “Grand Challenges for CS”, November 2002 Follow on to US Computing Research Association’s conference on “Grand Challenges”, June 2002 What is a Grand Challenge? • Scale • It arises from scientific curiosity about the foundation, the nature or the limits of the discipline. • It gives scope for engineering ambition to build something that has never been seen before. • It promises to go beyond what is initially possible, and requires development of understanding, techniques and tools unknown at the start of the project. • Appeal • It has enthusiastic support from (almost) the entire research community, even those who do not participate or benefit from it. • It has international scope: participation would increase the research profile of a nation. • It is generally comprehensible, and captures the imagination of the general public, as well as the esteem of scientists in other disciplines. What is a Grand Challenge? • Measurable • It will be obvious how far and when the challenge has been met (or not). • It encourages and benefits from competition among individuals and teams, with clear criteria on who is winning, or who has won. • Benefits • It decomposes into identified intermediate research goals, whose achievement brings scientific or economic benefit, even if the project as a whole fails. • It will lead to radical paradigm shift, breaking free from the dead hand of legacy CologNet’s role • EU Network of Excellence • Born out of Compulog • Promote logic • • • • Logic & Agents Logic & Databases .. Automated Reasoning • Identify grand challenges within AR Top Ten Challenges • Problems • 700 var, random 3SAT • 32bit parity problem • Proof systems • Better proof system than resolution • Solve SAT via IP • Local search • UNSAT local search procedure • Variable dependencies • Hybrid solver better than best complete or local solver • Encodings • Characterize props of real world encodings • Develop robust encodings • Develop realistic problem generators [Selman, Kautz, McAllester, IJCAI97] Top Ten Challenges • Problems • 700 var, random 3SAT • 32bit parity problem • Proof systems • Better proof system than resolution • Solve SAT via IP • Local search • UNSAT local search procedure • Variable dependencies • Hybrid solver better than best complete or local solver • Encodings • Characterize props of real world encodings • Develop robust encodings • Develop realistic problem generators [Selman, Kautz, McAllester, IJCAI97] Why do we need some challenges? At this point in time Why do we need some challenges? • Two arguments • Arguments based on • Moore’s law • Solver’s topping out Moore’s Law 500 400 300 200 100 0 Number of vars '92 '96 '00 • Are we keeping up with Moore’s law? • Number of transistors doubles every 18 months • Number of variables reported in random 3SAT experiments doubles every 3 or 4 years Moore’s Law 500 400 300 200 100 0 Number of vars '92 '96 '00 • Are we keeping up with Moore’s law? • Number of transistors doubles every 18 months • Number of variables reported in random 3SAT experiments doubles every 3 or 4 years We’re falling behind each year! Even though we’re getting better performance due to Moore’s law! Brief History of DP • 1st generation (1950s) • DP, DLL • 2nd generation (1980s/90s) • POSIT, Tableau, CSAT, … • 3rd generation (mid 1990s) • SATO, satz, grasp, … • 4th generation (2000s) • Chaff, BerkMin, forklift, … Actual Japanese 5th Generation Computer (from FGC Museum archive) • 5th generation? Brief History of DP • 1st generation (1950s) • DP, DLL • 2nd generation (1980s/90s) • POSIT, Tableau, CSAT, … • 3rd generation (mid 1990s) • SATO, satz, grasp, … • 4th generation (2000s) • Chaff, BerkMin, forklift, … Actual Japanese 5th Generation Computer (from FGC Museum archive) • 5th generation? • Will it need a paradigm shift? What are my 10 challenges? Financial Technological Social SAT industry v CSP industry • Producers • Prover Technology, … • Producers/Consumers • CADENCE, … • Consumers • Intel, … • Industries • Formal verification SAT industry v CSP industry • Producers • ILOG • Parc Technologies • .. • Producers/Consumers • Bouygues, … • Consumers • I2, SAP, Oracle, … • Industries • Scheduling, Transportation, Telecommunications, Supply Chain, … Challenge 1: new practical applications • Can we develop new & practical applications for SAT? • Aside from verification • Possible areas • Timetabling • Crew rostering • Scheduling • Network management • Cryptography … Challenge 2: embedded SAT solvers • Can we get SAT engines embedded in mainstream business tools? • Just as constraint tools are found within, for example, supply chain management software Other financial challenges • Many other financial challenges • Is there any reason why SAT cannot be as large an industry as constraint programming? • Can SAT solvers be shrink-wrapped? • … What are my 10 challenges? Financial Technological Social SAT research v CSP research • SAT solvers go back more than 40 years • Davis and Putnam, A computing procedure for quantification theory, JACM, 1960 • Gilmore, A proof method for quantification theory, IBM J. on Res. & Dev., 1960 • Davis, Logemann and Loveland, A machine program for theoremproving, CACM, 1962 • CSP solvers go back slightly less, perhaps only 30 years • Fikes, REF-ARF, Artificial Intelligence, 1970 • D. Waltz’s PhD thesis, MIT AI Lab, 1972 • U. Montanari, Networks of Constraints, Information Science, 1974 SAT research v CSP research • SAT solvers go back more than 40 years • Davis and Putnam, A computing procedure for quantification theory, JACM, 1960 • Gilmore, A proof method for quantification theory, IBM J. on Res. & Dev., 1960 • Davis, Logemann and Loveland, A machine program for theoremproving, CACM, 1962 • CSP solvers go back slightly less, perhaps only 30 years • Fikes, REF-ARF, Artificial Intelligence, 1970 • D. Waltz’s PhD thesis, MIT AI Lab, 1972 • U. Montanari, Networks of Constraints, Information Science, 1974 SAT solvers v CSP solvers • Tree search • Intelligent backtracking • Clause learning • Fast inference • Unit propagation • Resolution • Constraint language • Flat clauses SAT solvers v CSP solvers • Tree search • Intelligent backtracking • Clause learning • Fast inference • Tree search • Chronological backtracking • No learning • Fast inference • Unit propagation • Resolution • Arc-consistency • Specialized propagators • Constraint language • Constraint language • Flat clauses • Rich, modelling languages SAT solvers v CSP solvers • Tree search • Intelligent backtracking • Clause learning • Fast inference • Tree search • Chronological backtracking • No learning • Fast inference • Unit propagation • Resolution • Arc-consistency • Specialized propagators • Constraint language • Constraint language • Flat clauses • Rich, modelling languages SAT solvers v CSP solvers • Tree search • Intelligent backtracking • Clause learning • Fast inference • Tree search • Chronological backtracking • No learning • Fast inference • Unit propagation • Resolution • Arc-consistency • Specialized propagators • Constraint language • Constraint language • Flat clauses • Rich, modelling languages Challenge 3: non-clausal SAT solving • Can we extend our best SAT solvers to deal with non-clausal SAT? • Specifications not naturally in CNF? • Structure more apparent in unflattened fomulae • Solvers should be able to exploit this structure? Challenge 4: SAT modelling languages • Can we develop richer modelling languages for SAT solvers? • Let’s not stop with nonclausal formulae • Curse of DIMACS • We can only develop solvers so far • Then will need to focus on modelling • 3 most important parts of AI • Representation, representation, representation. p cnf 100 430 12 -31 44 0 55 27 -76 0 -21 52 84 0 SAT modelling languages • Desirable extensions • • • • Arithmetic Multiple values Global constraints … • Extend solver • Linear 0/1 inequalities • Arithmetic reasoner • … • Encode back into SAT • Efficient ways to encode arithmetic • … Challenge 5: specialized propagators • Can we effectively incorporate specialized propagators in SAT solvers? • Integral to success of constraint programming • Global constraints for all-different, cardinality, capacity, ordering, … • Need richer models! Challenge 6: learning via SAT • Can we add learning to commercial constraint toolkits via SAT solving? • At dead-end during constraint solving • No-good identified Not(X=2 & Y=1 & …) • Represent and reason with such no-goods via SAT subtheory -X2 v -Y1 v … Challenge 7: symmetry & SAT • Can we develop effective SAT solvers that factor out symmetry? • Currently very active area in constraint programming • Even more symmetry in SAT than CP? • How do we find the symmetries? • Again, the curse of DIMACS • Often very explicit in modelling problem Challenge 8: Connect 4 via QBF • Can we solve Connect 4 via QBF? • I promised some QBF challenges • Connnect 4 encodes into QBF directly • Alternating move order • Fixed game depth • Perfect branching heuristic known Other technological challenges • Many other technological challenges • Do improvements in solving random 3SAT help us solve real world problems? • When is more inference useful? • … What are my 10 challenges? Financial Technological Social What are social challenges? • Challenges in developing research field • • • • Sharing of intellectual property Conferences Competitions … Challenge 9: engaging other fields • Can SAT engage the interest of new research areas? • Already some interaction with • Constraint programming • Statistical mechanics • Formal methods • But what about • • • • Cryptography Coding theory Design theory … Intellectual property • Universities are becoming very aware of the “value” of research IP • Companies have protected their IP for some time • University of York (my old institution) just taken out their first software patent • Constraint propagation algorithm I helped develop • My biggest head-ache ever Challenge 10: surving software patents • Can SAT research progress unhindered by software patents? • Requires debate • Patents are supposed to encourage disclosure • Already don’t know how some SAT solvers really work Other social challenges • Many other social challenges • How do we evolve the SAT competition to maximize progress in field? • How do we attract new blood to SAT? • … The 10 Challenges 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. New pracical applications Embedded SAT solvers Non-clausal SAT solvers SAT modelling languages Specialized propagators Learning via SAT Symmetry & SAT Connect 4 via QBF Engaging other fields Surviving software patents Final remarks • Useful to consider challenges • Hope to stimulate some debate • For more debate • Come to Miami in July for CADE conference • “Challenges for Automated Reasoning” workshop • Travel grants available from CologNet