github/meteor
1
1
Fork 0
mirror of https://github.com/meteor/meteor.git synced 2026-05-02 03:01:46 -04:00
Code Issues Packages Projects Releases Wiki Activity
Files
c3d45ede004728f9dabd358af0c63cb49666b760
meteor/packages/logic-solver
History

README.md

Logic Solver

Introduction

Logic Solver is a boolean satisfiability solver written in JavaScript. Given a problem expressed as logical constraints on boolean (true/false) variables, it either provides a possible solution, or tells you definitively that there is no possible assignment of the variables that satisfies the constraints.

Many kinds of logic problems can be expressed in terms of constraints on boolean variables, including Sudoku puzzles, scheduling problems, and the package dependency problem faced by package managers that automatically resolve version conflicts.

Logic Solver can handle complex problems with thousands of variables, and has some powerful features such as incremental solving and solving under temporary assumptions. It also supports small-integer sums and inequalities, and can minimize or maximize an integer expression.

Logic Solver contains a copy of MiniSat, an industrial-strength SAT solver, compiled from C++ to JavaScript using Emscripten. See About MiniSat for more information.

XXX Link to a cool Sudoku demo. Show that this thing is actually pretty darn fast! Maybe include Sudoku as one of the code examples too, since the code is short and cool.

Table of Contents

Example: Dinner Guests

We are trying to decide what combination of Alice, Bob, and Charlie to invite over to dinner, subject to the following constraints:

  • Don't invite both Alice and Bob
  • Invite either Bob or Charlie

Setting up these constraints in code:

var solver = new Logic.Solver();

solver.require(Logic.atMostOne("Alice", "Bob"));
solver.require(Logic.or("Bob", "Charlie"));

Solving now will give us one possible solution, chosen arbitrarily:

var sol1 = solver.solve();
sol1.getTrueVars() // => ["Bob"]

Let's see what happens if we invite Alice. By using solveAssuming, we can look for a solution that makes an additional logical expression true over the ones we have required so far:

var sol2 = solver.solveAssuming("Alice");
sol2.getTrueVars() // => ["Alice", "Charlie"]

Aha! It seems that inviting Alice means we can't invite Bob, but then we must invite Charlie! If our reasoning is correct, it is impossible to invite Alice and not invite Charlie. We can confirm this:

solver.solveAssuming(Logic.and("Alice", "-Charlie")) // => null

(Note that "-Charlie" is shorthand for Logic.not("Charlie").)

Let's write some code to list all possible solutions:

var solutions = [];
var curSol;
while ((curSol = solver.solve())) {
  solutions.push(curSol.getTrueVars());
  solver.forbid(curSol.getFormula()); // forbid the current solution
}

solutions
// => [["Alice", "Charlie"], ["Charlie"], ["Bob", "Charlie"], ["Bob"]]

As you can see, there are four possible solutions to the original problem.

After running the above code, all possible solutions are now forbidden, so the solver is in an unsatisfiable state. Calls to solver.require and solver.forbid are permanent, so we cannot return to a satisfiable state, and any call to solve or solveAssuming henceforth will return no solution:

solver.solve() // => null

It's informative to look at the clauses generated by Logic Solver during this example. In this notation, v is the boolean "OR" operator:

-Alice v -Bob  (at most one of Alice, Bob)
Bob v Charlie  (at least one of Bob, Charlie)

Alice v -$assump1  (solve assuming Alice)

$and1 v -$assump2  (solve assuming Alice and not Charlie)
Alice v -$and1
-Charlie v -$and1

-Alice v Bob v -Charlie  (forbid ["Alice", "Charlie"])
Alice v Bob v -Charlie   (forbid ["Charlie"])
Alice v -Bob v -Charlie  (etc.)
Alice v -Bob v Charlie

These clauses are sent to MiniSat using variable numbers in place of names, making the entire problem quite compact:

[[-3,-4], [4,5],
 [3,-6],
 [8,-7], [3,-8], [-5,-8],
 [-3,4,-5], [3,4,-5], [3,-4,-5], [3,-4,5]]

Example: Magic Squares

A 3x3 "magic square" is an arrangement of the digits 1 through 9 into a square such that the digits in each row, column, and diagonal add up to the same number. Here is an example from Wikipedia:

2 7 6
9 5 1
4 3 8

Each row, column, and three-digit diagonal adds up to 15, as you can verify. (There are many 3x3 magic squares, but the magic sum is always 15, because all the digits together add up to 45!)

Let's use Logic Solver to find magic squares. We could be fancy about it and write code that would generalize to NxN magic squares, but let's keep it simple and name the digit locations as follows:

A B C
D E F
G H I

Because each location holds an integer, we must use integer variables instead of boolean variables. An integer in Logic Solver is represented as a group of bits, where each bit is a boolean variable, or an entire boolean formula. Let's create a 4-bit group of variables for each digit location:

var A = Logic.variableBits('A', 4);
var B = Logic.variableBits('B', 4);
var C = Logic.variableBits('C', 4);
var D = Logic.variableBits('D', 4);
var E = Logic.variableBits('E', 4);
var F = Logic.variableBits('F', 4);
var G = Logic.variableBits('G', 4);
var H = Logic.variableBits('H', 4);
var I = Logic.variableBits('I', 4);

var locations = [A, B, C, D, E, F, G, H, I];

A.bits // => ["A$0", "A$1", "A$2", "A$3"]

Let's also assign the number 15, in bit form, to a variable for convenience.

var fifteen = Logic.constantBits(15);
fifteen.bits // => ["$T", "$T", "$T", "$T"]

The binary representation of 15 is "1111", so its bit form consists of four copies of Logic.TRUE or "$T". We didn't have to know that, though, because Logic.constantBits generated it for us.

Now, we create a Solver and express our sum constraints:

var solver = new Logic.Solver();

_.each([[A,B,C], [D,E,F], [G,H,I], [A,D,G], [B,E,H], [C,F,I],
        [A,E,I], [G,E,C]],
       function (terms) {
         solver.require(Logic.equalBits(Logic.sum(terms), fifteen));
       });

Let's see what solution we get!

var sol1 = solver.solve();
sol1.evaluate(A) // => 3
sol1.evaluate(B) // => 10 (uh oh)
_.map(locations, function (loc) { return sol1.evaluate(loc); })
// => [3, 10, 2,
//     4,  5, 6,
//     8,  0, 7]

Oops, it looks like we forgot to specify that each "digit" is between 1 and 9! There is no harm done, because we have only underspecified the problem. We can continue to use the same solver instance.

Now we add inequalities to make each location A through I hold a number between 1 and 9 inclusive, and solve again:

_.each(locations, function (loc) {
  solver.require(Logic.greaterThanOrEqual(loc, Logic.constantBits(1)));
  solver.require(Logic.lessThanOrEqual(loc, Logic.constantBits(9)));
});

var sol2 = solver.solve();
_.map(locations, function (loc) { return sol2.evaluate(loc); })
// => [8, 1, 6,
//     3, 5, 7,
//     4, 9, 2]

Now we have a proper magic square!

However, it just so happens that we also forgot to specify that the numbers be distinct. To demonstrate that this is an important missing constraint, we can use solveAssuming to ask for a solution where A and B are equal:

var sol3 = solver.solveAssuming(Logic.equalBits(A, B));
_.map(locations, function (loc) { return sol3.evaluate(loc); })
// => [4, 4, 7,
//     8, 5, 2,
//     3, 6, 6]

Or where A, B, and C are equal:

var sol4 = solver.solveAssuming(Logic.and(Logic.equalBits(A, B),
                                          Logic.equalBits(B, C)));
_.map(locations, function (loc) { return sol4.evaluate(loc); })
// => [5, 5, 5,
//     5, 5, 5,
//     5, 5, 5]

A good way to enforce that all locations hold different digits is to generate a requirement about each pair of different locations:

_.each(locations, function (loc1, i) {
  _.each(locations, function (loc2, j) {
    if (i !== j) {
      solver.forbid(Logic.equalBits(loc1, loc2));
    }
  });
});

Solving now gives us a proper magic square again:

var sol5 = solver.solve();
_.map(locations, function (loc) { return sol5.evaluate(loc); })
// => [6, 7, 2,
//     1, 5, 9,
//     8, 3, 4]

If we wished to continue interrogating the solver, we could try asking for a magic square with a 1 in the upper-left corner, or proceed to enumerate a list of magic squares.

Finally, let's demonstrate that our "integers" are really just groups of boolean variables:

sol5.getTrueVars()
// => ["A$1", "A$2", "B$0", "B$1", "B$2", "C$1", "D$0", "E$0", "E$2",
//     "F$0", "F$3", "G$3", "H$0", "H$1", "I$2"]

_.map(A.bits, function (v) { return sol5.evaluate(v); })
// => [false, true, true, false]

You may be wondering whether it's bad that we generated 72 constraints as part of finding a 3x3 magic square. While there are certainly much faster ways to calculate magic squares, it is perfectly reasonable when setting up a logic problem to generate a complete set of pairwise constraints over N variables. In fact, having more constraints often improves performance in real-world problems, so it is worth generating extra constraints even when they are technically redundant. More constraints means more deductions can be made at each step, meaning fewer possibilities need to be tried that ultimately won't work out. In this case, it's important that when the solver assigns a digit to a particular location, it immediately be able to deduce that the same number does not appear at any other location.

Variables

Variable names are Strings which can contain spaces and punctuation:

Logic.implies('it is raining', 'take an umbrella');

Logic.exactlyOne("1,1", "1,2", "1,3")

Restrictions: A variable name must not be empty, consist of only the characters 0 through 9, or start with -. Variable names that start with $ are reserved for internal use.

You do not need to declare or create your variables before using them in formulas passed to require and forbid.

When you pass a variable name to a Solver for the first time, a variable number is allocated, and that name and number become synonymous for that Solver instance. You don't need to know about variable numbers to use Logic Solver, but you can always use a variable number in place of a variable name in terms and formulas, in case that is useful. (It is useful internally, and would probably be useful if you were to wrap Logic Solver in another library.) Examples of Solver methods that may allocate new variables are require, forbid, solveAssuming, and getVarNum.

If you want to add a free variable to a Solver but not require anything about it, you can use getVarNum to cause the variable to be allocated. It will then appear in solutions.

Methods

Logic.Solver#getVarNum(variableName, [noCreate])

Returns the variable number for a variable name, allocating a number if this is the first time this Solver has seen variableName.

Parameters
  • variableName - String - A valid variable name.
  • noCreate - Boolean - Optional. If true, this method will return 0 instead of allocating a new variable number if variableName is new.
Returns

Integer - A positive integer variable number, or 0 if noCreate is true and there is no variable number allocated for variableName.

Logic.Solver#getVarName(variableNum)

Returns the variable name for a given variable number. An error is thrown if variableNum is not an allocated variable number.

Parameters
  • variableNum - Integer - An allocated variable number.
Returns

String - A variable name.

Terms

A Term is a variable name or number, optionally negated. To negate a string Term, prefix it with "-". Examples of valid Terms are "foo", "-foo", 5, and -5. In other solvers and papers, you may see Terms referred to as "literals."

The following are equivalent:

solver.require("-A");
solver.require(Logic.not("A"));
solver.forbid("A");

In fact, Logic.not("A") returns "-A". It is valid to have more than one - in a Term ("---A"), and the meaning will be what you'd expect, but Logic.not will never return you such a Term, so in practice this case does not come up. Logic.not("-A") returns "A".

String Terms are called NameTerms, and numeric Terms are called NumTerms. You will not normally need to use numeric Terms, but if you do, note that it doesn't make sense to share them across Solver instances, because each Solver has its own variable numbers. See the Variables section for more information.

Constants

Logic.FALSE, Logic.TRUE

These Terms represent the constant boolean values false and true. You may seem them appear as the internal variables $F and $T or 1 and 2, which are automatically pinned to false and true.

Methods

Logic.isTerm(value)

Returns whether value is a valid Term. A valid Term is either a String consisting of a valid variable name preceded by zero or more - characters, or a non-zero integer.

Parameters
  • value - Any
Returns

Boolean

Logic.isNameTerm(value)

Returns whether value is a valid NameTerm (a Term that is a String).

Parameters
  • value - Any
Returns

Boolean

Logic.isNumTerm(value)

Returns whether value is a valid NumTerm (a Term that is a Number).

Parameters
  • value - Any
Returns

Boolean

Logic.Solver#toNameTerm(term)

Converts a Term to a NameTerm if it isn't already. If term is a NumTerm, the variable number is translated into a variable name. An error is thrown if the variable number is not an allocated variable number of this Solver.

Parameters
  • term - Term - The Term to convert, which may be a NameTerm or NumTerm.
Returns

NameTerm

Logic.Solver#toNumTerm(term, [noCreate])

Converts a Term to a NumTerm if it isn't already. If term is a NameTerm, the variable name is translated into a variable number. A new variable number is allocated if the variable name has not been seen before by this Solver, unless you pass true for noCreate.

Parameters
  • term - Term - The Term to convert, which may be a NameTerm or NumTerm.
  • noCreate - Boolean - Optional. If true, this method will not allocate a new variable number if it encounters a new variable name, but will return 0 instead.
Returns

NumTerm, or 0 (if noCreate is true and a new variable name is encountered)

Formulas

A Formula is an object representing a boolean expression. Conceptually, a Formula is built out of Terms and operations that combine Terms.

Here are some examples of Formulas:

// A and B
Logic.and("A", "B")

// If exactly one of (A, B, C) is true, then A does not equal D.
Logic.implies(Logic.exactlyOne("A", "B", "C"),
              Logic.not(Logic.equiv("A", "D")))

// More of (x1, x2, x3) are true than (y1, y2, y3)
var xs = ["x1", "x2", "x3"];
var ys = ["y1", "y2", "y3"];
Logic.greaterThan(Logic.sum(xs), Logic.sum(ys))

Formulas are immutable. To be on the safe side, do not mutate any arrays you use to create a Formula.

Formulas are Solver-independent. They can be created without a Solver, and although Solvers keep track of Formula objects and recognize them (to avoid compiling the same Formula twice), a Formula object never becomes tied to one Solver object and can always be reused, as long as it doesn't contain any explicit variable numbers (NumTerms).

A Term is not a Formula, but you can always pass a Term anywhere a Formula is required.

Functions such as Logic.and and Logic.greaterThan are called Formula constructor functions. One thing to note about them is that they do not always return Formulas, but may return Terms as well. Logic.and("A"), for example, returns "A". Some constructor functions take any number of arguments, which may be nested in arrays, so that the following are equivalent:

Logic.and("A", "B", "C")
Logic.and(["A", "B", "C"])
Logic.and("A", [["B", "C"]], [])

To use a Formula, you must tell a Solver to require or forbid it. Otherwise, the Formula does not take effect.

var solver = new Logic.Solver();
solver.require("A");

Logic.exactlyOne("A", "B"); // no effect, just creates a Formula

solver.require(Logic.exactlyOne("A", "B")); // this works

var myFormula = Logic.exactlyOne("A", "B");
solver.require(myFormula); // this also works

You should save and reuse Formula objects whenever possible, because the Solver will recognize the Formula object and not recompile it. Internally, each Formula is replaced by a variable in the Solver, such as $and1 for a Logic.and, and clauses are generated that relate the variable to the operands of the Formula. When you pass the same Formula object again, it is replaced by the same variable, and the Formula only needs to be compiled once.

Formulas that operate on integers are documented in the Bits section.

Methods

Logic.isFormula(value)

Returns true if value is a Formula object. (A Term is not a Formula.)

Parameters
  • value - Any
Returns

Boolean

Logic.not(operand)

Represents a boolean expression that is true when its operand is false, and vice versa.

When called on an operand that is a NameTerm, NumTerm, or Formula, returns a value of the same kind.

Parameters
  • operand - Formula or Term
Returns

Formula or Term (same kind as operand)

Examples
Logic.not("A") // => "-A"
Logic.not("-A") // => "A"
Logic.not(Logic.and("A", "B")) // => a Formula object

Logic.or(operands...)

Represents a boolean expression that is true when at least one of its operands is true.

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.and(operands...)

Represents a boolean expression that is true when all of its operands are true.

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.xor(operands...)

Represents a boolean expression that is true when an odd number of its operands are true.

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.implies(operand1, operand2)

Represents a boolean expression that is true unless operand1 is true and operand2 is false. In other words, if this Formula is required to be true, and operand1 is true, then operand2 must be true.

Parameters
  • operand1 - Formula or Term
  • operand2 - Formula or Term
Returns

Formula or Term

Logic.equiv(operand1, operand2)

Represents a boolean expression that is true when operand1 and operand2 are either both true or both false.

Parameters
  • operand1 - Formula or Term
  • operand2 - Formula or Term
Returns

Formula or Term

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.exactlyOne(operands...)

Represents a boolean expression that is true when exactly one of its operands is true.

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.atMostOne(operands...)

Represents a boolean expression that is true when zero or one of its operands are true.

Parameters
  • operands... - Zero or more Formulas, Terms, or Arrays
Returns

Formula or Term

Logic.Solver

You create a Logic.Solver with new Logic.Solver().

A Solver maintains a list of Formulas that must be true (or false), which you can think of as a list of constraints. Each Solver instance embeds a self-contained MiniSat instance, which learns and remembers facts that are derived from the constraints. At any time, you can ask the Solver for a solution that satisfies the current constraints, and it will either provide one (chosen arbitrarily) or report that none exists. You can then continue to add more constraints and solve again.

See Example: Dinner Guests for a good introduction to Solver.

Constraints are only ever added, never removed. If the current constraints are not satisfiable, then solve() will return null, and adding additional constraints cannot make the problem solvable again. However, using solveAssuming, you can look for a solution with a particular Formula temporarily in force. If solveAssuming returns null, there is no harm done, and you can continue to solve under other assumptions or add more constraints.

Sometimes solve() will take a long time! That is to be expected. The best thing to do is to try expressing the problem in a different way, with fewer variables, more sharing of common subexpressions, or more constraints between variables so that the solver can make important deductions in fewer steps. Also try wrapping your code in Logic.disablingAssertions(function () { ... }) in case runtime type checks are slowing down Formula compilation.

If you need an extra speed boost in Node, you could help me create a binary npm package containing a native-compiled MiniSat.

Logic.Solver#require(args...)

Requires that the Formulas and Terms listed in args be true in order for a solution to be valid.

Parameters
  • args... - Zero or more Formulas, Terms, or Arrays

Logic.Solver#forbid(args...)

Requires that the Formulas and Terms listed in args be false in order for a solution to be valid.

Parameters
  • args... - Zero or more Formulas, Terms, or Arrays

Logic.Solver#solve()

Finds a solution that satisfies all the constraints specified with require and forbid, or determines that no such solution is possible. A solution is an assignment of all the variables to boolean values.

To find more than one solution, you can forbid the first solution (using solver.forbid(solution.getFormula()), and solve again.

Solving is fully incremental, and each call to solve() has the benefit of everything learned by previous calls to solve(). Re-solving with one or two new constraints is typically very fast, because no work is repeated.

There is no guarantee of which solution is found if there are more than one. However, some statements can be made about what to expect:

  • MiniSat starts by trying a solution where all variables are false, so underconstrained variables will tend to be set to false.

  • Calling solve() repeatedly, with no intervening method calls, will in practice return the same solution each time. On the other hand, if you call solve, then solveAssuming, then solve again, the call to solveAssuming will affect the solution returned by the second solve.

  • Logic Solver and MiniSat are deterministic, so the same series of calls on a new Solver will generally produce the same results. However, the results may not be stable across different versions of Logic Solver.

Returns

Logic.Solution, or null if no solution is possible

Logic.Solver#solveAssuming(assumption)

Like solve(), but looks for a solution that additionally satisfies assumption. This is especially useful for testing whether a new constraint would make the problem unsolvable before requiring it, or for "querying" the solver about different types of solutions.

Note that any solution returned by solveAssuming is also a valid solution for solve to return. If you call solve, then solveAssuming, then solve again, the second solve will typically return the same solution as solveAssuming, because the internal state of the solver has been changed (even though no new permanent constraints have been introduced).

Parameters
  • assumption - Formula or Term
Returns

Logic.Solution or null

Logic.disablingAssertions(func)

Calls func(), disabling runtime type checks and assertions for the duration. This speeds up the processing of complex Formulas, especially when integers or large numbers of variables are involved, at the price of not validating the arguments to most function calls. It doesn't affect the time spent in MiniSat.

Parameters
  • func - Function
Returns

Any - The return value of func().

Logic.Solution

XXX

Optimization

XXX

Bits (integers)

XXX

About MiniSat

Solving satisfiability problems ("SAT-solving") is notoriously difficult from an algorithmic perspective, but solvers such as MiniSat implement advanced techniques that have come out of years of research. You can read more about MiniSat on its web page at http://minisat.se/.

MiniSat accepts input in "conjunctive normal form," which is a fairly low-level representation of a logic problem. Logic Solver's main job is to take arbitrary boolean formulas that you specify, such as "exactly one of A, B, and C is true," and compile them into a list of statements that must all be satisfied -- a conjunction of clauses -- each of which is a simple disjunction such as: "A or B or C." "Not A, or not B."

Although MiniSat operates on a low-level representation of the problem and has no explicit knowledge of its overall structure, it is able to use sophisticated techniques to derive new clauses that are implied by the existing clauses. A naive solver would try assigning values to some of the variables until a conflict occurs, and then backtrack, but not really learn anything from the conflict. Even custom solvers written for a particular problem often work this way. Solvers such as MiniSat, on the other hand, employ Conflict-Driven Clause Learning, which means that when they backtrack, they learn new clauses. These new clauses narrow the search space and cause subsequent trials to reach a conflict sooner, until the entire problem is found to be unsatisfiable or a valid assignment is found.

In principle, Logic Solver could be used as a clause generator for other SAT-solver backends besides MiniSat, or for a backend consisting of MiniSat compiled to native machine code instead of JavaScript.

Reference in New Issue View Git Blame Copy Permalink