![]() There is also the option to have a NOT A, this is written as ~A. The variables have a label here, for example A. All boolean statements can be rewritten/transformed into this form.įirst we’ll need to learn some more terminology. The statement above is written in a particular way, it is called the conjunctive normal form (or CNF). (A or B or ~C) and (B or C) and (~B) and (~A or C) Conjunctive normal form (CNF) When a variable is assigned true or false, it is called a literal. These problems use boolean variables that can be either true or false. It turns out you can write a lot of ‘problems’ in a specific way as a special boolean formula. ![]() SAT is short for ‘satisfiability’, what people mean when they say SAT is: Boolean satisfiability problem. In this first part of the series we’ll cover: ![]() This will be the first post in a series about SAT solving where we’ll end up building a simple solver in Java later on. The whole concept blew my mind when I learned about how they worked. Most software developers have never heard about SAT solvers, but they are amazingly powerful and the algorithms behind them are actually very easy to understand. SAT solving: Introduction to SAT (part 1)
0 Comments
Leave a Reply. |