DOC PREVIEW
CMU CS 15780 - Homework

This preview shows page 1 out of 4 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 4 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 4 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Graduate Artificial Intelligence 15-780Homework 2: Tree Search and SAT solving\Out on February 1Due on February 15Homework 2 Graduate Artificial Intelligence 15-780Problem 1: Proving with InstGenConsider the following formula:F = (∀x,P(x) ∨ Q(x)) ∧ (¬P (a) ∨ ¬P(b)) (1)Prove that F ⇒ ∃x,Q(x) using the InstGen algorithm given in class (pp. 38-47 in the slides for January 18th).For each iteration {0,... ,n}, please provide:• The first-order formula Gi;• The propositionalized formula G(Gr )i;• A propositional model M(Gr )for G(Gr )i;• The lifted model M for Gi;• The set of discordant pairs;• An application of InstGen on one of those discordant pairs that leads to Gi+1Discuss how you formed G0, and why you are using it to prove F ⇒ ∃x,Q(x). For the final iteration n reportwhich of the algorithm’s termination conditions you hit.We found a proof that took 4 applications of InstGen, but your proof may be longer. The propositional formulasG(Gr )ishould be simple enough to find models by hand.Problem 2: Build-A-SAT-Solver WorkshopIn this problem you need to build a boolean satisfiability solver that takes a set of variables and constraints in con-junctive normal form (CNF) and returns either a satisfying assignment or determines that no satisfying assignmentis possible.In particular, we are asking you to implement the DPLL algorithm—it is the basis for some of the world’s fastestSAT solvers. Even though SAT is an NP-complete problem DPLL typically has good empirical performance.The input will be provided in a simplified DIMACS CNF format (see, for example,http://www.satcompetition.org/2009/format-benchmarks2009.html):• Each line that starts with a ‘c’ is a comment;• The first non-comment line must be of the form: ‘p cnf〈numOfVariables〉 〈numOfClauses〉;• All other lines are space delimited lists of literals with a positive value indicating the variable and a negativevalue indicating its negation. For example, the number ‘-4’ represents ¬x4. Each line is terminated by a ‘0’.(Note: because of this don’t call any variable x0. Not only is this symbol reserved, but also 0 = −0.)For example, the formula (x1∨ ¬x2) ∧ (¬x1∨ x2∨ ¬x3) can be represented as:c Some made-up problemp cnf 3 21 -2 0-1 2 -3 0The solution should be a space delimited two column file with a row per variable. Each row should have theformat v a, where v is the variable number and a is either 0 or 1 (false or true). For example, a solution file for theabove problem might look like:1 02 03 0In this solution, each variable was set to false.Some test SAT problems can be found on the homework page. You can use the provided Python model verifierto check your solutions. Feel free to compare against minisat (http://minisat.se/) or any other existing solver.Just make sure that you hand in your own code.Page 1 of 3Homework 2 Graduate Artificial Intelligence 15-780In your implementation of DPLL, consider including the following features:• Unit propagation;• Variable ordering heuristics;• Value ordering heuristics;• Handling special cases (e.g. Horn clauses)Please do not include clause learning or or conflict-directed backjumping at this stage of your code. The solverthat you build here will be extended in the next problem set. Design your SAT solver with this in mind—make surethat your implementation is robust and easily extensible.We will not specify what language you should use, but you must provide two scripts to ease automated grading:• build.sh, a script that builds your project. For C++ this may be a bunch of g++ calls, or a single make call. Fora scripting language like Python this might be an empty file or a pleasant echo message for the grader.• run.sh, a script that takes in a single DIMACS CNF formatted file as input and prints either a solution or"UNSAT".In particular, your scripts should hook into a grading script that looks like:${DIR}/build.sh${DIR}/run.sh file1.cnf > ${DIR}/run_1.out${DIR}/run.sh file2.cnf > ${DIR}/run_2.out...How you will be graded:You must provide the following files:• The commented code for your solver;• Both build.sh and run.sh.Do not include any binaries.If your scripts do not conform to our naming standards, your code does not compile, or your code is a wrapperto an external SAT solver, the grader will be unhappy and mark accordingly. If the grader is in a good mood, theymight provide limited ‘run-time’ debugging, but do not count on it. Well commented code is always appreciatedand is known to put graders in a good mood.Your code will be first run against the provided test examples, then run against a reserved set of CNF problems.You will get full marks if your solver provides either a satisfying assignment or correctly identifies a formula asUNSAT within two minutes. (This is a generous cut-off and is per run.) Bonus marks will be awarded to the topthree fastest solvers for each problem instance in the reserved set.Code hand-in instructions will be sent out soon via email.Problem 3: Getting Empirical On Your SATWrite a random 3S AT generator. This generator should pass in two numbers: c and n. Given these numbers thegenerator should generate c clauses and write the result in the DIMACS format described in Problem 2. Each clauseshould have three literals selected uniformly from all possible literals of n variables. (recall that there are 2n literalsif there are n variables).Generate 25 different random 3SAT instances for n = 25 and c ={75,85,...,175}. Generate a further 25 differentrandom 3S AT instances for n = 50 and c ={150,170, ...,350}. This is a total of 550 problem instances—start theseexperiments early. Run your SAT solver from Problem 2 on each instance, and record the time that it takes to solveit and whether it was satisfiable or not.Page 2 of 3Homework 2 Graduate Artificial Intelligence 15-780a) Plot the probability of S AT vs. the ratiocnfor both n = 25 and n = 50 (separately; do not aggregate them).What do you notice? Can you explain this behavior?b) Plot a box-and-whiskers graph (see, for example, Matlab’s boxplot(X) command) for the runtime of yoursolver vs. the ratiocnfor both n = 25 and n = 50 (separately; do not aggregate them). What do you notice?Can you explain this behavior?Problem 4: Randomized SolversModify your solver from Problem 2 to branch randomly—branch by selecting a variable uniformly from the set ofremaining variables (not branched on; not unit-propagated).


View Full Document

CMU CS 15780 - Homework

Download Homework
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Homework and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Homework 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?