Project INF432 2021 Stéphane Devismes & Benjamin Wack 1 Outline This project consists in using a SAT-solver to automatically solve some problems formalized in clauses. A SAT-solver is a generic tool for finding a model of a set of formulas : thus, your task is not to find specific resolution strategies for your problem, but rather to translate that problem into the formalism the SAT-solver expects, and to let it find a solution by itself. You will have to choose a problem (a logic grid game such as Sudoku) and study its rules. You will then modelize a grid of your problem using boolean variables only, and you will translate the rules of the game into logical formulas, more specifically conjunctive normal forms. Once the problem has been modelled and validated by your TD lecturer, you will program a software using the programming language of your choice, which takes an instance of your problem as an input, and creates a DIMACS file encoding that instance as a formula in conjunctive normal form. You will then choose a SAT-solver 1 that you will use to treat these DIMACS files. Finally, using the execution trace from the SAT-solver, you will display an understan- dable solution to the instance of your problem. Optionally, depending on how fast you've progressed in your project, you may trans- form the model of your problem into equivalent 3-SAT clauses (you can use the algorithm proposed in exercise 51 p. 11 of your exercise handout). If your group has been really fast, you may program your own SAT-solver too, which will be made easier using the 3-SAT transformation. Note : Your grade for the project will be based on three tasks : writing a clear, well-structured and rigorous report ; delivering a well-structured, readable source code together with relevant test cases ; actively participating to a presentation, which will include a demo of your software. In particular, any student that does not contribute significantly to the presentation faces the risk of receiving the grade 0 for their project. 1. For instance, MiniSat, Z3, Sattime, SAT4j, SATzilla, precosat, MXC, clasp, SApperloT, TNM, gNovelty2+, Rsat, Picosat, Minisat, Zchaff, Jerusat, Satzoo, Limmat, Berkmin, OKSolver, ManySAT 1.1, . . .(http://www.satcompetition.org/). 1 2 Your tasks For this project, students must work in groups (of 3 people ideally, or 4 if need be), select one of the suggested topics or choose one and have it approved by the TD lecturer. 2.1 Deliverables Your group will have to produce : 1. A report in which : you describe the problem you chose in English (rules, examples, constraints) ; you translate that problem into (propositional or first-order) logic ; you model the problem in conjunctive normal form (product of clauses) ; you explain the important points of the implementation of your programs ; you illustrate the use of your programs with relevant examples. 2. A collection of programs : an interface which takes an instance of the problem as an input, and creates a DIMACS file encoding that instance. In order to make testing efficient, your interface should be able to take its inputs at least from a file 2 , in a format you will define. Optionally, you can also let the user enter an instance through the keyboard or a graphical interface. if applicable, a program which reads a DIMACS file and returns a set of 3-SAT clauses in DIMACS format ; a program which, given the trace of the SAT-solver, displays an understandable solution to the problem ; if possible, a program which chains these steps together with the call to the SAT-solver. 3. A well-chosen set of instances of your problem, which will allow you to test your modelization. 4. A group presentation during which you will present your problem, its modeliza- tion, and you will run your programs on your personal computer, or a university computer. 2.2 Planning This document is online from the very beginning of the course, a short version is distributed to students. Your group and topic have to be chosen before the end of the 2 nd week of TD. Delivery, by email to the TD lecturer, of the pre-report describing the modelization part of the project (max 5 pages) no later than March 5 th 2021. Delivery, by email to the TD lecturer, of the final report and the source codes, no later than April 30 th 2021. Group presentation of your project during the weeks of May 3 rd -7 th or May 10 th - 12 th (20 minute presentations, question time included). 2. if you are using JAVA, you can mimic the example found at www-verimag.imag.fr/~devismes/ JAVA/Fichier.java. 3 Technical notes SAT and n-SAT Knowing if a propositional logic formula in conjunctive normal form (CNF) is satisfiable is called satisfiability problem or SAT problem. When a CNF formula only contains clauses of n literals, the problem is called n-SAT problem. DIMACS format : The format used as input to SAT-solvers is an international stan- dard used for endocing formulas in conjunctive normal form. A file in the DIMACS format begins with a line specifying that the formula is in normal form, the number of variables in the formula, and how many clauses it contains. For example, p cnf 5 3 says that the file contains a formula in conjunctive normal form with 5 variables and 3 clauses. Then, the following lines describe the clauses, one on each line. Each line contains positive or negative integers, and ends with a zero. A positive integer i indicates that the ith variable appears in the clause, whereas a negative integer −i indicates that the negation of the ith variable atppears in the clause. For example, here's a formula, followed by its encoding using the DIMACS format : (x1 ∨ ¬x5 ∨ x4) ∧ (¬x1 ∨ x5 ∨ x3 ∨ x4) ∧ (¬x3 ∨ ¬x4) c c start with comments c c p cnf 5 3 1 -5 4 0 -1 5 3 4 0 -3 -4 0 4 Examples of Possible Topics Any logical game that consists in filling a grid with all the useful information available can be modeled. For instance, you could tackle : Easy : N queens Lights Out Medium : Futoshiki Dosun-Fuwari Norinori Graph Coloring Takuzu Hard : Light Up Usowan Hashiwokakero Tetravex Kurotto Any other topic validated by your TD lecturer Other topics will be listed on page https://wackb.gricad-pages.univ-grenoble-alpes.fr/inf402/ together with links to demo applets. 5 Example with the Pigeon Problem We illustrate our minimum expectations for this project with a simple problem. 5.1 Problem A pigeon-fancier owns n nests and p pigeons. He wishes that : each pigeon lives in a nest, there be at most one pigeon per nest How can we help him with logic ? 5.2 Modeling the Problem Using First Order Logic Predicate P (i, j) is true if and only if pigeon i is in nest j. The constraints of the probmes are modelled as follows : Each pigeon lives in a nest : ∀i, ∃j, P (i, j). There is at most one pigeon in each nest : ∀i,∀k, i 6= k =⇒ ∀j, P (i, j) ∨ P (k, j). 5.3 Modelization in Conjunctive Normal Form The boolean variable xi,j is true if and only if pigeon i lives in nest j. For example, for a set of pigeons {a, b, c} and a set of nests {1, 2, 3, 4}, the following constraints must be given to the SAT-solver : (xa,1 ∨ xa,2 ∨ xa,3 ∨ xa,4) ∧ (xb,1 ∨ xb,2 ∨ xb,3 ∨ xb,4) ∧ (xc,1 ∨ xc,2 ∨ xc,3 ∨ xc,4) ∧ (xa,1 ∨ xb,1)∧ (xa,1 ∨ xc,1)∧ (xb,1 ∨ xc,1) ∧ (xa,2 ∨ xb,2)∧ (xa,2 ∨ xc,2)∧ (xb,2 ∨ xc,2) ∧ (xa,3 ∨ xb,3)∧ (xa,3 ∨ xc,3)∧ (xb,3 ∨ xc,3) ∧ (xa,4 ∨ xb,4)∧ (xa,4 ∨ xc,4)∧ (xb,4 ∨ xc,4) 5.4 Resolution by a SAT-solver After translating the cnf formula into the DIMACS format, a SAT-solver will give an assignment to each variable satisfying the system of contraints. Using this, we can deduce how to place each pigeon. We note that while this problem is very easy to solve manually, the computer will have to solve an exponential number of constraints to solve it using logic. 6 Optional part : SAT solver For the most advanced groups, you have the possibility of programming your own SAT solver (in your favourite programming language) with several resolution strategies. Your solver will be a WalkSat type solver (see paragraph below). It will take as input the set of clauses to resolve in the form of a DIMACS file. The aim is then to return an assignement satisfying all clauses in that set, whenever possible. Notice that WalkSat solvers are incomplete : if the set of clauses given as input is contradictory the solver will not be able to determine it. The pseudo-code of the WalkSat algorithm is given below as a reference. 1: Draw an assignment v at random according to a uniform distribution 2: i = 0 3: WHILE (v is not a model) and i < N DO 4: Pick a clause C amongst clauses C' such that v(C') = false 5: Draw a real number q in [0,1] according to a uniform distribution 6: IF q < P THEN 7: Pick a variable x in C according to a uniform distribution 8: ELSE 9: Pick a variable x in C deterministically 10: END IF 11: Flip the value of v(x) in the assignement v 12: i++ 13: END WHILE 14: IF v is a model THEN 15: RETURN v 16: ELSE 17: RETURN "undecided" 18: ENDIF The code above has gaps, and that is on purpose... Indeed it does not specify the values of N , P , or the procedure to deterministically choose variable x at line 9. It is up to you to determine a reasonable value for such constants, and to choose variable x so that it minimizes the number of unsatisfied clauses. Optionally, you may experiment so as to find the best possible values of N and P , and program other heuristics for the choice of x, for instance : Choose the least modified variable of C ; Assign to each variable y a score with computed as the difference between the number of positive occurences, and negative occurences across clauses. Then choose the variable with the best score ; Heuristics inspired from MOMS and JW heuristics given in the course notes ; A mix some of these strategies ; Etc. In that case it would be interesting to compare the different heuristics that you imple- mented. Note that to simplify your implementation, you can assume that the set of clauses received has been preprocessed to get an equivalent 3-SAT problem (see beginning of Part 2 of this document).
欢迎咨询51作业君