SAT Flashcards
describe chronological backtracking?
> performance?
chronological backtracking: backtracking to the highest decision level that has not been tried with both values
> performs okay for randomly generated instances, performs bad for instances in practical applications
describe conflict driven learning
> what is the advantage/disadvantage?
conflict driven learning: solve until you reach a conflict
> formulate conflict as clause and add to list of clauses
> advantage: solver will not get into the same conflict again
what is decidability?
decidability: the guarantee to find an answer/find that there is no answer (given enough memory/runtime)
what are sources of incompleteness?
> incompleteness of input data
> insufficient runtime to wait for answer
what is undecidability?
undecidability: not always guaranteed to find an answer
which SAT problems are hard?
with n = number of variables and l = number of clauses
l/n = 4.26 > hard SAT problem
what are the properties of the SAT-complexity peak?
- very stable across problem size and solver types
- coincides with solubility transition
> l/n < 4.3 problems are underconstrained and SAT
> l/n > 4.3 problems are overconstrained and UNSAT
> this is also called “phase transition”
how does a local SAT search work?
local search:
1. make a random guess about variable values
2. test how wellthe guess is doing
3. flip a variable to improve
> e.g. flip variable that increases the number of clauses satisfied
local search: does flipping the most improving variable work?
> YES for 2SAT
> NO in general: usually does get stuck locally
explain GSAT
greedy SAT: because local search gets stuck, restart periodically with new initial guess
what is unusual about the search behavior of GSAT?
a lot of time is spent searching sideways > mostly searching on plateaus
what is MAXSAT?
MAXSAT is an optimization extension of SAT
> goal: find the maximum number of clauses that can be satisfied simultaneously
MAXSAT: how to model clause relevance?
model by assigning a cost to each clause if UNSAT
> if clause C is mandatory, cost is infinite and C is called HARD
> otherwise C is called SOFT
> any truth assignment has a cost which is the sum of all clause costs. try finding the truth assignment with the lowest finite cost
name 4 MAXSAT categories
- MAXSAT (ms): no hard clauses and all clauses have weight 1
- weighted MAXSAT (wms): no hard clauses
- partial MAXSAT(pms): hard clauses but all soft clauses have weight 1
- weighted partial MAXSAT (pwms): hard clauses and individual weight of soft clauses
what is 2SAT? (or 3SAT)
2SAT: conjunction of disjunctions of length 2
> solvable in polynomial time
