squeeze_simp 3SAT

Stream: general

[Kevin Buzzard]

import tactic

example : ∀ P Q R S U : bool, bnot (
  (Q || P || U) && (U || ¬Q || S) && (U || Q || ¬R) && (P || R || ¬S) &&
  (P || S || R) && (R || ¬U || Q) && (R || S || ¬U) && (¬S || ¬R || U) &&
  (U || ¬Q || ¬R) && (¬Q || U || ¬S) && (¬P || ¬R || Q) && (S || ¬U || ¬P) &&
  (¬R || ¬P || U) && (S || ¬R || ¬U) && (¬R || ¬Q || ¬S) && (Q || R || S) &&
  (¬U || P || ¬Q) && (R || ¬Q || ¬P) && (P || R || ¬Q) && (S || P || Q) &&
  (R || P || U) && (¬U || Q || R) && (¬U || R || ¬Q) && (¬S || ¬U || ¬Q) &&
  (¬U || ¬S || R) && (¬S || P || U) && (P || Q || ¬R) && (¬S || ¬R || U) &&
  (¬Q || ¬S || U) && (P || R || ¬Q) && (P || Q || ¬S) && (U || ¬S || ¬P) &&
  (¬U || R || ¬P) && (¬U || P || ¬Q) && (¬R || ¬P || S) && (R || S || ¬U) &&
  (P || ¬U || Q) && (¬S || R || P) && (¬P || ¬Q || ¬R) && (¬P || R || ¬S)) :=
begin
  -- squeeze_simp, -- hangs?
  simp, -- works
end

AITP making me think about 3SAT. squeeze_simp can't tell me how simp did it.

[Kevin Buzzard]

PS I've never used bool before.

[Kevin Buzzard]

Same behaviour for ∀ P Q R S U : bool, ff = (

[Kevin Buzzard]

Independent of this, can anyone give me an easy way to change a DIMACS (or whatever it's called) file (as for example output by toughsat) into a Lean file of either the above form or the analogous Prop form?

[Kevin Buzzard]

I'm trying to set a good example sheet question

[Marc Huisinga]

here's a quick terrible hack that probably does what you want:

import sys
import itertools
with open(sys.argv[1], "r") as f:
  clauses = [[int(x) for x in c.split(" ")[:-1]] for c in f.readlines() if c[0] != 'c' and c[0] != 'p']
  print("∀ %s : bool, %s" %
    (" ".join("x%d" % x for x in {abs(x) for x in itertools.chain.from_iterable(clauses)}),
     " && ".join("(%s)" % " || ".join("x%d" % x if x > 0 else "¬x%d" % -x for x in c) for c in clauses)))

[Sebastien Gouezel]

squeeze_simp can be very slow (quadratic in the number of lemmas it uses?), so maybe leave it alone for 10 minutes and see what comes out of it?

[Simon Hudon]

@Sebastien Gouezel That's right. It might be worth adding a flag to make it faster. It gets slow because, once it has a simp list, it tries to prune the lemmas that don't contribute to the proof. If we don't try to minimize, it gets faster.

[Kevin Buzzard]

Oh lol I've just realised the nots should be !s :-)

[Kevin Buzzard]

I'm such a boolnoob

[Minchao Wu]

@Kevin Buzzard Just a quick note, for these examples simp is overkilling, in fact, you don't need to import tactic

import data.bool

theorem foo : ∀ P Q R S U : bool, bnot (
  (Q || P || U) && (U || ¬Q || S) && (U || Q || ¬R) && (P || R || ¬S) &&
  (P || S || R) && (R || ¬U || Q) && (R || S || ¬U) && (¬S || ¬R || U) &&
  (U || ¬Q || ¬R) && (¬Q || U || ¬S) && (¬P || ¬R || Q) && (S || ¬U || ¬P) &&
  (¬R || ¬P || U) && (S || ¬R || ¬U) && (¬R || ¬Q || ¬S) && (Q || R || S) &&
  (¬U || P || ¬Q) && (R || ¬Q || ¬P) && (P || R || ¬Q) && (S || P || Q) &&
  (R || P || U) && (¬U || Q || R) && (¬U || R || ¬Q) && (¬S || ¬U || ¬Q) &&
  (¬U || ¬S || R) && (¬S || P || U) && (P || Q || ¬R) && (¬S || ¬R || U) &&
  (¬Q || ¬S || U) && (P || R || ¬Q) && (P || Q || ¬S) && (U || ¬S || ¬P) &&
  (¬U || R || ¬P) && (¬U || P || ¬Q) && (¬R || ¬P || S) && (R || S || ¬U) &&
  (P || ¬U || Q) && (¬S || R || P) && (¬P || ¬Q || ¬R) && (¬P || R || ¬S)) :=
dec_trivial

[Kevin Buzzard]

Thanks. Marijn Heule sent me this: https://www.cs.utexas.edu/~marijn/game/

[Johan Commelin]

That game is really annoying

[Reid Barton]

I won!

[Alex J. Best]

Me too! I used an "algorithm" of click until the board is completely coloured, then repeatedly find a triple of reds, and double click a random one of those 3. I'm curious if that procedure has a name in 3-sat literature.

[Kenny Lau]

related: https://en.wikipedia.org/wiki/Bogosort

[Alex J. Best]

Hahah I think the bogosort analogue would be more like, pick a random assignment, assign everything check for SAT, unassign everything, repeat. Perhaps my approach is the Bozosort analogue?!

[Marc Huisinga]

GSAT might be fitting!

[Mario Carneiro]

Actually, random assignment is a pretty good strategy if satisfying assignments have high probability

[Mario Carneiro]

which might be the case due to structural features of the problem

[Kevin Buzzard]

These questions typically have one satisfying solution apparently

[Mario Carneiro]

well the interesting ones do, but a big portion of what a sat solver does is triage where it tries to determine quickly if a problem is easy. A lot of sat problems are literally bottlenecked on parsing the input