The Linear-Input Strategy Backtracks

• All centre clauses FALSE in models of the side clauses

  

• Have to identify potential side clauses

• Complete for only Horn clauses