Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid the `CNF budget exceeded` exception via smarter translation into CNF. #4078

Merged
merged 3 commits into from Dec 12, 2014

Conversation

@gbasler
Copy link
Contributor

@gbasler gbasler commented Oct 27, 2014

The exhaustivity checks in the pattern matcher build a propositional
formula that must be converted into conjunctive normal form (CNF) in
order to be amenable to the following DPLL decision procedure.
However, the simple conversion into CNF via negation normal form and
Shannon expansion that was used has exponential worst-case complexity
and thus even simple problems could become untractable.

A better approach is to use a transformation into an equisatisfiable
CNF-formula (by generating auxiliary variables) that runs with linear
complexity. The commonly known Tseitin transformation uses bi-
implication. I have choosen for an enhancement: the Plaisted
transformation which uses implication only, thus the resulting CNF
formula has (on average) only half of the clauses of a Tseitin
transformation.

The Plaisted transformation uses the polarities of sub-expressions to
figure out which part of the bi-implication can be omitted. However,
if all sub-expressions have positive polarity (e.g., after
transformation into negation normal form) then the conversion is
rather simple and the pseudo-normalization via NNF increases chances
only one side of the bi-implication is needed.

I implemented only optimizations that had a substantial
effect on formula size:

  • formula simplification, extraction of multi argument operands
  • if a formula is already in CNF then the Tseitin/Plaisted
    transformation is omitted
  • Plaisted via NNF
  • omitted: (sharing of sub-formulas is also not implemented)
  • omitted: (clause subsumption)

Review by @adriaanm

gbasler and others added 3 commits Jun 15, 2014
Remove redundant UniqueSym class.
Signed-off-by: Gerard Basler <gerard.basler@gmail.com>
…o CNF.

The exhaustivity checks in the pattern matcher build a propositional
formula that must be converted into conjunctive normal form (CNF) in
order to be amenable to the following DPLL decision procedure.
However, the simple conversion into CNF via negation normal form and
Shannon expansion that was used has exponential worst-case complexity
and thus even simple problems could become untractable.

A better approach is to use a transformation into an _equisatisfiable_
CNF-formula (by generating auxiliary variables) that runs with linear
complexity. The commonly known Tseitin transformation uses bi-
implication. I have choosen for an enhancement: the Plaisted
transformation which uses implication only, thus the resulting CNF
formula has (on average) only half of the clauses of a Tseitin
transformation.

The Plaisted transformation uses the polarities of sub-expressions to
figure out which part of the bi-implication can be omitted. However,
if all sub-expressions have positive polarity (e.g., after
transformation into negation normal form) then the conversion is
rather simple and the pseudo-normalization via NNF increases chances
only one side of the bi-implication is needed.

I implemented only optimizations that had a substantial
effect on formula size:
- formula simplification, extraction of multi argument operands
- if a formula is already in CNF then the Tseitin/Plaisted
  transformation is omitted
- Plaisted via NNF
- omitted: (sharing of sub-formulas is also not implemented)
- omitted: (clause subsumption)
@scala-jenkins scala-jenkins added this to the 2.11.5 milestone Oct 27, 2014
@adriaanm
Copy link
Member

@adriaanm adriaanm commented Oct 27, 2014

Awesome! I'll take a look ASAP.

private val id: Int = Sym.nextSymId

override def toString = variable +"="+ const +"#"+ id
override def toString = variable + "=" + const + "#" + id

This comment has been minimized.

@soc

soc Oct 27, 2014
Member

Nit-picking: s"$variable=$const#$id"

@retronym
Copy link
Member

@retronym retronym commented Oct 27, 2014

Outstanding commit message!

Not sure how much scaffolding will be required, but it sure would be great if we could find a way to unit test the new transformation steps.

@adriaanm
Copy link
Member

@adriaanm adriaanm commented Oct 27, 2014

PLS REBUILD/pr-scala@654912f5020d4f42dff8e2f5a17bdfa5d37befa5

Spurious dbuild failure /cc @cunei (I can download the jar from my machine)

[sbt] [warn]    [NOT FOUND  ] com.typesafe.dbuild#d-projects_2.10;0.9.1!d-projects_2.10.jar (30094ms)
[sbt] [warn] ==== dbuild-snapshots: tried
[sbt] [warn]   http://typesafe.artifactoryonline.com/typesafe/temp-distributed-build-snapshots/com.typesafe.dbuild/d-projects_2.10/0.9.1/jars/d-projects_2.10.jar
[sbt] [warn]    ::::::::::::::::::::::::::::::::::::::::::::::
[sbt] [warn]    ::              FAILED DOWNLOADS            ::
[sbt] [warn]    :: ^ see resolution messages for details  ^ ::
[sbt] [warn]    ::::::::::::::::::::::::::::::::::::::::::::::
[sbt] [warn]    :: com.typesafe.dbuild#d-projects_2.10;0.9.1!d-projects_2.10.jar
[sbt] [warn]    ::::::::::::::::::::::::::::::::::::::::::::::
[sbt] sbt.ResolveException: download failed: com.typesafe.dbuild#d-projects_2.10;0.9.1!d-projects_2.10.jar
@scala-jenkins
Copy link

@scala-jenkins scala-jenkins commented Oct 27, 2014

(kitty-note-to-self: ignore 60575133)
🐱 Roger! Rebuilding pr-scala for 654912f. 🚨

@adriaanm adriaanm self-assigned this Oct 28, 2014
@retronym
Copy link
Member

@retronym retronym commented Oct 31, 2014

To flesh out on my unit testing idea, I wonder how much of the code we can exercise without bringing in Symbol / Tree / Type from the compiler, and instead using something like:

object TestSolver extends global.patmat.Solver {
  class Const;
  val NullConst = new Const;
  type Type = Int;

  case class TypeConst(i: Int) extends Const;
  object TypeConst extends TypeConstExtractor;
  case class ValueConst(i: Int) extends Const;
  object ValueConst extends ValueConstExtractor {
    def apply(t: Tree): Const = ???
  };

  class Tree;
  class Var(val x: Tree) extends AbsVar {
    def domainSyms = None;
    def implications = Nil;
    def mayBeNull = false;
    def propForEqualsTo(c: Const): Prop = ???;
    def registerEquality(c: Const) = ();
    def registerNull() = ();
    def symForStaticTp = None
  };

  object Var extends VarExtractor {
    def apply(x: Tree): Var = ???;
    def unapply(v: Var): Some[Tree] = Some(v.x)
  };

  def prepareNewAnalysis = {};
  def reportWarning(msg: String) = sys.error(msg)
}

We still have a dependency on global (although more refactoring could decouple that), but we then create a new implementatio of the Solver trait that allows for more direct testing of things like the CNF transform and the changes proposed in this PR.

Tests based on this could go into tests/junit/scala/tools/nsc/transform/patmat/SolverTest.scala.

@paulp
Copy link
Contributor

@paulp paulp commented Oct 31, 2014

trait that allows for more direct testing of things like the CNF transform and the changes proposed in this PR.

From there, such a small step to the observation that almost all the logic in the compiler could be decoupled from the compiler. Not because it's easier to test, though obviously it is, but for the million other reasons. Type inference is an especially offensive example, where frankly trivial problems have gone and will go unsolved indefinitely because you need a stomach of iron to go anywhere near the relevant pieces. But the pattern matcher has less excuse.

@adriaanm
Copy link
Member

@adriaanm adriaanm commented Oct 31, 2014

But the pattern matcher has less excuse.

True. It was designed with that goal in mind. (The goal of testing, not of making excuses.)

@gbasler
Copy link
Contributor Author

@gbasler gbasler commented Nov 2, 2014

Thanks Jason for the jump start, I'll try to add a test case.

@adriaanm

This comment has been minimized.

If it's necessary to have a _Linked_HashSet, could you add a comment to emphasize & explain this?

@adriaanm

This comment has been minimized.

maybe add a comment that we know Eq can no longer occur?

@adriaanm
Copy link
Member

@adriaanm adriaanm commented Nov 3, 2014

All this looks extremely good to me! I'm going to need a bit more time to digest the new CNF translation, so any additional comments in that part of the code would be appreciated!

I also feel like we're getting to the point of complexity that some testing of the solver is in order.

@adriaanm
Copy link
Member

@adriaanm adriaanm commented Nov 3, 2014

I don't want to block this PR on that, though.

@gbasler gbasler force-pushed the gbasler:topic/fix-analysis-budget branch from b8210c9 to 654912f Dec 11, 2014
adriaanm added a commit that referenced this pull request Dec 12, 2014
Avoid the `CNF budget exceeded` exception via smarter translation into CNF.
@adriaanm adriaanm merged commit d9f623d into scala:2.11.x Dec 12, 2014
1 check passed
1 check passed
default pr-scala Took 58 min.
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked issues

Successfully merging this pull request may close these issues.

None yet

6 participants
You can’t perform that action at this time.