In our previous works we showed, how to convert a directed graph into a SAT problem. We showed that if the directed graph is strongly connected, then the converted SAT problem is Black-and-White. A SAT problem is Black-and-White if it has exactly two solutions, the black assignment, where each variable is false, and the white one, where each variable is true. In this paper, we study the other way: How to convert a SAT problem into a directed graph. This direction seems to be very dificult, so we introduce the BWConverter toolchain which helps us to create Black-and-White SAT instances, and convert them to directed graphs using diferent strategies. The toolchain consist of two tools: the BWConverter and the NPP tool. As a first step, one has to use the BWConverter tool, which creates a Black-and-White SAT problem from any UNSAT problems. The resulting SAT problem is Black-and-White if the input was UNSAT . As a second step, we generate a directed graph using our NPP tool. This tool generates edges from clauses which contain either exactly one positive literal, or exactly one negative one using the observations of our previous models.
The propositional satisfiability problem, for short the SAT problem, is the problem to find an assignment to the the Boolean variables of the input formula which ∗This research was supported by the grant EFOP-3.6.1-16-2016-00001 “Complex improvement of research capacities and services at Eszterházy Károly University”.
Copyright © 2020 for this paper by its authors. Use permitted under Creative Commons License
Attribution 4.0 International (CC BY 4.0).
makes it true. The formula is given in conjunctive normal form (CNF) which is
represented as a clause set. If each clause consists of at most literals, then it is a
-SAT problem. We know that the 2-SAT problem is solvable in linear time [
Horn SAT is the restriction to instances where each clause has at most one
positive literal. Horn SAT is solvable in linear time [
The hierarchy of tractable satisfiability problems [
, -SAT, where , -SAT is the class of problems in which every clause has
exactly literals and every variable has at most occurrences. All , -SAT problems
are satisfiable in polynomial time [
A formula is SLUR (Single Lookahead Unit Resolution) solvable if, for all possible
sequences of selected variables, algorithm SLUR does not give up. Algorithm SLUR
is a non-deterministic algorithm based on unit propagation. It eventually gives
up the search if it starts with, or creates, an unsatisfiable formula with no unit
clauses. The class of SLUR solvable formulae was developed as a generalization
including Horn SAT, renamable Horn SAT, extended Horn SAT, and the class of
CC-balanced formulae [
In this paper we restrict the general SAT problem such that each clause should contain at least one positive and one negative literal. We study how can we generate a directed graph from this kind of problem. Our goal is to give tools which help to do this work.
In our previous works we showed, how to convert a directed graph into a SAT
problem [
A SAT problem is Black-and-White if it has exactly two solutions, the black assignment, where each variable is false, and the white one, where each variable is true. In this paper, we study the other way: How to convert a SAT problem into a directed graph.
This direction seems to be very dificult, because if we would have a complete converter from SAT to directed graphs, then we could use our previous result to convert it to 2-SAT, i.e., we would have a SAT to 2-SAT converter. What we present is just an incomplete converter, so we do not attack the P = NP question.
The BWConverter toolchain contains two tools: the BWConverter and the NPP tool. As a first step, one has to use the BWConverter tool, which creates a Black-and-White SAT problem from UNSAT problems.
The BWConverter makes sure that its output has the same set of solutions as the input, except the black and the white assignment. To do so, we have implemented several algorithms.
The most interesting one introduces two new variables, and ; then it adds (¬ ) to each clause which contains only positive literals; then it adds ( ) to each clause which contains only negative ones; finally, it adds (¬ ∨ ) as a new clause to the output. The resulting SAT problem is Black-and-White if the input was UNSAT.
As a second step, we generate a directed graph using our NPP tool. This tool generates edges from clauses which contain either exactly one positive literal, or exactly one negative one using the observations of our previous models.
From example from the clause (¬ ∨ ∨ ) it generates the edges: → with weight 50%, and → with weight 50%. From the clause (¬ ∨ ¬ ∨ ) it generates the edges (the weights are in ()): → (50%), → (50%), → (50%), and → (50%). This conversation is too eager, because it creates a strongly connected graph even if the input was not a Black-and-White SAT problem. As a solution, we attach to each edge a weight number which indicates, how likely is that the edge is important. Then we iteratively remove the edges with the smallest and / or with the highest weight until we would have a non strongly connected directed graph in the next iteration. We call this directed graph to be the directed graph representation of the input SAT problem.
We studied where this state transition point is in case of unsatisfiable random 3-SAT problems.
The BWConverter tool can create a Black-and-White SAT problem from an UNSAT problem. It has 3 main switches: BWConverter -nooverlap num | BWConverter -n num BWConverter -overlap num | BWConverter -o num BWConverter -pigeonholeeater | BWConverter -p
After the first two ones we give a number, which shows how smart do we use these strategies. If the number is 0, then we do not use other input clauses to generate less clauses. 1 means that we use always the same clause to generate less clauses. 2 means that we use one of the best clause in order to generate as few clauses as possible.
They remove the black and the white clauses from each input clause. We introduce them by examples. Let us assume that the input has 6 variables: from to , these clauses was already processed: {, , }, {, , }, and the current clause is {, , }. Then: -n 0 generates: ¬ }, {, , , , , ¬ }. -n 1 generates: ¬ }. -n 2 generates: -o 0 generates: ¬ }, {, , , ¬ }. -o 1 generates: ¬ }. -o 2 generates: ¬ }, {, , , , ¬ }, {, , , , ¬ }. ¬ }, {, , , ¬ }, {, , , ¬ }. {, , , {, , , {, , , {, , , {, , , {, , ,
Note, that in case of -n there is no such full-length clause which is subsumed by the generated clauses, so they do not overlap.
-p introduces two new variables and ; then it adds (¬ ) to each clause which contains only positive literals; then it adds ( ) to each clause which contains only negative ones; finally, it adds (¬ ∨ ) as a new clause to the output. The resulting SAT problem is Black-and-White if the input was UNSAT.
An example for -p is the following: Let us assume that the input is ( ∨ ) ∧ ( ∨ ) ∧ ( ∨ ) ∧ (¬ ∨ ¬ ) ∧ (¬ ∨ ¬ ) ∧ (¬ ∨ ¬ ) ∧ (¬ ∨ ¬ ) ∧ (¬ ∨ ¬ ) ∧ (¬ ∨ ¬ ), which is actually the Pigeon Hole problem1 with 3 pigeons and 2 holes. Then the output is: (¬ ∨ ∨ ) ∧ (¬ ∨ ∨ ) ∧ (¬ ∨ ∨ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ (¬ ∨ ).
There are some more minor switches: -nob means that the output will not subsume the black clause. -now means that the output will not subsume the white clause. -bw means that the generated output will be a black-and-what SAT problem, if the input was an UNSAT problem. This is the same as -nob -now, and this is a default switch. -same means that the output problem will have the same set of solutions as the input, because it adds the black and the white clauses at the end of the output. -help prints the help.
The NPP tool work as follows: it reads a CNF file in DIMACS format. For each clause it adds the edges (, , ) to the graph, where is a negative literal, is a positive literal, and is 1/ , where is the number of positive literals in . It also adds the edges ( 1, 2, ) to the graph, where 1 and 2 are diferent negative literals, and = 1/ , where is the number of positive literals in .
For example if = {¬, ¬, ¬, , }, then the following edges is added to the graph: (, , 0.5), (, , 0.5), (, , 0.5), (, , 0.5), (, , 0.5), (, , 0.5), (, , 0.33), (, , 0.33), (, , 0.33), (, , 0.33), (, , 0.33), (, , 0.33).
The tool has the following switches: NPP -autominlimit | NPP -a NPP -automaxlimit | NPP -A NPP -setminlimit num | NPP -s num NPP -setmaxlimit num | NPP -S num NPP -normalized | NPP -N
-a finds the biggest limit, such that by deleting edges with weight ≤ limit the directed graph is still strongly connected. -A finds the lowest limit, such that by deleting edges with weight ≥ limit the directed graph is still strongly connected. -s sets the lower limit to num, i.e., it deletes all edges where the weight ≤ num. 1https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/PHOLE/descr.html -S sets the upper limit to num, i.e., it deletes all edges where the weight ≥ num.
The most typical usage is NPP -a -A which finds automatically both limits.
The output of the NNP tool is the adjency matrix of the constructed and modified graph. If = −1 that means that there is no directed vertex from to , otherwise the value is the weight of vertex from to . If we use -N switch the tool will normalize the weight values to [0; 1] interval before it removes any edge from graph.
The initial UNSAT 3-SAT formula let be as follows: (¬ ∨ ∨ ) ∧ ( ∨ ¬ ∨ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ ( ∨ ¬ ∨ ¬ ) ∧ (¬ ∨ ∨ ¬ ) ∧ ( ∨ ∨ ) ∧ (¬ ∨ ¬ ∨ ¬ ).
After running the BWConverter tool, the modified formula is as follows: (¬ ∨ ∨ )∧( ∨¬ ∨ )∧( ∨¬ ∨¬ )∧( ∨¬ ∨¬ )∧(¬ ∨ ∨¬ )∧( ∨ ∨ ∨¬ )∧(¬ ∨ ¬ ∨ ¬ ∨ ). Note, that this is not UNSAT any more, it is Black-and-White. 5. Usage and Conclusion The toolchain can be found here: http://fmv.ektf.hu/tools.html. It consists of two tools: BWConverter, and NPP. Its typical usage is the following: • java BWConverter -o 2 unsat.cnf bw.cnf • java NPP -a -A -N bw.cnf
This work was an inner project, because we used to need a tool to test our theories. For us the toolchain was very useful, so we decided to publish it. As future work we should prove the lemmas what we found by the help of this toolchain.