Node.js SAT solver tutorial
Sometimes, at Form und Zeichen, we face special requirements on a Web App. Many challenges can be tackled using familiar techniques such as if-statements, for-loops, handling asynchronous operations, and executing database queries. However, occasionally, we encounter problems that possess a logical nature, making them particularly challenging to solve iteratively.
This is where SAT solvers play a crucial role. These powerful tools are specifically designed to automatically solve intricate logic problems. In this article, I will delve into the utilization of SAT solvers and demonstrate how they can empower modern Next.js websites.
Logic-solver
Logic-solver is a npm package, that contains a copy of MiniSat which is a SAT solver written in C++. While SAT solvers in C++ are faster than the ones compiled to JavaScript, logic-solver has a big advantage. It is very easy to install and use for Node.js based web projects. However, the solving speed of logic-solver is still by far better, than an iterative program written to solve a logic problem.
A bicycle configurator as an example
Imagine you’re tasked with building a bicycle configurator for a webshop, catering to the preferences of customers. The objective is to display an image of a bicycle and provide visitors with various configuration options. These options include choosing the brake type, wheel size, and bicycle size.
However, it’s important to note that not all bicycle sizes support every wheel size. For instance, smaller wheel sizes are more suitable for children’s bikes. Additionally, certain combinations of bicycle size and wheel size restrict the availability of specific brake types.
Even in this simplified example with only three selectors, the task of accurately representing the behavior in our code is already becoming complex. If the customer were to request additional selectors, say ten in total, implementing an iterative solution would introduce significant complexity and increase the likelihood of errors.
Start by installing logic-solver.
npm i logic-solver
Defining the basic data structure
In this example, we organize the data in 3 arrays. They could be loaded from a database as well, but to keep things simple, we use static test data.
const breaks = [];
const wheels = [];
const bicycleSize = [];
The next step is to fill the array with our test data. In every entry of the breaks array, there is a wheels array. This array contains all wheel ids the break could be used for. Similarly, every wheel has a bicycleSizes array.
const breaks = [
{
id: 1,
name: 'standard break',
wheels: [1, 2, 3]
}, {
id: 2,
name: 'backpedal',
wheels: [1, 2]
}, {
id: 3,
name: 'disc break',
wheels: [3]
}
];
const wheels = [
{
id: 1,
name: '12 Inch Kids Wheel',
bicycleSizes: [1]
}, {
id: 2,
name: '20 Inch Kids Wheel',
bicycleSizes: [2]
}, {
id: 3,
name: '27.5 Inch Adults Wheel',
bicycleSizes: [3]
}
];
const bicycleSizes = [
{
id: 1,
name: 'small',
}, {
id: 2,
name: 'medium',
}, {
id: 3,
name: 'big',
}
];
Create a basic setup for our problem
The next step is to define some variables for the sovler. Set the number of bits to your needs.
import * as Logic from 'logic-solver';
const breakId = Logic.variableBits('BID', 8); // 8 bit number
const wheelId = Logic.variableBits('WID', 8);
const bicycleSizeID = Logic.variableBits('BSID', 8);
Let’s begin by introducing the first rule. There is a list of possible breakIds, wheelIds and bicycleSizeIds which we can retrieve from our database. In this three rules, I require element (break, wheel, bicycleSize) to get an ID out of all possible IDs.
const solver = new Logic.Solver();
const breakIds = breaks.map(b => b.id); // [1, 2, 3]
const wheelIds = wheels.map(w => w.id); // [1, 2, 3]
const bicycleSizeIDs = bicycleSizes.map(bs => bs.id); // [1, 2, 3]
solver.require(
Logic.or(
...breakIds.map(bid =>
(
Logic.equalBits(breakId, Logic.constantBits(bid))
)
)
)
);
solver.require(
Logic.or(
...wheelIds.map(wid =>
(
Logic.equalBits(wheelId, Logic.constantBits(wid))
)
)
)
);
solver.require(
Logic.or(
...bicycleSizeIDs.map(bsid =>
(
Logic.equalBits(bicycleSizeID, Logic.constantBits(bsid))
)
)
)
);
We already have enough code to make our first test. When the solver tries to find a solution, the only requirement is to set some IDs. The solver should just pick the first ID (ID 1) for every element. But even if it chooses different IDs, the solution is still correct for now.
const solution = solver.solve();
if (solution) {
const result = {
breakId: solution.evaluate(breakId),
wheelId: solution.evaluate(wheelId),
bicycleSizeID: solution.evaluate(bicycleSizeID)
}
console.log(result);
}
else {
console.log('error');
}
Expected output:
{ breakId: 1, wheelId: 1, bicycleSizeID: 1 }
Add missing requirements
Let’s add our final rules, that combine our products in a correct manner. Here, I setup a rule with the following meaning: If the selected breakId is [id] then only the following wheels are allowed [wheels array of the break object]. This is done by using the Logic.implies function and then a simple Logic.or.
Similarly, I use the same strategy for our wheels array.
solver.require(
Logic.and(
breaks.map(b =>
(
Logic.implies(
Logic.equalBits(breakId, Logic.constantBits(b.id)),
Logic.or(
b.wheels.map(w =>
(
Logic.equalBits(wheelId, Logic.constantBits(w))
)
)
)
)
)
)
)
);
solver.require(
Logic.and(
wheels.map(w =>
(
Logic.implies(
Logic.equalBits(wheelId, Logic.constantBits(w.id)),
Logic.or(
w.bicycleSizes.map(bs =>
(
Logic.equalBits(bicycleSizeID, Logic.constantBits(bs))
)
)
)
)
)
)
)
);
The expected output is still the same, because the break with the id 1, the wheel with the id 1 and the bicycle with the id 1 fit together. But if you tell the solver to use the break with the ID 3, things change. Because the break with ID 3 requires to use the wheel with the ID 3, we get a completely different solution.
Requireing specific settings for the break the wheel or the bicycle size is actually what you can use to consider user input.
solver.require(Logic.equalBits(breakId, Logic.constantBits(3)));
Expected output:
{ breakId: 3, wheelId: 3, bicycleSizeID: 3 }
How to get every possible solution
It is even possible to print out every possible solution. On big models this might take a while though. We could use this strategy to show the user only possible selection options for the current settings the user made.
let solution = solver.solve();
while (solution) {
const result = {
breakId: solution.evaluate(breakId),
wheelId: solution.evaluate(wheelId),
bicycleSizeID: solution.evaluate(bicycleSizeID)
}
console.log(result);
solver.forbid(solution.getFormula());
solution = solver.solve();
}
Expected output:
{ breakId: 1, wheelId: 1, bicycleSizeID: 1 }
{ breakId: 3, wheelId: 3, bicycleSizeID: 3 }
{ breakId: 2, wheelId: 2, bicycleSizeID: 2 }
{ breakId: 1, wheelId: 2, bicycleSizeID: 2 }
{ breakId: 1, wheelId: 3, bicycleSizeID: 3 }
{ breakId: 2, wheelId: 1, bicycleSizeID: 1 }
Notes
You need to add logicsolver.d.ts to your project root folder to make logic-solver work with typescript. The solving of a small model like the one in our example is very fast. If the model is very big and the formulas are complex, solving can take a lot of time.
In bigger solving projects, it is not enough to find a single solution. You might want to find the best solution possible. Finding the best solution is computational intensive, but if you are interested in an example, let us know and we will publish a blog post about this topic.
Conclusion
Logic-solver is a great library that offers an easy-to-use SAT solver for Node.js projects. It doesn’t offer the full functionality of a solver like Prolog, but it is good enough for the requirements of web projects.
Most of the time, it is not necessary to use a SAT solver. But for some projects they fit perfectly. In a project with complex logic formulas, using a SAT solver is extremely time-saving.
