Skip to content

Latest commit

 

History

History
81 lines (67 loc) · 1.57 KB

README.md

File metadata and controls

81 lines (67 loc) · 1.57 KB

incremental-examples

Some examples of using incremental SAT solvers (SAT/SMT/AR Summer School 2024). Check it out with:

git clone [email protected]:kfazekas/incremental-examples.git

0. Setup CaDiCaL

cd cadical
./configure
make

1. HCP2DIMACS example

cd 1_dimacs
make
./hcp2dimacs ../graphs/small-example.hcp | ../cadical/build/cadical
  • The following example takes ~21 seconds (49950 variables, 11039524 clauses):
./hcp2dimacs ../graphs/fhcpcs-graph28.hcp | ../cadical/build/cadical

2. HCP2IPASIR example

cd 2_ipasir
make
time ./hcp2ipasir ../graphs/small-example.hcp
time ./hcp2ipasir ../graphs/fhcpcs-graph1.hcp
  • The following example now takes only ~4 seconds:
time ./hcp2ipasir ../graphs/fhcpcs-graph28.hcp
  • The larger example needs more than 2 minutes:
time ./hcp2ipasir ../graphs/fhcpcs-graph70.hcp

3. HCP2CEGAR example

cd 3_ipasir_cegar
make
time ./hcp2cegar ../graphs/small-example.hcp
time ./hcp2cegar ../graphs/fhcpcs-graph1.hcp
  • Takes ~0,052s and 208 iterations:
time ./hcp2cegar ../graphs/fhcpcs-graph28.hcp
  • Takes ~0,179s and 323 iterations:
time ./hcp2cegar ../graphs/fhcpcs-graph70.hcp

4. HCP2IPASIRUP example

cd 4_ipasirup
make
time ./hcp2ipasirup ../graphs/small-example.hcp
time ./hcp2ipasirup ../graphs/fhcpcs-graph1.hcp
  • Takes ~0,015s and 41 sub-cycle is detected:
time ./hcp2ipasirup ../graphs/fhcpcs-graph28.hcp
  • Takes ~0,075s and 183 sub-cycle is detected:
time ./hcp2ipasirup ../graphs/fhcpcs-graph70.hcp