Implementation of boolean algebra in SymPy

[Hitesh Anand]

Hello there,

I had introduced myself earlier through this mailing list. I want to introduce a new feature to SymPy which will be focused mainly on boolean algebra concepts. I am mentioning my idea below and I hope I get some guidance about whether the idea is feasible or not by the helpful mentors here. So, the idea goes as following:

Title : Satisfiability solver using symbolic variables

So basically, most of us know about the Satisfiability problem, which is a NP-complete problem and quite a famous one. We are given various boolean variables and a formula consisting of various combination of these variables using ANDs, ORs and NOTs. 

If we are able to find a suitable assignment for these boolean variables, then the formula is said to be satisfiable, else unsatisfiable.

Status : I have went through various SymPy tutorials and tried many things myself but I didn't find much related to boolean algebra. Hence, this might act as a new feature made available by SymPy. 

Although this feature exists to some extent in other solvers such as Pysat, the symbols used to represent the boolean variables are not much clear. For example, if we are considering any graph problem, and we have to encode the variable corresponding to whether node 1 is connected to node 2 or not, we represent this encoding as some numerical value while implementing the solver. But, SymPy provides us the power of using simplified symbols that might be user-friendly and simpler to implement. For instance, in the above graph problem, the variable mentioned will be encoded as 'x12' which is quite easier to understand than the numerical encodings (1, 2, 3,.....) where we have to remember the encoding formula used.

Difficulty : The difficulty is between intermediate to advanced. I have implemented this SAT solver using python and although the algorithm was quite simple (recursive backtracking), it took me some time and effort to implement it using python. Even then, it worked only upto 40-50 boolean variables.

Approach : The approach will be on the lines of recursive backtracking, or the famous DPLL algorithm. 

 I have not mentioned the idea completely here, since I hope one of the mentors will guide me improving upon this idea so that we can add a remarkable new feature to Sympy. It will be very helpful for me to decide whether this idea is worth implementing or not and what should be the exact approach and implementation strategy.

Regards,

Hitesh

[Aaron Meurer]

SymPy already has a SAT solver (see the satisfiable() function).
However, there are many ways that the boolean logic functionalities of
SymPy can be improved. You can find some if you search the issue
tracker, or take a look at the code to see what sorts of things are
not implemented yet.

Aaron Meurer

> --
> You received this message because you are subscribed to the Google Groups "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sympy+un...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/sympy/089923b4-4fc7-4ce0-8da7-f5e038f71a37n%40googlegroups.com.