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
Descargar

Challenges for SAT and QBF