home
work
logs
info
SAT Solver Group research on efficiency of satisfiability resolution strategies.
GitHub Repo
Findings
TECHNOLOGY
BUILD
Java
JUnit
Shell Script
TOOLS
IntelliJ
Bash
PLATFORMS
UNIX
ABOUT
DESCRIPTION
This research compares different satisfiability resolution techniques, such as DPLL and CDCL with different branching and conflict resolution heuristics. In this project, we implemented several heuristics for solving satisfiability and made comparisons through cnf formatted test cases. We also modelled the Einstein's Puzzle into CNF form to be used with our solvers.
MOTIVATION
The motivation behind creating the solvers was to understand the DPLL and CDCL algorithms through implementation, as well as to compare and benchmark different heuristics.
CHALLENGES
The challenge in this project was finding and implementing heuristics for conflict resolution and picking branch variables that can improve the solvers. We went through several research papers before settling with the more common techniques that could be implemented within the project timeframe.
DESIGN
SOLVERS
We implemented 2 solvers for this project:

Davis–Putnam–Logemann–Loveland (DPLL)
The DPLL algorithm is a backtracking search algorithm that performs chronological backtracking until the variables are exhausted. We wrote it in both recursive and iterative forms.

Conflict-Driven Clause Learning (CDCL)
The CDCL algorithm performs conflict clause learning and non-chronological backtracking by resolving an implication graph. CDCL can be customised with different heuristics for clause learning and picking branching variables.
CDCL HEURISTICS
For the CDCL solver, we implemented 3 variations of branching heuristics:

2-Clause
Pick an unassigned variable that occurred the most across 2­-clauses. This heuristic forces 2-­clauses to become assertive after decision­ making.

All Clause
Pick an unassigned variable that occurred the most across all clauses.

Random
Pick an unassigned variable randomly from a list of unassigned symbols.

For the conflict analysis and clause learning heuristic, we implemented 1-UIP:

1-Unique Implication Point (1-UIP)
We used the implication graph to extract antecedent clauses to apply resolution with, starting from the conflict clause antecedent to the conflict node. However, the resolution is terminated as soon as we have reached a state where only 1 variable in the resolved clause belongs to the conflict level. This provides us with an assertive clause that can be propagated after backtracking to the highest level of the remaining variables in the resolved clause.
EINSTEIN PUZZLE
The Einstein Puzzle is a logic puzzle that establishes a list of conditions among 5 neighbours. There are five houses in five different colors. In each house lives a person with a different nationality. The five owners drink a certain type of beverage, smoke a certain brand of cigar, and keep a certain pet. No owners have the same pet, smoke the same brand of cigar or drink the same beverage.

Question
Who owns the fish?

Hints
  • The Brit lives in the red house.
  • The Swede keeps dogs as pets.
  • The Dane drinks tea.
  • The green house is on the left of the white house.
  • The green house’s owner drinks coffee.
  • The person who smokes Pall Mall rears birds.
  • The owner of the yellow house smokes Dunhill.
  • The man living in the center house drinks milk.
  • The Norwegian lives in the first house.
  • The man who smokes Blends lives next to the one who keeps cats.
  • The man who keeps the horse lives next to the man who smokes Dunhill.
  • The owner who smokes Bluemasters drinks beer.
  • The man who keeps the horse lives next to the man who smokes Dunhill.
  • The German smokes Prince.
  • The Norwegian lives next to the blue house.
  • The man who smokes Blends has a neighbor who drinks water.

Assumptions
  • The owner is the resident of each house.
  • One of the residents owns the fish.
  • The term neighbor in the last hint refers only to a directly adjacent neighbor.
  • The houses are on the same side of the street.
  • They are next to each other, and are ordered from left to right as you face them.

To model this problem, we created 150 variables to capture states and possible combinations. From these 150 variables, we designed rules that comply with the conditions specified by the puzzle. These rules were represented by 1300 clauses, categorised into several sections.

Simple Rules
2-clauses to represent specified conditions that bind 2 properties.
(i.e. If person P is Dane, then person P drinks tea.)

Proximity Rules
Clauses representing implications between states (ownership of traits) and positions of the houses.
(i.e. If person P is in first house and has green house, then if person Q is in second house, then person Q has white house.)

Exactly-1 Rules
Clauses that limit the ownership of each category of traits for a single owner.
(i.e. If person P is in the first house, then person P cannot be in the second to fifth house, etc.)

Unicity Rules
Clauses that define the exclusivity of traits between the owners.
(i.e. If person P is in the first house, then person Q is not in the first house, etc.)

These set of literals and clauses were written in Conjunctive Normal Form (CNF) and used with our solvers to solve the puzzle.
TEAM
Chase Tiong Chase was responsible for writing the recursive DPLL solver, designing the data structures to represent literals and clauses, writing unit tests and shell scripts, analysis and benchmarking of results.
Huang Lie Jun I wrote the iterative DPLL solver, the implication graph data structures and modelled the Einstein's Puzzle. Chase and I worked on the CDCL solver and heuristics together.
REFERENCES
SATLIB Benchmark Problems A collection of satisfiability benchmark problems in cnf form.
Exponential Recency Weighted Average Branching Heuristic for SAT Solvers ERWA branching heuristics for CDCL solvers.
On Freezing and Reactivating Learnt Clauses Clause learning heuristics for CDCL solvers.
Clause Learning in SAT Seminar Automatic Problem Solving Clause learning with implementation of implication graph and use of unique implication points.
CDCL SAT Solvers Detailed notes on CDCL solvers and its constituent procedures.
VSIDS Branching Heuristics in CDCL SAT Solvers VSID branching heuristics for CDCL solvers.
Practical SAT Solving Reference SAT solving lecture series.
HypeDyn Stories
Food Logging
Hello world, let's connect!