CODEWITHSUNDEEP
sat
BGR
BGR

Reputation: 159

Example of large solvable 3SAT problems with solution

does anyone knows a link to examples of solvable 3SAT problems, with also the solution to the problem?

Thanks

Upvotes: 0

Views: 1687

Answers (3)

Fabrice TIERCELIN
Fabrice TIERCELIN

Reputation: 993

To get a solveable problem with one solution, first build a solution and then build a problem on it:

  1. Choose any variables

    a, b, c, d, e, f

  2. Choose any values for those variables (at this point, we already have the solution)

    a = true, b = false, c = true, d = true, e = false, f = false

  3. Create a clause of 1, 2 or 3 literals, with at least one satisfied literal

    (¬c or d or e)

  4. Repeat step 3 as many time you want

    (¬c or d or e)

    and (a or ¬b or ¬d)

    and (b or e or ¬f)

    and (¬b or c or ¬f)

    and (c)

    and (a or d)

You have a solveable problem with a solution. This algorithm is exhaustive: You can get all the solveable problems.

Bonus To get an unsolveable problem:

  1. Define at least 3 variables

a, b, c, d, e, f

  1. Choose 3 variables among them

    b, d, f

  2. Create the 8 following clauses

    (b or d or f)

    and (b or d or ¬f)

    and (b or ¬d or f)

    and (b or ¬d or ¬f)

    and (¬b or d or f)

    and (¬b or d or ¬f)

    and (¬b or ¬d or f)

    and (¬b or ¬d or ¬f)

  3. Add any additional clauses

    ...

    and (¬c or d or e)

    and (a or ¬b or ¬d)

    and (b or e or ¬f)

    and (¬b or c or ¬f)

    and (c)

    and (a or d)

You have an unsolveable problem. This algorithm is not exhaustive: You won't get all the unsolveable problems

Upvotes: 1

BGR
BGR

Reputation: 159

this is what I did:

  1. download 3 SAT examples, for for example this site: https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html in the download items, UF means it is satisfiable, uuf it means it is unsatisfiable.

  2. Then I add these examples to https://msoos.github.io/cryptominisat_web/, which is a version of MiniSAT (SAT solver) in the browser.

  3. Click the play button, and MiniSAT calculates the solution.

Upvotes: 1

SebastianH
SebastianH

Reputation: 786

You can construct a trivial solveable 3Sat instance, which is solveable in polynomial time. There are several ways to construct trivial solveable 3Sat problems:

  • Use each variable exactly one times -> each variable setting is a solution
  • Don't use negations -> each variable is set to true is a solution
  • ...

I don't know a non trivial 3Sat example, which is big and solveable. Ones a year the Sat Competition is held. You can look into the benchmarks, whether there is a 3Sat benchmark.

Upvotes: 2

Related Questions