Commit Graph

67 Commits

Author SHA1 Message Date
David Greenspan
1b85b8205e Enable detailed profiling of the constraint solver
See the report using METEOR_PROFILE=1
2015-03-13 10:47:52 -07:00
David Greenspan
9f15f41482 Solve the "unknown var" problem more elegantly
The constraint-solver now uses the logic-solver in such a way that
accessing variables that weren't part of the problem statement will
never throw an error.  That way, we don't have to worry about
present and future cases where we don't generate any logical formulas
involving a package "foo" and then we say to minimize some weighted
sum over packages including "foo".
2015-03-13 06:37:06 -07:00
David Greenspan
78efe0b06b Don't run logic-solver tests on client
see comment
2015-03-10 12:31:49 -07:00
David Greenspan
dbfd1291c7 Code review changes
Validate package names in CS.Input.  Fix comments.  Remove dead code.
Use an equality requirement at the end of logic-solver's minMax.
2015-03-10 12:22:19 -07:00
David Greenspan
de5e67356a Some clean-up and allow minimization strategies 2015-03-09 23:15:25 -07:00
David Greenspan
5810fd6c81 Prevent stack overflow in logic-solver
Turn recursive addClauses->useFormulaTerm->addClauses into iterative.
Also do a couple tweaks that seem to improve performance.

The "stack overflow bug" case is now hovering around 10-20 seconds.
(It's a failure case, but it sure takes a while to fail.)
2015-03-09 22:20:34 -07:00
David Greenspan
eda46a2824 Get rid of the "zeroGoal" flag
From running benchmarks while changing the code:
* It doesn't seem to slow things down to *always* try to "hit 0"
  when minimizing
* It does seem to slow things down if the "<= 0" constraint is
  expressed using <= instead of "forbid the terms with non-zero
  weights"

This change also fixes a bug where we required terms with zero
weights to be 0.
2015-03-06 15:53:31 -08:00
David Greenspan
a78393b1e7 Implement "allAnswers" flag in constraint solver
I thought it would help me write a test for a bug that turned
up in code review, but it doesn't.  Still, I'm sure it will be
useful.

Also, Logic.Solution#getFormula is something I've been wanting
to write for a while.
2015-03-06 12:47:34 -08:00
David Greenspan
d34fc87d9b Recompile minisat 2015-03-05 17:55:42 -08:00
David Greenspan
9869245b8e Improve comments in optimize.js 2015-03-05 08:48:09 -08:00
David Greenspan
90c6b3e1bb No longer shift vars by 1 in MiniSat C wrapper
See 26e00d4d75
2015-03-05 08:23:24 -08:00
David Greenspan
023d471831 Code review changes to minisat_wrapper
All except fixing the 0-based/1-based thing
2015-03-04 17:46:14 -08:00
David Greenspan
8789a91d58 More code review changes (minisat_wrapper) 2015-03-04 16:45:42 -08:00
David Greenspan
b4da76a7e8 Improve comments 2015-03-04 14:22:45 -08:00
David Greenspan
db1e2ec823 Rebuild MiniSat with emscripten 1.28, new comment 2015-03-04 10:55:23 -08:00
David Greenspan
7ca88892e4 Add note to a logic_test 2015-03-04 10:10:42 -08:00
David Greenspan
1a648cf4c4 Clean up and comment Termifier interface 2015-03-04 10:06:37 -08:00
David Greenspan
8f84a60523 Make the "pushToNth" minor change from review
Just for clarity.

Add a needed test of weightedSum that catches "holes" in the array.
2015-03-04 09:11:57 -08:00
David Greenspan
f97f8f516a Fixes from initial review of logic.js except for…
…the pushToNth fix and documenting the "termifier" interface
2015-03-03 13:06:55 -08:00
David Greenspan
faa07c3e29 More code review changes; explain polarity
FormulaInfo is a constructed class
2015-03-03 12:47:47 -08:00
David Greenspan
8c095667e8 toNameTerm and toNumTerm no longer take arrays
this feature wasn't used anyway
2015-03-03 11:56:17 -08:00
David Greenspan
73306afa06 NameTerms can't be numbers or just - chars 2015-03-03 11:45:44 -08:00
David Greenspan
55c788a62f Fix bad order of declarations 2015-03-03 11:42:24 -08:00
David Greenspan
3ebeb5f0e6 Start making changes from Glasser initial review 2015-02-25 20:14:40 -08:00
David Greenspan
61f746989b Bump versions for new-version-solver-2 2015-02-09 21:57:39 -08:00
David Greenspan
0cef7aef20 Version bumps for release new-version-solver-1 2015-02-09 21:16:25 -08:00
David Greenspan
a5df9f84ab Implement proper cost function
Lots of things happened here:
* Refactored how cost minimization is expressed
* Cost function now distinguishes major/minor/patch/rest
* Order of terms is improved
* Reachability analysis of catalog makes benchmarks much faster
* Lock down versions of special packages before solving rest (perf)
* Explaining conflicts no longer crashes on cycles
* Antigravity for patches (and wrap nums, prereleases, etc.) so that
  we take bug fixes to indirect dependencies.

TODO:
* Refuse to make breaking changes to root reps
* Make sure we don't have antigravity changing any previous solutions
  for no reason
* Proper pre-release handling
* Unit tests
2015-02-06 20:47:31 -08:00
David Greenspan
3b41f812f8 Fix bug in optimization
I've been assuming that minimize/maximize requires the value to
remain the optimum, but it wasn't actually doing that.
2015-02-01 08:06:24 -08:00
David Greenspan
ff4398fe1c New constraint solver works!
It even explains conflicts.  It just doesn't spit out the list of
other constraints on conflicted packages yet (easy to do).

Left to do:
- Remove old solver code
- Call nudge()
- More nuanced cost function
- Clean up solver.js a little
- Proper handling of pre-release versions
- Lots more tests of different scenarios!
2015-01-30 16:45:28 -08:00
David Greenspan
2de487f631 Improve way to disable "check" in Logic
for speed
2015-01-28 15:54:51 -08:00
David Greenspan
3b2e1b7ab6 Let costWeights be a number instead of an array 2015-01-28 15:29:40 -08:00
David Greenspan
a04fbe89d0 Support getting MiniSat's conflict clause
It really just says which assumptions created the conflict when
solveAssuming is used.  And currently we only support one assumption
(which may represent a formula).  If we supported N assumptions, it's
possible MiniSat's analysis would tell us which of the N is the
problem.  It's not clear if it would be a minimal set though.

Still, might as well have the capability at the level of interfacing
with MiniSat in case it comes in handy.
2015-01-28 14:31:36 -08:00
David Greenspan
2491ffd9aa minimize/maximize in solver 2015-01-21 11:56:25 -08:00
David Greenspan
7450ac3de9 List of public API classes and functions 2015-01-21 11:56:25 -08:00
David Greenspan
a8268b659a Solution#evaluate; optimize/minimize 2015-01-21 11:56:25 -08:00
David Greenspan
f48e042a9e Eight queens and Sudoku
And some performance profiling.  Minified minisat.

Put in the code for N>3 atMostOne in case we need it.
2015-01-21 11:56:25 -08:00
David Greenspan
12dab04277 solveAssuming works 2015-01-21 11:56:24 -08:00
David Greenspan
a8a7902ad2 create Logic.Solution 2015-01-21 11:56:24 -08:00
David Greenspan
881d5702e1 Test calling MiniSat 2015-01-21 11:56:24 -08:00
David Greenspan
aea2f86abe Bring in MiniSat 2015-01-21 11:56:24 -08:00
David Greenspan
212c4811f1 Sums and tests 2015-01-21 11:56:24 -08:00
David Greenspan
bf218213f4 Half-adder, full-adder, and tests 2015-01-21 11:56:23 -08:00
David Greenspan
50fda15c99 lessThan[OrEqual] tests
The more complex ones aren’t hand-verified.  Will have to write more end-to-endy tests with the SAT solver.
2015-01-21 11:56:23 -08:00
David Greenspan
6e6a5b0ab6 Logic.lessThan[OrEqual], Logic.equalBits
Unit tests for equalBits; needs tests for lessThanOrEqual
2015-01-21 11:56:23 -08:00
David Greenspan
110222323b Logic.exactlyOne 2015-01-21 11:56:23 -08:00
David Greenspan
3c5ec3767e Logic.implies, Logic.equiv 2015-01-21 11:56:23 -08:00
David Greenspan
fd8eb4028b Test pointing out formula gen trade-off 2015-01-21 11:56:23 -08:00
David Greenspan
7e826a3394 More atMostOne tests 2015-01-21 11:56:22 -08:00
David Greenspan
0897883413 Logic.atMostOne works! Clause generation is clever
My program is surprising me with its concise generated CNF!  That is fun.
2015-01-21 11:56:22 -08:00
David Greenspan
9e55f9f7dc Finish _generateFormula and require/forbid
…in terms of what is which’s responsibility.

Allow Logic.xor(…) to return a term in the one-arg case.  From now on, helpers like Logic.and, Logic.or, and Logic.xor don’t have to return AndFormulas, OrFormulas, or XorFormulas; they can return other formulas or terms if they like, resulting in fewer intermediate variables.

This completes nested formula generation, so now we are ready for atMostOne.
2015-01-21 11:56:22 -08:00