Proceedings of the 11th International Conference on Applied Informatics Eger, Hungary, January 29–31, 2020, published at http://ceur-ws.org The BWConverter Toolchain: An Incomplete Way to Convert SAT Problems into Directed Graphs∗ Tamás Balla, Csaba Biró, Gábor Kusper Eszterházy Károly University, Faculty of Informatics {balla.tamas,biro.csaba,kusper.gabor}@uni-eszterhazy.hu Abstract 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 difficult, so we introduce the BWConverter toolchain which helps us to create Black-and-White SAT instances, and convert them to directed graphs using different 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. Keywords: SAT, Strongly Connected Directed Graphs, BWConverter MSC: 03B05, 05C20 1. Introduction 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). 24 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 [1]. On the other hand 3-SAT is NP-complete [7]. So, there is a big the gap between the easiness of 2-SAT and hardness of 3-SAT. We know some classes which are between them: Horn SAT is the restriction to instances where each clause has at most one positive literal. Horn SAT is solvable in linear time [9], as are a number of gen- eralizations such as renamable Horn SAT [2], extended Horn SAT [6] and q-Horn SAT [5]. The hierarchy of tractable satisfiability problems [8], which is based on Horn SAT and 2-SAT, is solvable in polynomial time. An instance on the 𝑘-th level of the hierarchy is solvable in 𝑂(𝑛𝑘+1 ) time. 𝑟,𝑟-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 [15]. 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 [14]. 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 [3, 12]. We have presented two SAT solvers [4, 10, 11] and introduced several models [13]. 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 difficult, 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 25 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. 2. The BWConverter tool 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: {𝑎, 𝑏, 𝑐, ¬𝑑}. 26 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. 3. The NPP Tool 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 different 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. 1 https://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/DIMACS/PHOLE/descr.html 27 -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. 4. An Example 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. a a 133,33 % 66,66 % 133,33 % 133,33 % 133,33 % d 66,66 % b d b 133,33 % 66,66 % 133,33 % c c Result of using the tool with The generated graph from the formula -a -A (NPP -a -A) 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. References [1] B. Aspvall, M. F. Plass, R. E. Tarjan, A Linear-Time Algorithm For Testing The Truth Of Certain Quantified Boolean Formulas, Information Processing Letters, pp. 121–123, 1979. 28 [2] B. Aspvall, Recognizing Disguised NR(1) Instances of the Satisfiability Problem, J. of Algorithms, 1, pp. 97–103, 1980. [3] Cs. Biró, G. Kusper, Equivalence of Strongly Connected Graphs and Black-and- White 2-SAT Problems, Miskolc Mathematical Notes, Vol. 19, No. 2, pp. 755-768, 2018. [4] Cs. Biró and G. Kusper, BaW 1.0 - A Problem Specific SAT Solver for Effective Strong Connectivity Testing in Sparse Directed Graphs, CINTI-2018, pp. 137-142, 2018. [5] E. Boros, P. L. Hammer, X. Sun, Recognition of q-Horn Formulae in Linear Time. Discrete Applied Mathematics, v. 55, pp. 1–13, 1994. [6] V. Chandru, J. Hooker, Extended Horn Sets in Propositional Logic, J. of the ACM, 38(1), pp. 205–221, 1991. [7] S. A. Cook, The Complexity of Theorem-Proving Procedures, Proc of STOC’71, pp. 151–158, 1971. [8] M. Dalal, D. W. Etherington, A Hierarchy of Tractable Satisfiability Problems. Information Processing Letters, v.44, pp. 173–180, 1992. [9] W. F. Dowling, J. H. Gallier, Linear-Time Algorithms for Testing the Satisfia- bility of Propositional Horn Formulae. J. of Logic Programming, 1(3), pp. 267–284, 1984. [10] G. Kusper and Cs. Biró, Solving SAT by an Iterative Version of the Inclusion- Exclusion Principle, SYNASC 2015, IEEE Computer Society Press pp. 189–190, 2015. [11] G. Kusper, Cs. Biró, Gy. B. Iszály, SAT solving by CSFLOC, the next generation of full-length clause counting algorithms, Future IoT 2018, pp.1–9, 2018. [12] G. Kusper, Cs. Biró, Convert a Strongly Connected Directed Graph to a Black- and-White 3-SAT Problem by the Balatonboglár Model, submitted to Theory of Com- puting, 17 pages, arrived on 24.08.2019, status: under review. [13] G.Kusper, Cs. Biró, T. Balla, Representing Directed Graphs as 3-SAT Problems Using The Simplified Balatonboglár Model, The 11th International Conference on Applied Informatics to be held in Eger, Hungary January 29–31, 2020. [14] J. S. Schlipf, F. Annexstein, J. Franco, R. P. Swaminathan, On finding solutions for extended Horn formulas, Information Processing Letters, v. 54, pp. 133–137, 1995. [15] C. A. Tovey, A Simplified NP-complete Satisfiability Problem, Discrete Applied Mathematics, v. 8, pp. 85–89, 1984. 29