SAT plugin

The first problem identified as an NP-complete problem was SAT problem. For this one among other reasons, is usual to design solutions for SAT problems when studying models of computation and their theory of computational complexity.

P systems are not an exception, but all the oposite. In case studies some different solutions can be found, based on cell like P systems with active membranes, tissue like P systems will cell division, tissue P systems with cell separation and SN P systems.

Each solution has its own internal representation for objects coding formulas with their clauses and variables. But what it is clear that for the end user solving SAT problem the input is the same: that is, the formula itself. Something like this in CNF format (conjunctive normal form, or a conjunction of disjunctions of literals - variables or negations of variables):

../_images/SATformula.png

With the default mechanisms of MeCoSim, we can define an input table for entering information about each variable and each clause, indicating if it appears negated or not. That is, each tuple requires three data, that could lead to an input table with 3 columns:

../_images/SATInputTableConfig.png

Now as users we can forget about P systems and just enter our formula, that will be converted internally into simulation parameters for generating objects for the computation (as stated in simulation params tab, depending that step of the internal representation):

../_images/SATInputTable.png

Ok, not bad, but it is not so comfortable to introduce the formula. Well, it is a general purpose application that fulfill our requirements, and can be adapted to population dynamics and to SAT, but obviously you it is not a bespoke suit. Fortunately, SAT is so common that a custom suit was built in this case as a plugin. There we can enter the formula as it was initially presented in CNF format, obviously replacing OR by +, AND by * and negations by variables nx1 instead of x1:

../_images/SATplugin2.png

The generated table can be copied (Ctrl + C) and then pasted in the general purpose input table for input clauses and finally obtain the result (satisfiable formula or not):

../_images/SATresult.png

Test SAT plugin