CSSCPA Design

CSSCPA and the FLi

• Problems in TPTP CNF syntax
• Components must output logical consequences to stdout
• Employs a formula librarian (the FLi)
• Modus operandi
  • Save problem in FLi
  • Choose components based on expected performance
  • Run components in competition parallel
    • Stop if a solution is found
  • Parse components outputs for logical consequences
  • FLi accumulates logical consequences that improve things
    • Total and average clause weight
    • Minimal deltas
  • Restart when FLi's problem is significantly easier
• Output improved problem files and component proof
  • Sufficient information to build a monolithic proof

Iterative easing

• Creates a sequence of easier problems
• Is sound in principle
• On the macro level, is cooperative time-slicing