Skip to content

Latest commit

 

History

History
110 lines (74 loc) · 3.1 KB

README.md

File metadata and controls

110 lines (74 loc) · 3.1 KB
Raw

SAT-Solver

Running the SAT-Solver

Once built via cargo build --release the solver can be executed the following:

./target/release/sat [MODE] [FILEPATH] [FILEPATH] --heuristic [HEURISTIC] [FLAGS]

MODE

  • dpll
  • cdcl

HEURISTIC

Supported heuristics are:

  • arbitrary
  • dlis
  • dlcs
  • mom
  • boehm
  • jeroslaw_wang
  • vsids
  • custom

Flags

short long description
-H --heuristic Specify the heuristic to use [default: arbitrary]
-d --depth Shows the depth of the search tree
-k --k Argument for k-bounded learning [default: 10]
-m --m Argument for m-size relevance based learning [default: 10]
-s --subsumed_clauses Eliminates subsumed clauses
-f --flamegraph Specify whether to create a flamegraph
-r --restarts_threshold Specify the conflict threshold for a restart
-l --luby Use luby sequence for restarts
-F --restart_factor Specify the factor for restarts
-D --DRUP Output in DRUP format
-h --help Print help
-V --version Print version

CPU Time Measurement

To measure the CPU time for each .cnf file in src/inputs, run the cputime binary:

cargo run --bin cputime -- --time-limit [TIME-LIMIT] --heuristic [HEURISTIC]

TIME-LIMIT

Time-Limit arguments:

  • true: 60sec execution time frame (default value)
  • false: measures the duration of the execution without timeout

Plotting

To create the plots for the existing .csv files in src/cputime, run the plot binary: cargo run --bin plot

Running the tests

When cloning make sure to also sync the submodule which includes testfiles:

git submodule update --init --recursive

Run the tests using cargo:

cargo test --package sat_solver --lib -- cdcl --nocapture

Performance

We were able to solve 202 cnfs from exercise 2 correctly (same var assignment as minisat) and 199 finished with a timout of 60 seconds while the remaining three took just over a minute.

Average time for all 202 problems: 1.4s with vsids, without restarts. (gruppe-m-2/src/cputime/60sec_vsids.csv)
Average time for all 202 problems: 12.17s without vsids, without restarts. (gruppe-m-2/src/cputime/60sec_arbitrary.csv)

The problems from 2006th sat competition we tried to solve took no longer than 15mins.

Team Responsibilities

Noel:

  • Fix issue with Conflict analysis
  • Subsumed Clauses
  • Restarts
  • Drup logging

Laura:

  • Implication Graph
  • Conflict analysis

Flo:

  • 2-Watched Literals
  • Fix/Update impl. graph while setting vars
  • Fix/Rewrite Conflict analysis
  • Non-chron backtracking
  • Test + Debug non-chronological backtracking
  • Check whether unit clauses can occur in conflict analysis
  • Check impl for set_var in respect to unit clauses
  • Pure literal elimination as preprocessing
  • Output valid DIMACS solution
  • VSIDS performance

Our favourite Implication Graph during debugging